It looks like you're new here. If you want to get involved, click one of these buttons!

- All Categories 2.3K
- Chat 494
- ACT Study Group 6
- Green Mathematics 1
- Azimuth Math Review 6
- MIT 2020: Programming with Categories 53
- MIT 2020: Lectures 21
- MIT 2020: Exercises 25
- MIT 2019: Applied Category Theory 339
- MIT 2019: Lectures 79
- MIT 2019: Exercises 149
- MIT 2019: Chat 50
- UCR ACT Seminar 4
- General 64
- Azimuth Code Project 110
- Statistical methods 2
- Drafts 1
- Math Syntax Demos 15
- Wiki - Latest Changes 0
- Strategy 111
- Azimuth Project 1.1K

Options

Many of you are programmers - and many of you use languages like Haskell that make explicit use of category-theoretic concepts. The course is *not* mainly about programming. So, it's good to have a place specially for talking about
category theory in computer science. And that's this thread!

If you want to learn more, I recommend this:

- Bartosz Mileweski,
*Category Theory for Programmers*.

## Comments

The Mileweski course is on my queue as all my exposure to cat. theory has been through Haskell or presented in more-or-less sensational ways. What convinced me to pay attention was a conference talk about discovering the general form of a fold using categories. I still need to finish watching the talk but my working theory is that a math discipline that can derive something like that in such a beautiful way has to be worth learning.

`The Mileweski course is on my queue as all my exposure to cat. theory has been through Haskell or presented in more-or-less sensational ways. What convinced me to pay attention was a conference talk about discovering the general form of a fold using categories. I still need to finish watching the talk but my working theory is that a math discipline that can derive something like that in such a beautiful way has to be worth learning.`

The title of this discussion was borrowed from this YouTube video:

It's a pretty high-powered tour of how category theory has interacted with computer science over the decades, by an expert on this topic.

`The title of this discussion was borrowed from this YouTube video: * Philip Wadler, [Category Theory for the Working Hacker](https://www.youtube.com/watch?v=V10hzjgoklA). It's a pretty high-powered tour of how category theory has interacted with computer science over the decades, by an expert on this topic.`

I hope this is the right place to write this.

I was thinking about Fong and Spivak's first chapter, where they focus on Galois connections. Galois connections are a special case of

adjunctions, where the functors are acting over two posets.I thought it might be fun to do an exercise in Haskell based on Ed Kmett's adjunction library.

In Haskell, we can write an adjunction between two

endofunctorsas a type class. This type class has two natural transformations:`leftAdjunct`

and`rightAdjunct`

.In category theory, this is written as \(f \dashv g\)

In this class,

`leftAdjunct`

and`rightAdjunct`

are natural transformations and obey the following laws:Puzzle 1: Give the type class instance for`Adjunction ((,) e) ((->) e)`

Puzzle 2: Define`unit :: Adjunction f g => a -> g (f a)`

and`counit :: Adjunction f g => f (g a) -> a`

such that:Puzzle 3: Give a definition of`leftAdjunct`

and`rightAdjunct`

in terms of`unit`

and`counit`

(so now we can write`{-# MINIMAL (unit, counit) | (leftAdjunct, rightAdjunct) #-}`

when we define the`Adjunction`

type class).Puzzle 4: Check out thefunctor composition type constructor(:.:), and consider`Comp1 . unit :: Adjunction f g => a -> (g :.: f) a`

. Write out`instance Adjunction f g => Monad (g :.: f)`

where`return = Comp1 . unit`

. What popular monad is this isomorphic to in the special case of`Adjunction ((,) e) ((->) e)`

?`I hope this is the right place to write this. I was thinking about Fong and Spivak's first chapter, where they focus on [Galois connections](https://en.wikipedia.org/wiki/Galois_connection). Galois connections are a special case of [*adjunctions*](https://en.wikipedia.org/wiki/Adjoint_functors), where the functors are acting over two posets. I thought it might be fun to do an exercise in Haskell based on Ed Kmett's [adjunction](https://hackage.haskell.org/package/computational-algebra-0.3.0.0/docs/Data-Functor-Adjunction.html) library. In Haskell, we can write an adjunction between two _endofunctors_ as a type class. This type class has two natural transformations: <code>leftAdjunct</code> and <code>rightAdjunct</code>. <pre> {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE TypeOperators #-} module Adjunction where import GHC.Generics class (Functor f, Functor g) => Adjunction f g | f -> g, g -> f where leftAdjunct :: (f a -> b) -> a -> g b rightAdjunct :: (a -> g b) -> f a -> b </pre> In category theory, this is written as \\(f \dashv g\\) In this class, <code>leftAdjunct</code> and <code>rightAdjunct</code> are natural transformations and obey the following laws: <pre> -- leftAdjunct . rightAdjunct === id -- rightAdjunct . leftAdjunct === id </pre> **Puzzle 1**: Give the type class instance for <code>Adjunction ((,) e) ((->) e)</code> **Puzzle 2**: Define <code>unit :: Adjunction f g => a -> g (f a)</code> and <code>counit :: Adjunction f g => f (g a) -> a</code> such that: <pre> -- leftAdjunct counit === id -- rightAdjunct unit === id </pre> **Puzzle 3**: Give a definition of <code>leftAdjunct</code> and <code>rightAdjunct</code> in terms of <code>unit</code> and <code>counit</code> (so now we can write <code>{-# MINIMAL (unit, counit) | (leftAdjunct, rightAdjunct) #-}</code> when we define the <code>Adjunction</code> type class). **Puzzle 4**: Check out the [_functor composition type constructor_ (:.:)](https://hackage.haskell.org/package/base-4.11.0.0/docs/GHC-Generics.html#t::.:), and consider <code>Comp1 . unit :: Adjunction f g => a -> (g :.: f) a</code>. Write out <code>instance Adjunction f g => Monad (g :.: f)</code> where <code>return = Comp1 . unit</code>. What popular monad is this isomorphic to in the special case of <code>Adjunction ((,) e) ((->) e)</code>?`

I really appreciated this approach to interpretations of functional programs corresponding to different categories. It seems to me the more applied category theory we develop/discover, the more interpretations of functional programs we have!

Compiling to categories by Conal Elliott

`I really appreciated this approach to interpretations of functional programs corresponding to different categories. It seems to me the more applied category theory we develop/discover, the more interpretations of functional programs we have! [Compiling to categories by Conal Elliott](http://conal.net/papers/compiling-to-categories/) > It is well-known that the simply typed lambda-calculus is modeled by any cartesian closed category (CCC). This correspondence suggests giving typed functional programs a variety of interpretations, each corresponding to a different category. A convenient way to realize this idea is as a collection of meaning-preserving transformations added to an existing compiler, such as GHC for Haskell. This paper describes such an implementation and demonstrates its use for a variety of interpretations including hardware circuits, automatic differentiation, incremental computation, and interval analysis. Each such interpretation is a category easily defined in Haskell (outside of the compiler). The general technique appears to provide a compelling alternative to deeply embedded domain-specific languages.`

I'm near the beginning still, but so far Mileweski's Category Theory for Programmers looks like something I've wanted for years! Thanks for the link. (I remember some category theory from grad school, and I'm a pretty experienced programmer with a pretty functional style, but I don't understand the connections between the two fields at all.)

`I'm near the beginning still, but so far Mileweski's [Category Theory for Programmers](https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/) looks like something I've wanted for years! Thanks for the link. (I remember some category theory from grad school, and I'm a pretty experienced programmer with a pretty functional style, but I don't understand the connections between the two fields at all.)`

Solution to Puzzle 1Write out the types and then copy them to the term level.Solution to Puzzle 2This part requires some choices (type unification).Reasoning: To produce g (f a) we have leftAdjunct at our disposal. rightAdjunct wouldn't work because its g b is in negative position. Now, matching g (f a) against g b in our case says that b = f a. Hence

leftAdjunct :: (f a -> f a) -> (a -> g (f a))and we can fill the first argument with id.Reasoning: Now the roles are reversed. We want to consume f (g a). This means only a premise with f (g a) in negative position will be (or at least is likely to be) relevant. That premise is rightAdjunct. This time, matching f (g a) against f a gives a = g a (different a's). Hence

rightAdjunct :: (g a -> g b) -> (f (g a) -> b)and after identifying the type variables a and b we can fill the first argument again with id.Further reflection on positive and negative positions: In both leftAdjunct and rightAdjunct both a and b occur in both positive and negative position. a has positive position in f a since f is a covariant functor, not contravariant. The difference is that leftAdjunct has f and g in positive position, and rightAdjunct has them in negative position.

I think I first encountered the notion of positive and negative positions in an error message in Agda. Something like https://stackoverflow.com/questions/2583337/strictly-positive-in-agda. There is an air of fundamentality about it. Or maybe it's just part of our boolean culture.

`<b>Solution to Puzzle 1</b> Write out the types and then copy them to the term level. <pre>instance Adjunction ((,) e) ((->) e) where -- leftAdjunct :: ((e, a) -> b) -> (a -> (e -> b)) leftAdjunct u a e = u (e, a) -- rightAdjunct :: (a -> (e -> b)) -> ((e, a) -> b) rightAdjunct v (e, a) = v a e</pre> <b>Solution to Puzzle 2</b> This part requires some choices (type unification). <pre>unit :: Adjunction f g => a -> g (f a) unit = leftAdjunct id</pre> Reasoning: To produce g (f a) we have leftAdjunct at our disposal. rightAdjunct wouldn't work because its g b is in negative position. Now, matching g (f a) against g b in our case says that b = f a. Hence <i>leftAdjunct :: (f a -> f a) -> (a -> g (f a))</i> and we can fill the first argument with id. <pre>counit :: Adjunction f g => f (g a) -> a counit = rightAdjunct id</pre> Reasoning: Now the roles are reversed. We want to consume f (g a). This means only a premise with f (g a) in negative position will be (or at least is likely to be) relevant. That premise is rightAdjunct. This time, matching f (g a) against f a gives a = g a (different a's). Hence <i>rightAdjunct :: (g a -> g b) -> (f (g a) -> b)</i> and after identifying the type variables a and b we can fill the first argument again with id. Further reflection on positive and negative positions: In both leftAdjunct and rightAdjunct both a and b occur in both positive and negative position. a has positive position in f a since f is a covariant functor, not contravariant. The difference is that leftAdjunct has f and g in positive position, and rightAdjunct has them in negative position. I think I first encountered the notion of positive and negative positions in an error message in Agda. Something like https://stackoverflow.com/questions/2583337/strictly-positive-in-agda. There is an air of fundamentality about it. Or maybe it's just part of our boolean culture.`

Joel Sjögren: Great job! These solutions are absolutely correct.

I'd say these notions are fundamental.

I first encountered them in the Sahlqvist Theorem in modal logic, where consequents must always be positive.

They also appear in the Modal μ-calculus. Here you can only construct \(\mu x. \phi(x)\) if \(\phi\) is positive. In fact, in the modal-\(\mu\) calculus positive formulae express

monotone mapson power set algebra of the possible worlds in Kripke model. In this setting \(\mu x. \phi(x)\) expresses the fixed point of \(\phi\) as a monotone map, and it is well defined as a consequence of the Knaster-Tarski theorem.John Baez has a discussion of monotone maps in his thread Lecture 4 - Chapter 1: Galois Connections. For anyone interested, I'll move this discussion over there (since it's not really about Haskell)...

`Joel Sjögren: Great job! These solutions are absolutely correct. > I think I first encountered the notion of positive and negative positions in an error message in Agda. Something like https://stackoverflow.com/questions/2583337/strictly-positive-in-agda. There is an air of fundamentality about it. Or maybe it's just part of our boolean culture. I'd say these notions are fundamental. I first encountered them in the [Sahlqvist Theorem](https://www.encyclopediaofmath.org/index.php/Sahlqvist_theorem) in modal logic, where consequents must always be positive. They also appear in the [Modal μ-calculus](https://en.wikipedia.org/wiki/Modal_%CE%BC-calculus). Here you can only construct \\(\mu x. \phi(x)\\) if \\(\phi\\) is positive. In fact, in the modal-\\(\mu\\) calculus positive formulae express _monotone maps_ on power set algebra of the possible worlds in Kripke model. In this setting \\(\mu x. \phi(x)\\) expresses the fixed point of \\(\phi\\) as a monotone map, and it is well defined as a consequence of the [Knaster-Tarski theorem](https://en.wikipedia.org/wiki/Knaster%E2%80%93Tarski_theorem). John Baez has a discussion of monotone maps in his thread [Lecture 4 - Chapter 1: Galois Connections](https://forum.azimuthproject.org/discussion/1828/lecture-4-chapter-1-galois-connections). For anyone interested, I'll move this discussion over there (since it's not really about Haskell)...`

Scott Fleischman: Thanks for plugging my

Compiling to categoriespaper. Looking for additional fun and useful interpretations of functional programs is indeed one of my motivations for joining the class.Since writing that paper, I've further developed categories of differentiable functions and have begun applying them to elegant machine learning by directly differentiating Haskell programs. The current state of this work is described in a very recent paper

The simple essence of automatic differentiation (Differentiable functional programming made easy).Abstract:

Here's an older version of the abstract, making the categorical nature more explicit:

Questions and comments on these papers are most welcome!

`Scott Fleischman: Thanks for plugging my [*Compiling to categories*](http://conal.net/papers/compiling-to-categories/) paper. Looking for additional fun and useful interpretations of functional programs is indeed one of my motivations for joining the class. Since writing that paper, I've further developed categories of differentiable functions and have begun applying them to elegant machine learning by directly differentiating Haskell programs. The current state of this work is described in a very recent paper [*The simple essence of automatic differentiation (Differentiable functional programming made easy)*](http://conal.net/papers/essence-of-ad). Abstract: <blockquote> Automatic differentiation (AD) in reverse mode (RAD) is a central component of deep learning and other uses of large-scale optimization. Commonly used RAD algorithms such as backpropagation, however, are complex and stateful, hindering deep understanding, improvement, and parallel execution. This paper develops a simple, generalized AD algorithm calculated from a simple, natural specification. The general algorithm can be specialized by varying the representation of derivatives. In particular, applying well-known constructions to a naive representation yields two RAD algorithms that are far simpler than previously known. In contrast to commonly used RAD implementations, the algorithms defined here involve no graphs, tapes, variables, partial derivatives, or mutation. They are inherently parallel-friendly, correct by construction, and usable directly from an existing programming language with no need for new data types or programming style, thanks to use of an AD-agnostic compiler plugin. </blockquote> Here's an older version of the abstract, making the categorical nature more explicit: <blockquote> Automatic differentiation (AD) is often presented in two forms: forward mode and reverse mode. Forward mode is quite simple to implement and package via operator overloading, but is inefficient for many problems of practical interest such as deep learning and other uses of gradient-based optimization. Reverse mode (including its specialization, backpropagation) is much more efficient for these problems but is also typically given much more complicated explanations and implementations. This paper develops a very simple specification and implementation for mode-independent AD based on the vocabulary of categories. Although the categorical vocabulary would be awkward to write in directly, one can instead write regular Haskell programs to be converted to this vocabulary automatically (via a compiler plugin) and then interpreted as differentiable functions. The result is direct, exact, and efficient differentiation with no notational overhead. The specification and implementation are generalized considerably by parameterizing over an underlying category. This generalization is then easily specialized to two variations of reverse-mode AD. These reverse-mode implementations are much simpler than previously known and are composed from two generally useful category transformers: continuation-passing and dualization. All of the implementations are calculated from simple, homomorphic specifications and so are correct by construction. The dualized variant is suitable for gradient-based optimization and is particularly compelling in simplicity and efficiency, requiring no matrix-level representations or computations. </blockquote> Questions and comments on these papers are most welcome!`

Welcome Conal!

These papers look great, I'm working through both of them.

I hope this is not too premature, but I am excited to try to apply Michael Izbicki's 2013 work on applying monoids to speed up cross validation to your own work.

In addition, it would be great to understand your first paper. Hopefully this week or next week I can give writing a DSL that compiles to your framework a shot.

`Welcome Conal! These papers look great, I'm working through both of them. I hope this is not too premature, but I am excited to try to apply [Michael Izbicki's 2013](https://izbicki.me/public/papers/icml2013-algebraic-classifiers.pdf) work on applying monoids to speed up cross validation to your own work. In addition, it would be great to understand your first paper. Hopefully this week or next week I can give writing a DSL that compiles to your framework a shot.`

In trying to solve Puzze 4, I'm having some compilation problems. When I define

The compiler says it needs an Applicative for Monad (g :.: f), so I write

But now it complains with:

Any magic incantantion (pragma, I suppose) to avoid the problem?

`In trying to solve Puzze 4, I'm having some compilation problems. When I define instance Adjunction f g => Monad (g :.: f) where return = Comp1 . unit (>>=) = undefined The compiler says it needs an Applicative for Monad (g :.: f), so I write instance Adjunction f g => Applicative (g :.: f) where pure = undefined (<*>) = undefined But now it complains with: Duplicate instance declarations: instance Adjunction f g => Applicative (g :.: f) -- Defined at /Users/jmgimeno/Dropbox/Developer/lleida-developers/haskell/haskellformac/AppliedCategoryTheory.hsproj/Adjunctions.hs:36:10 instance (Applicative f, Applicative g) => Applicative (f :.: g) -- Defined in ‘GHC.Generics’ Any magic incantantion (pragma, I suppose) to avoid the problem?`

Hi Conal and welcome. I was introduced to your papers here in this forum and they look great! I had never guessed that that book of Lambek and Scott had so tangible applications, and toching so disparage areas as hardware synthesis and ML. Look forward to more discussion.

`Hi Conal and welcome. I was introduced to your papers here in this forum and they look great! I had never guessed that that book of Lambek and Scott had so tangible applications, and toching so disparage areas as hardware synthesis and ML. Look forward to more discussion.`

Anybody know how diagrams like this (from the book) were created?

`Anybody know how diagrams like this (from the book) were created? ![pie recipe](https://user-images.githubusercontent.com/117439/38265765-6f15d1ce-373c-11e8-8e1a-15821414fa23.png)`

Hey Bob,

I suspect that Fong and Spivak used TikZ to make these string diagrams.

Here’s some links on how various people do it:

https://tex.stackexchange.com/a/264599

http://www.ryancreich.info/index.php?page=latex&subpage=string_diagrams

https://golem.ph.utexas.edu/category/2018/01/freetikz.html

`Hey Bob, I suspect that Fong and Spivak used TikZ to make these string diagrams. Here’s some links on how various people do it: - https://tex.stackexchange.com/a/264599 - http://www.ryancreich.info/index.php?page=latex&subpage=string_diagrams - https://golem.ph.utexas.edu/category/2018/01/freetikz.html`

Matthew, thanks a lot.

`Matthew, thanks a lot.`

Juan Manuel Gimeno #10 wrote:

Hmm... I'm bumping into this too.

I think it's easier if we skip

`GHC.Generics`

. Here's some boilerplate that should get you to where you want to be:`[Juan Manuel Gimeno #10](https://forum.azimuthproject.org/discussion/comment/16546/#Comment_16546) wrote: > Any magic incantation (pragma, I suppose) to avoid the problem? Hmm... I'm bumping into this too. I think it's easier if we skip `GHC.Generics`. Here's some boilerplate that should get you to where you want to be: <pre> {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE DeriveFunctor #-} module Adjunction where class (Functor f, Functor g) => Adjunction f g | f -> g, g -> f where leftAdjunct :: (f a -> b) -> a -> g b rightAdjunct :: (a -> g b) -> f a -> b unit :: Adjunction f g => a -> g (f a) unit = leftAdjunct id infixr 7 :.: newtype (:.:) (f :: k2 -> *) (g :: k1 -> k2) (p :: k1) = Comp1 { unComp1 :: f (g p) } deriving (Functor) instance Adjunction f g => Applicative (g :.: f) where pure = undefined (<*>) = undefined instance Adjunction f g => Monad (g :.: f) where return = Comp1 . unit (>>=) = undefined </pre>`

After Mathew's suggestion (thanks !!), I've been able to finish all the code:

`After Mathew's suggestion (thanks !!), I've been able to finish all the code: {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE DeriveFunctor #-} module Adjunction where import Control.Monad class (Functor f, Functor g) => Adjunction f g | f -> g, g -> f where {-# MINIMAL (unit, counit) | (leftAdjunct, rightAdjunct) #-} -- leftAdjunct . rightAdjunct === id -- rightAdjunct . leftAdjunct === id leftAdjunct :: (f a -> b) -> a -> g b leftAdjunct f = fmap f . unit rightAdjunct :: (a -> g b) -> f a -> b rightAdjunct f = counit . fmap f -- leftAdjunct counit === id -- rightAdjunct unit === id unit :: a -> g (f a) unit = leftAdjunct id counit :: f (g a) -> a counit = rightAdjunct id instance Adjunction ((,) e) ((->) e) where -- leftAdjunct :: ((e, a) -> b) -> a -> e -> b -- rightAdjunct :: (a -> e -> b) -> (e, a) -> b leftAdjunct f a e = f (e,a) rightAdjunct f (e,a) = f a e infixr 7 :.: newtype (:.:) (f :: k2 -> *) (g :: k1 -> k2) (p :: k1) = Comp1 { unComp1 :: f (g p) } deriving (Functor) instance Adjunction f g => Applicative (g :.: f) where pure = return (<*>) = ap instance Adjunction f g => Monad (g :.: f) where return = Comp1 . unit x >>= f = Comp1 (fmap (rightAdjunct (unComp1 . f)) (unComp1 x))`

Hi Juan, I can't compile your code with ghc-8.2.2 on windoze 10. I get a parse error on all the instances.

`Hi Juan, I can't compile your code with ghc-8.2.2 on windoze 10. I get a parse error on all the instances.`

Jim, I suppose that's because the first version I posted had extra spaces before the instances. Now I think the posted version is right. Haskell is very strict with indentation.

Tell me if there are more problems with the posted code and I'll try to fix them.

`Jim, I suppose that's because the first version I posted had extra spaces before the instances. Now I think the posted version is right. Haskell is very strict with indentation. Tell me if there are more problems with the posted code and I'll try to fix them.`

Great. Now compiles without the tabs. I can probably use it to cheat on Puzzle 4. Are you a 2 or 4 spaces person normally? :)

`Great. Now compiles without the tabs. I can probably use it to cheat on Puzzle 4. Are you a 2 or 4 spaces person normally? :)`

Personally I prefer 4 but, as I often work on my laptop, usually I use only two :-D

`Personally I prefer 4 but, as I often work on my laptop, usually I use only two :-D`

2 for me!

`2 for me!`

And the last piece of Puzzle 4 is the State monad which can be "tested" with:

`And the last piece of Puzzle 4 is the State monad which can be "tested" with: type MyState s = (((->) s) :.: ((,) s)) -- MyState s a = s -> (s, a) inc = Comp1 (\s -> (s+1, s+1)) double = Comp1 (\s -> (s*2, s*2)) computation = do a <- inc b <- double return b unComp1 computation 5 -- which returns (12, 12)`

Okay. We got adjunctions.

But so far we've been working with preorders and posets. How would one efficiently encode both preorders and posets and their operations?

`Okay. We got adjunctions. But so far we've been working with preorders and posets. How would one efficiently encode both preorders and posets and their operations?`

Do any of you have any suggestions for resources that will help me catch up with this convo? I've read though LYAH etc, but maybe could use a more in depth overview of Haskell typeclasses? Thanks

`Do any of you have any suggestions for resources that will help me catch up with this convo? I've read though LYAH etc, but maybe could use a more in depth overview of Haskell typeclasses? Thanks`

A good book alfter LYAH is Real World Haskell, which is also freely available at http://book.realworldhaskell.org/read/.

And the classic "reference" for typeclasses is the Typeclassopedia (https://wiki.haskell.org/Typeclassopedia) but it is very very dense and terse.

`A good book alfter LYAH is Real World Haskell, which is also freely available at http://book.realworldhaskell.org/read/. And the classic "reference" for typeclasses is the Typeclassopedia (https://wiki.haskell.org/Typeclassopedia) but it is very very dense and terse.`

Thanks Juan, I tried to read through the Typeclassopedia once but did find it too terse so I'll check out that other book.

`Thanks Juan, I tried to read through the Typeclassopedia once but did find it too terse so I'll check out that other book.`

@Juan : Excellent job! Thank you so much for this!

@Keith : The way I would model a preorder is with a function like

`(≤) :: a -> a -> Bool`

that obeys transitivity. I might use QuickCheck to enforce the laws it should obey in a unit test. I can't remember seeing someone do a supremum or infimum, but then again I'm just an acolyte at this stuff.There is a related construction I've seen, though.

I've alluded to in this thread and elsewhere that for any \(\bigwedge\)-complete semi-lattice \((L,\leq_L, \bigwedge)\) and monotone function \(f : L \to L\), then we can define:

$$ \mu f := \bigwedge \{x\ :\ f(x) \leq_L x \} $$ and \(\mu f\) is guaranteed to always exist.

We can think of

`μ :: forall a. (a -> a) -> a`

as a higher order function.Puzzle 5: How do you write`μ`

in Haskell?(Hint:

`(μ (\f n -> if (n==0) then 1 else n * f (n-1)) 5) == 120`

;-))Puzzle 6: What popular technologist news website is named after an alternate name given to`μ`

?`@Juan : Excellent job! Thank you so much for this! @Keith : The way I would model a preorder is with a function like `(≤) :: a -> a -> Bool` that obeys transitivity. I might use [QuickCheck](https://hackage.haskell.org/package/QuickCheck) to enforce the laws it should obey in a unit test. I can't remember seeing someone do a supremum or infimum, but then again I'm just an acolyte at this stuff. There is a related construction I've seen, though. I've alluded to in this thread and elsewhere that for any \\(\bigwedge\\)-complete semi-lattice \\((L,\leq_L, \bigwedge)\\) and monotone function \\(f : L \to L\\), then we can define: $$ \mu f := \bigwedge \\{x\ :\ f(x) \leq_L x \\} $$ and \\(\mu f\\) is guaranteed to always exist. We can think of `μ :: forall a. (a -> a) -> a` as a higher order function. **Puzzle 5**: How do you write `μ` in Haskell? (Hint: `(μ (\f n -> if (n==0) then 1 else n * f (n-1)) 5) == 120` ;-)) **Puzzle 6**: What popular technologist news website is named after an alternate name given to `μ`?`

Puzzle 5: mu f = let x = f x in x

One cheating strategy that I like: https://www.haskell.org/hoogle/?hoogle=forall+a.+(a+->+a)+->+a

Any intuitions available for the connection between the \(\mu \), adjoints and recursion? The high level picture isn't yet super clear to me.

Puzzle 6: presumably the y combinator, although I still don't really understand the relation between the untyped lambda expression for the y combinator \(\lambda f (\lambda x (f (x x)) (\lambda x (f (x x)) \) and the Haskell version.

`Puzzle 5: mu f = let x = f x in x One cheating strategy that I like: https://www.haskell.org/hoogle/?hoogle=forall+a.+%28a+-%3E+a%29+-%3E+a Any intuitions available for the connection between the \\(\mu \\), adjoints and recursion? The high level picture isn't yet super clear to me. Puzzle 6: presumably the y combinator, although I still don't really understand the relation between the untyped lambda expression for the y combinator \\(\lambda f (\lambda x (f (x x)) (\lambda x (f (x x)) \\) and the Haskell version.`

Hey Reuben,

First of all, excellent job!

Second, I should offer some explanation. I was cheating a bit. Let me explain.

If \(f\) is monotonic on some meet-complete semi lattice \(L\), then \(\mu f := \bigwedge \{x\ :\ f(x) \leq_L x \}\) is called \(f\)'s "Least Fixed Point". This is from the Knaster-Tarski Theorem.

Now \(\mu f\) obeys the equation:

$$ \mu f = f (\mu f) $$ In general in mathematics, when \(f(x) = x\), we say \(x\) is a fixed-point for \(f\). So \(\mu\) is often referred to as the "least fixed point operator". In Haskell, it is defined in the prelude and it is called

`fix`

.This operator is essentially the same as the \(\mathbf{Y}\) combinator. The \(\mathbf{Y}\) combinator is also known as the fixed-point combinator. In particular, it obeys the equation, for any \(\lambda\)-term \(F\):

$$ Y F \rightleftharpoons_\beta F (Y F) $$ Where \(\rightleftharpoons_\beta\) expresses \(\beta\)-equivalence.

Now to how I was cheating. The fact is \(\mu\) is a fixed-point operator for a rather special partial order. For instance,

`fix (\x -> 2*x-1)`

will not return 1. See this stack overflow for more discussion. The gist is becauseundefined, denoted`⊥`

, is a possible value and least fixed point for`\x -> 2*x - 1`

. The Haskell wiki has an introduction to denotational semantics which presents the relevant partial order \(\sqsubseteq\). Denotational semantics provides the partial order \(\sqsubseteq\) that \(\mu\) operates as a fixed point on.In fact, the proper definition of \(\mu\) given the partial order \(\sqsubseteq\) in denotational semantics is:...where \(f\) is a special kind of monotonic function called Scott Continuous. In denotational semantics we only have a

Directed Complete Partial Order(dcpo). Arbitrary joins are only guaranteed to exist for directed sets. This is why in domain theory we write \(\bigvee_{\sqsubseteq}\) or \(\text{sup}_{\sqsubseteq}\).Arbitrary meets are not guaranteed at all!With a little coaxing the two fixed-point definitions do coincide. But it involves a little heavy lifting:

Puzzle 7 (Maybe Hard):Let \((P, \subseteq, \bigvee_{\sqsubseteq})\) be adcpo. For a set \(A \subseteq P\) define \(A^u := \{p \in P\ :\ \forall a \in A. a \sqsubseteq p\}\) and \(A^d := \{p \in P\ :\ \forall a \in A. p \sqsubseteq a\}\). Define the Dedekind-Macneill completion \(\mathbf{DM}(P) := \{ A \subseteq P\ :\ A = (A^u)^d \} \); we have \(\left(\mathbf{DM}(P),\subseteq, \bigcup, \bigcap\right)\) is a complete lattice. There is an embedding \(\downarrow: P \to \mathbf{DM}(P) \) where \(x\downarrow := \{x\}^d\). Further, all Scott continuous functions \(f: P \to P\) can be lifted into monotonic functions \(f^\mathbf{DM}: \mathbf{DM}(P) \to \mathbf{DM}(P)\) with \(f^\mathbf{DM}(A) := ((f_!(A))^u)^d\) (where \(f_!\) is the push-forward of \(f\) that John Baez introduces in lecture 9).Show as an exercise:$$ \left(\bigvee_{\sqsubseteq} \left\{ \underbrace{f(f(f(\cdots(f}_n(\bot)))) \ :\ n\in \mathbb{N} \right\}\right)\Bigg\downarrow = \bigcap\{A \in \mathbf{DM}(P)\ :\ f^\mathbf{DM}(A) \subseteq A \} $$ ...So least fixed points from the Knaster-Tarski theorem coincide with least fixed points from domain theory in the Dedekind-Macneil Completion of a

dcpo.However, this is a purely mathematical construction. In programming we can't take Dedekind-Macneil completions and we can't compute arbitrary suprema or minima.

In Haskell when we deal with adjunctions or least fixed points, they are defined by construction.

There are still connections between least fixed points and adjunctions worth exploring, but I chat about them elsewhere since I think since they are pure math.

There are least fixed point and greatest fixed point type constructors

`Mu`

and`Nu`

. Ralf Hinz (2010) has an excellent paper on this worth exploring. Hinz touches on the adjoint relationship between the least fixed point and greatest fixed point.However, the least fixed point operator for a

dcpois a special case of a more general construction in category theory.Hopefully tomorrow or the day after I will give an exercise where we can build up to this, as well as see the fixed point operator's role in recursion.

[Edit: Added side condition for domain theory fixed point definition that \(f\) needs to be Scott continuous, and using proper definition of \(f^{\mathbf{DM}}\)]

`Hey Reuben, First of all, excellent job! Second, I should offer some explanation. I was cheating a bit. Let me explain. If \\(f\\) is monotonic on some meet-complete semi lattice \\(L\\), then \\(\mu f := \bigwedge \\{x\ :\ f(x) \leq_L x \\}\\) is called \\(f\\)'s "Least Fixed Point". This is from the [Knaster-Tarski Theorem](https://en.wikipedia.org/wiki/Knaster%E2%80%93Tarski_theorem). Now \\(\mu f\\) obeys the equation: $$ \mu f = f (\mu f) $$ In general in mathematics, when \\(f(x) = x\\), we say \\(x\\) is a fixed-point for \\(f\\). So \\(\mu\\) is often referred to as the "least fixed point operator". In Haskell, it is defined in the prelude and it is called `fix`. This operator is essentially the same as the \\(\mathbf{Y}\\) combinator. The \\(\mathbf{Y}\\) combinator is also known as the [fixed-point combinator](https://en.wikipedia.org/wiki/Fixed-point_combinator). In particular, it obeys the equation, for any \\(\lambda\\)-term \\(F\\): $$ Y F \rightleftharpoons_\beta F (Y F) $$ Where \\(\rightleftharpoons_\beta\\) expresses \\(\beta\\)-equivalence. Now to how I was cheating. The fact is \\(\mu\\) is a fixed-point operator for a rather special partial order. For instance, `fix (\x -> 2*x-1)` will not return 1. See this [stack overflow](https://stackoverflow.com/questions/4787421/how-do-i-use-fix-and-how-does-it-work) for more discussion. The gist is because *undefined*, denoted `⊥`, is a possible value and least fixed point for `\x -> 2*x - 1`. The Haskell wiki has an [introduction to denotational semantics](https://en.wikibooks.org/wiki/Haskell/Denotational_semantics) which presents the relevant partial order \\(\sqsubseteq\\). Denotational semantics provides the partial order \\(\sqsubseteq\\) that \\(\mu\\) operates as a fixed point on. ***In fact, the proper definition of \\(\mu\\) given the partial order \\(\sqsubseteq\\) in denotational semantics is:*** <center>\\(\mu f := \bigvee_{\sqsubseteq} \left\\{ \underbrace{f(f(f(\cdots(f}_n(\bot)\cdots))) \ :\ n\in \mathbb{N} \right\\}\\)</center> ...where \\(f\\) is a special kind of monotonic function called [Scott Continuous](https://en.wikipedia.org/wiki/Scott_continuity). In denotational semantics we only have a [*Directed Complete Partial Order* (**dcpo**)](https://en.wikipedia.org/wiki/Complete_partial_order#Definitions). Arbitrary joins are only guaranteed to exist for [directed sets](https://en.wikipedia.org/wiki/Directed_set). This is why in domain theory we write \\(\bigvee_{\sqsubseteq}\\) or \\(\text{sup}_{\sqsubseteq}\\). *Arbitrary meets are not guaranteed at all!* With a little coaxing the two fixed-point definitions do coincide. But it involves a little heavy lifting: **Puzzle 7 (Maybe Hard):** Let \\((P, \subseteq, \bigvee_{\sqsubseteq})\\) be a **dcpo**. For a set \\(A \subseteq P\\) define \\(A^u := \\{p \in P\ :\ \forall a \in A. a \sqsubseteq p\\}\\) and \\(A^d := \\{p \in P\ :\ \forall a \in A. p \sqsubseteq a\\}\\). Define the [Dedekind-Macneill completion](https://en.wikipedia.org/wiki/Dedekind%E2%80%93MacNeille_completion) \\(\mathbf{DM}(P) := \\{ A \subseteq P\ :\ A = (A^u)^d \\} \\); we have \\(\left(\mathbf{DM}(P),\subseteq, \bigcup, \bigcap\right)\\) is a complete lattice. There is an embedding \\(\downarrow: P \to \mathbf{DM}(P) \\) where \\(x\downarrow := \\{x\\}^d\\). Further, all Scott continuous functions \\(f: P \to P\\) can be lifted into monotonic functions \\(f^\mathbf{DM}: \mathbf{DM}(P) \to \mathbf{DM}(P)\\) with \\(f^\mathbf{DM}(A) := ((f_!(A))^u)^d\\) (where \\(f_!\\) is the push-forward of \\(f\\) that John Baez introduces in [lecture 9](https://forum.azimuthproject.org/discussion/1931/lecture-9-the-logic-of-subsets)). *Show as an exercise*: $$ \left(\bigvee_{\sqsubseteq} \left\\{ \underbrace{f(f(f(\cdots(f}_n(\bot)))) \ :\ n\in \mathbb{N} \right\\}\right)\Bigg\downarrow = \bigcap\\{A \in \mathbf{DM}(P)\ :\ f^\mathbf{DM}(A) \subseteq A \\} $$ ...So least fixed points from the Knaster-Tarski theorem coincide with least fixed points from domain theory in the Dedekind-Macneil Completion of a **dcpo**. However, this is a purely mathematical construction. In programming we can't take Dedekind-Macneil completions and we can't compute arbitrary suprema or minima. In Haskell when we deal with adjunctions or least fixed points, they are defined by construction. --------------------------------------------------------------------------------------- There are still connections between least fixed points and adjunctions worth exploring, but I chat about them elsewhere since I think since they are pure math. There are least fixed point and greatest fixed point type constructors `Mu` and `Nu`. [Ralf Hinz (2010)](http://www.cs.ox.ac.uk/ralf.hinze/SSGIP10/AdjointFolds.pdf) has an excellent paper on this worth exploring. Hinz touches on the adjoint relationship between the least fixed point and greatest fixed point. However, the least fixed point operator for a **dcpo** is a special case of a more general construction in category theory. Hopefully tomorrow or the day after I will give an exercise where we can build up to this, as well as see the fixed point operator's role in recursion. [Edit: Added side condition for domain theory fixed point definition that \\(f\\) needs to be Scott continuous, and using proper definition of \\(f^{\mathbf{DM}}\\)]`

One relation between the haskell code for the Adjunction typeclass and the Galois connections in the text is, for example, the proof that \( p \le g(f(p)) \).

The proof starts with \( f(p) \le f(p) \), and then applies the adjunction to get \( p \le g(f(p)) \).

In Haskell this corresponds to the implementation of the

`unit`

functionBeing

`unit`

the same function as the monad's`return`

(modulo use of`Comp1`

)What property of the Galois connection is proved by the implementation of bind`(>>=)`

?`One relation between the haskell code for the Adjunction typeclass and the Galois connections in the text is, for example, the proof that \\( p \le g(f(p)) \\). The proof starts with \\( f(p) \le f(p) \\), and then applies the adjunction to get \\( p \le g(f(p)) \\). In Haskell this corresponds to the implementation of the `unit` function unit :: a -> g(f(a)) unit = leftAdjunction id Being `unit` the same function as the monad's `return` (modulo use of `Comp1`) return = Comp1 . unit **What property of the Galois connection is proved by the implementation of bind `(>>=)` ?** x >>= f = Comp1 (fmap (rightAdjunct (unComp1 . f)) (unComp1 x))`

@Matthew thanks so much for this exposition! Will be a while before I can answer that puzzle, but it's a really cool insight into denotational semantics.

All this is starting to remind me of Hilbert's hotel in set theory, where (1+) is a fix point for the natural numbers, because they [0,succ(0),succ(succ(0))...]

`@Matthew thanks so much for this exposition! Will be a while before I can answer that puzzle, but it's a really cool insight into denotational semantics. All this is starting to remind me of Hilbert's hotel in set theory, where (1+) is a fix point for the natural numbers, because they [0,succ(0),succ(succ(0))...]`

@Reuben - Excellent you should mention that. That's some excellent intuition.

John Harrison's compute proof system HOL-Light uses the Knaster-Tarski theorem to construct the natural numbers. Here is the source code: https://github.com/jrh13/hol-light/blob/master/nums.ml

It's a little hard to read, so I will attempt to translate it.

In

Higher Order Logic(like HOL-Light, Isabelle/HOL or HOL5), the axiom of choice is defined in terms of theHilbert choice operator\(\epsilon\). It was introduced by David Hilbert (1926). It is a higher order function \(\epsilon : (p \to \mathbf{Bool}) \to p\). It obeys "The (Hilbert) Axiom of Choice":$$ \exists x. P(x) \Longleftrightarrow P (\epsilon P) $$ This is one of the three axioms of HOL-Light. One of the others is "The Axiom of Infinity":

$$ \text{there exists a type } \tau \text{ with a function } succ: \tau \to \tau \text{ that is injective but not surjective} $$ Since \(succ\) is not surjective, there is some number that is not in the range of \(succ\). Symbolically, this is \(\exists x . \forall y. succ(y) \neq x\). So consider the predicate \(R(x) : \tau \to \mathbf{Bool} := \forall y. succ(y) \neq x\). This expresses "\(x\) not in the range of \(succ\)". HOL-Light defines zero using Hilbert's choice operator and this predicate:

$$ 0 := \epsilon R $$ Zero exists as a consequence of Hilbert's axiom of choice.

Next Harrison defines his monotone map. He uses \(S(X) := succ_!(X) \cup \{0\}\) where I'm using John Baez's notation \(succ_!\) to mean the image of \(succ\). \(S\) is monotone because \(succ\) is injective.

He finally defines

$$ \mathbb{N} := \bigcap \{X\ :\ S(X) \subseteq X\} $$ Now Harrison actually uses a function he wrote called

`new_inductive_definition`

. The presentation here is more like Isabelle/HOL's construction. In Isabelle/HOL inductive definitions directly wraps the Knaster-Tarski fixed point contruction. However Isabelle/HOL doesn't do the other nice things Harrison does which follow the discussion above.`@Reuben - Excellent you should mention that. That's some excellent intuition. John Harrison's compute proof system HOL-Light uses the Knaster-Tarski theorem to construct the natural numbers. Here is the source code: https://github.com/jrh13/hol-light/blob/master/nums.ml It's a little hard to read, so I will attempt to translate it. In *Higher Order Logic* (like HOL-Light, Isabelle/HOL or HOL5), the axiom of choice is defined in terms of the *Hilbert choice operator* \\(\epsilon\\). It was introduced by [David Hilbert (1926)](https://eudml.org/doc/159124). It is a higher order function \\(\epsilon : (p \to \mathbf{Bool}) \to p\\). It obeys "The (Hilbert) Axiom of Choice": $$ \exists x. P(x) \Longleftrightarrow P (\epsilon P) $$ This is one of the three axioms of HOL-Light. One of the others is "The Axiom of Infinity": $$ \text{there exists a type } \tau \text{ with a function } succ: \tau \to \tau \text{ that is injective but not surjective} $$ Since \\(succ\\) is not surjective, there is some number that is not in the range of \\(succ\\). Symbolically, this is \\(\exists x . \forall y. succ(y) \neq x\\). So consider the predicate \\(R(x) : \tau \to \mathbf{Bool} := \forall y. succ(y) \neq x\\). This expresses "\\(x\\) not in the range of \\(succ\\)". HOL-Light defines zero using Hilbert's choice operator and this predicate: $$ 0 := \epsilon R $$ Zero exists as a consequence of Hilbert's axiom of choice. Next Harrison defines his monotone map. He uses \\(S(X) := succ_!(X) \cup \\{0\\}\\) where I'm using John Baez's notation \\(succ_!\\) to mean the image of \\(succ\\). \\(S\\) is monotone because \\(succ\\) is injective. He finally defines $$ \mathbb{N} := \bigcap \\{X\ :\ S(X) \subseteq X\\} $$ Now Harrison actually uses a function he wrote called `new_inductive_definition`. The presentation here is more like [Isabelle/HOL's construction](http://isabelle.in.tum.de/website-Isabelle2013/dist/library/HOL/Nat.html). In Isabelle/HOL inductive definitions directly wraps the Knaster-Tarski fixed point contruction. However Isabelle/HOL doesn't do the other nice things Harrison does which follow the discussion above.`

Wow, this is awesome, thanks! It fits nicely with the set theory I remember, and the natural numbers being the intersection of all inductive sets.

I still want to understand the connection to adjoints better. In particular, the definition of mu

\(\mu f := \bigwedge \{x\ :\ f(x) \leq_L x \}\)

is tantalizingly similar to the "process" for computing adjoints outlined in lecture 6.

`Wow, this is awesome, thanks! It fits nicely with the set theory I remember, and the natural numbers being the intersection of all inductive sets. I still want to understand the connection to adjoints better. In particular, the definition of mu \\(\mu f := \bigwedge \\{x\ :\ f(x) \leq_L x \\}\\) is tantalizingly similar to the "process" for computing adjoints outlined in lecture 6.`

A lot of people are excited about Conal Elliot's paper Compiling to Categories (2017). So I was thinking of adapting an exercise I know so we can start to understand it together.

Finally taglessDSLs are a style of specifying small languages in Haskell, Agda and Coq using type classes. They were first introduce by Carette, Kiselyov and Shan inFinally Tagless, Partially Evaluated. A real world example of an application of this approach is the servant library for building web applications in Haskell.What is flexible about finally tagless DSLs is that because the language is defined in a type class and the semantics are defined in a instance implementation.

My goal is to write a finally tagless DSL and ultimately write an instance implementation for it using the classes Conal Elliot introduces in §2 of his paper.

The following is adapted from Joseph Abrahamson, who originally published this exercise on Code Wars. It is open source under the BSD2 license.

This simple finally tagless DSL uses De Bruijn indices for encoding \(\lambda\)-expressions in the simply typed \(\lambda\)-calculus. It also includes a fixed point operation for encoding recursion as well as integers and .

For example the Haskell expression

would be expressed as a

`Term`

in this DSL withFinally Tagless Puzzle 1: Write an instance for this language.Here are some test vectors:

Finally Tagless Puzzle 2: Write an instance for this language without using`newtype`

or`data`

, just`base`

Finally Tagless Puzzle 3: Use the various category type classes that Conal Elliot introduces to make an abstract instance for this DSL (I have not yet managed this exercise myself, but you will need`NumCat`

and`BoolCat`

at least).If you are working this out, it doesn't hurt to read Oleg Kiselyov's lecture notes or watch Joseph Abrahamson's talk.

`A lot of people are excited about Conal Elliot's paper [Compiling to Categories (2017)](http://conal.net/papers/compiling-to-categories/). So I was thinking of adapting an exercise I know so we can start to understand it together. *Finally tagless* DSLs are a style of specifying small languages in Haskell, Agda and Coq using type classes. They were first introduce by Carette, Kiselyov and Shan in [*Finally Tagless, Partially Evaluated*](http://okmij.org/ftp/tagless-final/JFP.pdf). A real world example of an application of this approach is the [servant library](https://github.com/haskell-servant/servant) for building web applications in Haskell. What is flexible about finally tagless DSLs is that because the language is defined in a type class and the semantics are defined in a instance implementation. My goal is to write a finally tagless DSL and ultimately write an instance implementation for it using the classes Conal Elliot introduces in §2 of his paper. The following is adapted from Joseph Abrahamson, who originally published this exercise on [Code Wars](https://www.codewars.com). It is open source under the [BSD2 license][License]. This simple finally tagless DSL uses De Bruijn indices for encoding \\(\lambda\\)-expressions in the simply typed \\(\lambda\\)-calculus. It also includes a fixed point operation for encoding recursion as well as integers and . <pre> {-# LANGUAGE Rank2Types #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE ScopedTypeVariables #-} -- After getting rid of mocks, shouldn't need these two below {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MonoLocalBinds #-} module Tagless where import Prelude hiding (and, or) class Language k where here :: (a, h) `k` a before :: h `k` a -> (any, h) `k` a lambda :: (a, h) `k` b -> h `k` (a -> b) apply :: h `k` (a -> b) -> (h `k` a -> h `k` b) loop :: h `k` (a -> a) -> h `k` a int :: Int -> h `k` Int add :: h `k` Int -> h `k` Int -> h `k` Int down :: h `k` Int -> h `k` Int up :: h `k` Int -> h `k` Int mult :: h `k` Int -> h `k` Int -> h `k` Int gte :: h `k` Int -> h `k` Int -> h `k` Bool bool :: Bool -> h `k` Bool and :: h `k` Bool -> h `k` Bool -> h `k` Bool or :: h `k` Bool -> h `k` Bool -> h `k` Bool neg :: h `k` Bool -> h `k` Bool ifte :: h `k` Bool -> h `k` a -> h `k` a -> h `k` a class Language k => Interpreted k where run :: h `k` a -> h -> a type Term a = forall k h . Language k => h `k` a -- In the code below -- find a concrete value for `l` -- and elide all the mocks instance Language l where here = undefined before = undefined lambda = undefined apply = undefined loop = undefined int = undefined add = undefined mult = undefined down = undefined up = undefined gte = undefined bool = undefined and = undefined or = undefined neg = undefined ifte = undefined instance Interpreted l where run = undefined interpret :: Term a -> a interpret t = (run :: h `l` a -> h -> a) t () </pre> For example the Haskell expression \a -> \b -> a + b would be expressed as a `Term` in this DSL with ex :: Term (Int -> Int -> Int) ex = lambda (lambda (add (before here) here)) **Finally Tagless Puzzle 1**: Write an instance for this language. Here are some test vectors: <pre> interpret (apply (lambda here) (int 6)) == 6 </pre> <pre> interpret (apply (lambda here) (bool True)) == True </pre> <pre> interpret (ifte (bool True) (int 3) (int 4)) == 3 </pre> **Finally Tagless Puzzle 2**: Write an instance for this language without using `newtype` or `data`, just `base` **Finally Tagless Puzzle 3**: Use the various category type classes that Conal Elliot introduces to make an abstract instance for this DSL (I have not yet managed this exercise myself, but you will need `NumCat` and `BoolCat` at least). If you are working this out, it doesn't hurt to read [Oleg Kiselyov's lecture notes](http://okmij.org/ftp/tagless-final/course/lecture.pdf) or watch [Joseph Abrahamson's talk](https://www.youtube.com/watch?v=JxC1ExlLjgw). [License] : https://en.wikipedia.org/wiki/BSD_licenses#3-clause_license_(%22BSD_License_2.0%22,_%22Revised_BSD_License%22,_%22New_BSD_License%22,_or_%22Modified_BSD_License%22)`

@Mathew In the definition

`interpret t = run t ()`

GHC complains with

`Variable not in scope: run :: r0 h0 a -> () -> a`

`@Mathew In the definition `` interpret t = run t () `` GHC complains with `` Variable not in scope: run :: r0 h0 a -> () -> a ```

Good catch!

You have to implement

`run`

as part of the semantics. I'm afraid I've seen it's type signature vary from implementation to implementation, I'm still trying to wrap my head around how to make a type class for it. I will update this when I figure it out.However,

`run`

shouldn't be complicated. If you grasping for it, Oleg Kiselyov implements it near the top of page 27 of his lecture notes Typed Tagless Final Interpreters (2012). He gives his implementation of`interpret`

at the bottom.As an aside, I am still trying to figure out your puzzle. Can I have a hint? Is there a page in Fong and Spivak I should look at?

`Good catch! You have to implement `run` as part of the semantics. I'm afraid I've seen it's type signature vary from implementation to implementation, I'm still trying to wrap my head around how to make a type class for it. I will update this when I figure it out. However, `run` shouldn't be complicated. If you grasping for it, Oleg Kiselyov implements it near the top of page 27 of his lecture notes [Typed Tagless Final Interpreters (2012)](http://okmij.org/ftp/tagless-final/course/lecture.pdf). He gives his implementation of `interpret` at the bottom. ------------------------------------------- As an aside, I am still trying to figure out your puzzle. Can I have a hint? Is there a page in Fong and Spivak I should look at?`

@Matthew I’ve arrived only at page 7 of Kiseliov’s notes. I’ll come back to the puzzle after finishing it.

The solution of my “puzzle” I suppose has to do with the second property of closure operators, because the second condition is just the join function over monads.

In a monad I can interpret the implementation of bind as join composed with fmap. What I can’t interpret is this “flat composed with fmap” in preorder terms.

`@Matthew I’ve arrived only at page 7 of Kiseliov’s notes. I’ll come back to the puzzle after finishing it. The solution of my “puzzle” I suppose has to do with the second property of closure operators, because the second condition is just the join function over monads. In a monad I can interpret the implementation of bind as join composed with fmap. What I can’t interpret is this “flat composed with fmap” in preorder terms.`

Hey Juan!

Okay, I just edited my code above so it should compile. Note that switched from Oleg's notation to Conal's notation.

I added an

`Interpretable`

class. If a language implements`Interpretable`

it can be evaluated in Haskell. With this class there can be multiple instances of`run`

for different semantics. It's clear from reading Conal's paper that not every instance of this language can be`Interpretable`

. If you want to evaluate a term given some semantics you'll need to specialize`interpret`

using the clumsy way I've demonstrated.`Hey Juan! Okay, I just edited my code above so it should compile. Note that switched from Oleg's notation to Conal's notation. I added an `Interpretable` class. If a language implements `Interpretable` it can be evaluated in Haskell. With this class there can be multiple instances of `run` for different semantics. It's clear from reading Conal's paper that not every instance of this language can be `Interpretable`. If you want to evaluate a term given some semantics you'll need to specialize `interpret` using the clumsy way I've demonstrated.`

I have a lot of catching up to do on this thread, but I just got an email from David Spivak that might interest folks here:

A lot of these are coding projects. If anyone is seriously interested in trying them, please let David Spivak and me know!

Implement Functorial Data Migration using MapReduce. The iterative and join-based nature of many categorical algorithms make implementation using MapReduce/Hadoop particularly challenging. The goal of this project is to develop efficient algorithms for implementing functorial data migration on MapReduce.Implement a web-based GUI for Functorial Data Migration. The FQL tool is text-based and not particularly well-suited to run in a browser. Having a simple web-based GUI will help demonstrate functorial data migration to a larger class of people than currently possible. The goal of this project is to develop such a GUI.Implement a Categorical Theorem Prover. Modern theorem provers for first-order logic are not particularly well-suited for reasoning about categories, which requires purely equational reasoning, empty sorts, ground completeness, and other niche features. The goal of this project is to implement a theorem prover specifically tailored to categorical needs.Implement a Flexible FQL to SQL compiler. The FQL tool can interact with SQL databases, provided those databases are made up entirely of binary tables. This is an onerous restriction in practice, and theoretically, it should be possible for FQL to interact with any database that can be viewed as a database in categorical normal form. The goal of this project is to extend the class of SQL databases that FQL can interact with by revisiting FQL's core SQL generation algorithms.Develop an FQL Query Optimizer. Although the the equational theory for FQL is well defined (it is related to the internal language of cartesian closed categories), it is unclear how this equational theory can be used to actually optimize FQL queries. The goal of this project is to build an FQL query optimizer.Develop FQL Scenarios. The goal of this project is to use the FQL tool to solve real-world information-integration problems.Work through David Spivak's Book using FQL++. The FQL++ tool provides an extensive set of algorithms to compute with finite categories. The goal of this project is to use the FQL++ tool to solve the exercises in Category Theory for Scientists.Develop Operads for Domain Specific Languages. The goal of this project is to formalize particular domain specific languages as operads, possibly using the OPL tool.Integrate EASIK and FQL. Although the EASIK and FQL tools are based on similar categorical foundations, the tools do not interact particularly well. The goal of this project is to allow the tools to interoperate.Integrate FQL and a File System. A file system file and directory forms an acyclic graph, and aliases can be represented as path equations. The files themselves are given by a set-valued functor. The goal of this project is to express a file system as FQL schemas and instances. More speculatively, this could be the first step in a categorical database management system.Understand Geospatial databases using category theory. Interval-centric data can possibly be implemented using bi-modules.Develop a Theory of Functorial Data Isomorphism.Describe isomorphisms such as Sigma(F o G)(I) = (Sigma(F) o Sigma(G))(I), and develop a method of inserting them automatically into FQL programs, so that users can program up to isomorphism.Interpret Learn Reject.It may be possible for two people with no common ground to nevertheless develop a shared understanding of a domain by repeatedly following a loop that develops a span between schemas.Generalize to categories other than set.Develop a theory of functorial program migration/integration by generalizing results from the FQL project on functorial data migration/integration from the topos of Sets to the effective topos or domain-like things.Matching and inference.Generalize schema matching, entity resolution, and program synthesis techniques to infer schema mappings, instance mappings, and queries (bi-modules)Develop a Categorical Theory of Entity Resolution/Record Linkage.Extend the Functorial Data Model to include Nested Data, Aggregation, and Grouping.Extend the Functorial Data Model to include Richer Constraints, such as Embedded Dependencies/finite-limit theories.Extend the Functorial Data Model to include Updates and View-UpdatesExtend the Functorial Data Model to include Uncertain InformationConsistency and Conservativity in Functorial Data MigrationThe Sigma data migration functor, and other related operations, such as pushouts, do not preserve the consistency of their input instances; in logical terms the resulting equational theories need not be conservative extensions of their schemas. The goal of this project is to develop algorithms to detect what an instance presentation is not consistent, and to give proofs of situations when inconsistency cannot arise.Excel and FQL Interoperability. In principle spreadsheets have much structure relevant to FQL: each sheet is a table with unique row numbers, cells can reference other cells, mappings can be represented as two column tables, and data integrity constraints represented as formulas. The idea of this project is to import this structure into FQL, or, more speculatively, implement functorial data migration directly in Excel as a macro or extension.`I have a lot of catching up to do on this thread, but I just got an email from David Spivak that might interest folks here: > I was talking with Ryan Wisnesky today, and he pointed me to a [webpage full of project ideas](http://categoricaldata.net/projects.html) that your students might be interested in. A lot of these are coding projects. If anyone is seriously interested in trying them, please let [David Spivak](dspivak@categoricaldata.net) and me know! <ul> <li><b>Implement Functorial Data Migration using MapReduce</b>. The iterative and join-based nature of many categorical algorithms make implementation using MapReduce/Hadoop particularly challenging. The goal of this project is to develop efficient algorithms for implementing functorial data migration on MapReduce. </li> <li><b>Implement a web-based GUI for Functorial Data Migration</b>. The FQL tool is text-based and not particularly well-suited to run in a browser. Having a simple web-based GUI will help demonstrate functorial data migration to a larger class of people than currently possible. The goal of this project is to develop such a GUI. </li> <li><b>Implement a Categorical Theorem Prover</b>. Modern theorem provers for first-order logic are not particularly well-suited for reasoning about categories, which requires purely equational reasoning, empty sorts, ground completeness, and other niche features. The goal of this project is to implement a theorem prover specifically tailored to categorical needs.</li> <li><b>Implement a Flexible FQL to SQL compiler</b>. The FQL tool can interact with SQL databases, provided those databases are made up entirely of binary tables. This is an onerous restriction in practice, and theoretically, it should be possible for FQL to interact with any database that can be viewed as a database in categorical normal form. The goal of this project is to extend the class of SQL databases that FQL can interact with by revisiting FQL's core SQL generation algorithms. </li> <li><b>Develop an FQL Query Optimizer</b>. Although the the equational theory for FQL is well defined (it is related to the internal language of cartesian closed categories), it is unclear how this equational theory can be used to actually optimize FQL queries. The goal of this project is to build an FQL query optimizer.</li> <li><b>Develop FQL Scenarios</b>. The goal of this project is to use the FQL tool to solve real-world information-integration problems.</li> <li><b>Work through David Spivak's Book using FQL++</b>. The FQL++ tool provides an extensive set of algorithms to compute with finite categories. The goal of this project is to use the FQL++ tool to solve the exercises in Category Theory for Scientists.</li> <li><b>Develop Operads for Domain Specific Languages</b>. The goal of this project is to formalize particular domain specific languages as operads, possibly using the OPL tool.</li> <li><b>Integrate EASIK and FQL</b>. Although the EASIK and FQL tools are based on similar categorical foundations, the tools do not interact particularly well. The goal of this project is to allow the tools to interoperate.</li> <li><b>Integrate FQL and a File System</b>. A file system file and directory forms an acyclic graph, and aliases can be represented as path equations. The files themselves are given by a set-valued functor. The goal of this project is to express a file system as FQL schemas and instances. More speculatively, this could be the first step in a categorical database management system.</li> <li><b>Understand Geospatial databases using category theory</b>. Interval-centric data can possibly be implemented using bi-modules.</li> <li><b>Develop a Theory of Functorial Data Isomorphism.</b> Describe isomorphisms such as Sigma(F o G)(I) = (Sigma(F) o Sigma(G))(I), and develop a method of inserting them automatically into FQL programs, so that users can program up to isomorphism.</li> <li><b>Interpret Learn Reject.</b> It may be possible for two people with no common ground to nevertheless develop a shared understanding of a domain by repeatedly following a loop that develops a span between schemas.</li> <li><b>Generalize to categories other than set.</b> Develop a theory of functorial program migration/integration by generalizing results from the FQL project on functorial data migration/integration from the topos of Sets to the effective topos or domain-like things.</li> <li><b>Matching and inference.</b> Generalize schema matching, entity resolution, and program synthesis techniques to infer schema mappings, instance mappings, and queries (bi-modules)</li> <li><b>Develop a Categorical Theory of Entity Resolution/Record Linkage</b>.</li> <li><b>Extend the Functorial Data Model to include Nested Data, Aggregation, and Grouping</b>.</li> <li><b>Extend the Functorial Data Model to include Richer Constraints, such as Embedded Dependencies/finite-limit theories</b>.</li> <li><b>Extend the Functorial Data Model to include Updates and View-Updates</b></li> <li><b>Extend the Functorial Data Model to include Uncertain Information</b></li> <li><b>Consistency and Conservativity in Functorial Data Migration</b>The Sigma data migration functor, and other related operations, such as pushouts, do not preserve the consistency of their input instances; in logical terms the resulting equational theories need not be conservative extensions of their schemas. The goal of this project is to develop algorithms to detect what an instance presentation is not consistent, and to give proofs of situations when inconsistency cannot arise.</li> <li><b>Excel and FQL Interoperability</b>. In principle spreadsheets have much structure relevant to FQL: each sheet is a table with unique row numbers, cells can reference other cells, mappings can be represented as two column tables, and data integrity constraints represented as formulas. The idea of this project is to import this structure into FQL, or, more speculatively, implement functorial data migration directly in Excel as a macro or extension.</li> </ul>`

Hi @Matthew, my take on

Puzzle 1isBy the way, the third test vector you gave

`interpret (interpret (ifte (bool True) (int 3) (int 4))) == 3`

has an extra call to

`interpret`

.`Hi @Matthew, my take on *Puzzle 1* is instance Language (->) where here (a, _) = a before f (_, h) = f h lambda f h a = f (a, h) apply f g h = f h (g h) loop f h = f h a where a = loop f h int n _ = n add f g h = f h + g h mult f g h = f h * g h down f h = f h - 1 up f h = f h + 1 gte f g h = f h >= g h bool b _ = b and f g h = f h && g h or f g h = f h || g h neg f h = not (f h) ifte b t e h = if b h then t h else e h instance Interpreted (->) where run f h = f h interpret :: Term a -> a interpret t = (run :: (h -> a) -> h -> a) t () By the way, the third test vector you gave `` interpret (interpret (ifte (bool True) (int 3) (int 4))) == 3 `` has an extra call to `interpret`.`

@Matthew I've continued working with my puzzle about the relations between the proofs about adjunctions over posets in the book and implementations of the adjunctions in Haskell.

Exercise 1.91in the book asks us to prove, usingProposition 1.81, that if \(f \dashv g \) then:Let's beging with 1. From the Haskell perspective, this expression is similar to the

`unit`

(a.k.a.`return`

) of a monad.1'.

`unit :: a -> g (f a)`

The proof of 1. is given by reflexivity \( f(p) \le f(p) \) and then adjointness \(p \le (g(f(p)) \)

The implementation of

`unit`

is giving by`unit = leftAdjoint id`

which has exactly the same structure as the proof of 1 (

`id`

is the translation ofreflexivityinto the Haskell domain).Let's return to the 2, which is

\( g(f(g(f(p)))) \cong g(f(p)) \)

We have to prove it in both directions:

2a. \( g(f(g(f(p)))) \le g(f(p)) \)

From 3. we have \( f(g(q)) \le q \); by monotonicity of \( g \) we get \( g(f(g(q))) \le g(q) \); which is valid for all \( q \in Q \) and in particular for \( q = f(p) \) so \( g(f(g(f(p)))) \le g(f(p)) \).

Its Haskell version is the function

`join`

(part of the definition of a monad)2a'.

`join :: g (f (g (f a))) -> g (f a)`

and its implementation

`join :: fmap counit`

2b. \( g(f(p)) \le g(f(g(f(p)))) \)

From 1. we have \( p \le g(f(p)) \); by monotonicity of \( f \) we get \( f(p) \le f(g(f(p))) \); and by monotonicity of \( g \) we get \( g(f(p)) \le g(f(g(f(p)))) \)

Its Haskell version is the

`duplicate'`

function (the name is due that it has the structure of the`duplicate`

function of a comonad)2b'.

`duplicate' :: g (f a) -> g (f (g (f a)))`

and its implementation is given by

`duplicate' = (fmap . fmap) unit`

.A footnote before

Exercise 1.91tells us that we can do the same "the other way round", that is, that we can similarly proveWhich, in the Haskell domain, seems very similar to

`counit`

(a.k.a.`extract`

) in a comonad. I'll omit the proofs because are dual to the ones presented.3'.

`counit :: f (g a) -> a`

and an implementation

`counit = rightAdjoint id`

From the proof of 4 we get

4a'.

`join' :: f (g (f (g a))) -> f (g a)`

and

4b'. `duplicate :: f (g a) -> f (g (f (g a)))

with implementations:

So we have proved that given \(f \dashv g \), \(g \circ f\) is a

monad(with`unit`

and`join`

) and that \(f \circ g\) is acomonad(with`extract`

and`duplicate`

).I don't know if the other two functions,

`join'`

and`duplicate'`

, give any interesting properties to \(f \circ g\) and \(g \circ f\).PS: I haven't proved if the equations which relate

`unit`

and`join`

in a monad (resp.`counit`

and`extract`

in a comonad) follow from their implementations.`@Matthew I've continued working with my puzzle about the relations between the proofs about adjunctions over posets in the book and implementations of the adjunctions in Haskell. *Exercise 1.91* in the book asks us to prove, using *Proposition 1.81*, that if \\(f \dashv g \\) then: 1. \\( p \le g(f(p)) \\) 2. \\( g(f(g(f(p)))) \cong g(f(p)) \\) Let's beging with 1. From the Haskell perspective, this expression is similar to the `unit` (a.k.a. `return`) of a monad. 1'. `unit :: a -> g (f a)` The proof of 1. is given by reflexivity \\( f(p) \le f(p) \\) and then adjointness \\(p \le (g(f(p)) \\) The implementation of `unit` is giving by `unit = leftAdjoint id` which has exactly the same structure as the proof of 1 (`id` is the translation of _reflexivity_ into the Haskell domain). Let's return to the 2, which is \\( g(f(g(f(p)))) \cong g(f(p)) \\) We have to prove it in both directions: 2a. \\( g(f(g(f(p)))) \le g(f(p)) \\) From 3. we have \\( f(g(q)) \le q \\); by monotonicity of \\( g \\) we get \\( g(f(g(q))) \le g(q) \\); which is valid for all \\( q \in Q \\) and in particular for \\( q = f(p) \\) so \\( g(f(g(f(p)))) \le g(f(p)) \\). Its Haskell version is the function `join` (part of the definition of a monad) 2a'. `join :: g (f (g (f a))) -> g (f a)` and its implementation `join :: fmap counit` 2b. \\( g(f(p)) \le g(f(g(f(p)))) \\) From 1. we have \\( p \le g(f(p)) \\); by monotonicity of \\( f \\) we get \\( f(p) \le f(g(f(p))) \\); and by monotonicity of \\( g \\) we get \\( g(f(p)) \le g(f(g(f(p)))) \\) Its Haskell version is the `duplicate'` function (the name is due that it has the structure of the `duplicate` function of a comonad) 2b'. `duplicate' :: g (f a) -> g (f (g (f a)))` and its implementation is given by `duplicate' = (fmap . fmap) unit`. A footnote before *Exercise 1.91* tells us that we can do the same "the other way round", that is, that we can similarly prove 3. \\( f(g(q)) \le q \\) 4. \\( f(g(f(g(q)))) \cong f(g(q)) \\) Which, in the Haskell domain, seems very similar to `counit` (a.k.a. `extract`) in a comonad. I'll omit the proofs because are dual to the ones presented. 3'. `counit :: f (g a) -> a` and an implementation `counit = rightAdjoint id` From the proof of 4 we get 4a'. `join' :: f (g (f (g a))) -> f (g a)` and 4b'. `duplicate :: f (g a) -> f (g (f (g a))) with implementations: join' = (fmap . fmap) counit duplicate = fmap unit So we have proved that given \\(f \dashv g \\), \\(g \circ f\\) is a *monad* (with `unit` and `join`) and that \\(f \circ g\\) is a *comonad* (with `extract` and `duplicate`). I don't know if the other two functions, `join'` and `duplicate'`, give any interesting properties to \\(f \circ g\\) and \\(g \circ f\\). PS: I haven't proved if the equations which relate `unit` and `join` in a monad (resp. `counit`and `extract` in a comonad) follow from their implementations.`

Nice stuff!

Juan wrote:

You seem to have proved all the interesting properties I know. Mathematicians would say that whenever we have a left adjoint functor \(f\) and a right adjoint functor \(g\), the composite \(f \circ g\) is a monad and the composite \(g \circ f\) is a comonad. We are considering the special case where the categories involved are preorders. In this case \(f \circ g\) is always an

idempotent monad, meaning$$ f(g(f(g(q))) \cong f(g(q)) $$ for all \(q\), and similarly \(g \circ f\) is always an

idempotent comonad, meaning$$ g(f(g(f(p))) \cong g(f(p)) $$ for all \(p\). In a preorder these isomorphisms become equations.

An idempotent monad on a preorder is called a

closure operatorbecause the classic example is taking the closure of a subset of a topological space. Similarly, an idempotent comonad on a preorder is calledco-closure operatorand the classic example is taking the interior of a subset of a topological space.`Nice stuff! [Juan wrote](https://forum.azimuthproject.org/discussion/comment/16784/#Comment_16784): > I don't know if the other two functions, `join'` and `duplicate'`, give any interesting properties to \\(f \circ g\\) and \\(g \circ f\\). You seem to have proved all the interesting properties I know. Mathematicians would say that whenever we have a left adjoint functor \\(f\\) and a right adjoint functor \\(g\\), the composite \\(f \circ g\\) is a monad and the composite \\(g \circ f\\) is a comonad. We are considering the special case where the categories involved are preorders. In this case \\(f \circ g\\) is always an **idempotent monad**, meaning $$ f(g(f(g(q))) \cong f(g(q)) $$ for all \\(q\\), and similarly \\(g \circ f\\) is always an **idempotent comonad**, meaning $$ g(f(g(f(p))) \cong g(f(p)) $$ for all \\(p\\). In a preorder these isomorphisms become equations. An idempotent monad on a preorder is called a **[closure operator](https://en.wikipedia.org/wiki/Closure_operator#Closure_operators_on_partially_ordered_sets)** because the classic example is taking the closure of a subset of a topological space. Similarly, an idempotent comonad on a preorder is called **co-closure operator** and the classic example is taking the interior of a subset of a topological space.`

Wow Juan! You skipped past puzzle #1 and answered #2!

My answer to #1 was based on Oleg's lecture notes (page 27):

I later saw the slick solution. You skipped to it right away!

Also, I love these explanations you are giving.

I had a random thought regarding your first puzzle:

Consider

`flip (>>=) :: Monad m => (a -> m b) -> m a -> m b`

. Prelude calls this`(=<<)`

.This is intimately related to the definition of the closure of

`a`

in topology. From Wikipedia:Symbolically:

$$ (a \subseteq cl(b)) \Longrightarrow cl(a) \subseteq cl(b) $$ Every topology gives rise to a preorder, called its

specialization order. I mentioned this in the Chapter 1 thread. And you can recover an isomorphic Alexandrov topology from every preorder. You can also map all of the monotonically increasing functions \(f\) to continuous functions and vice versa. So these topics are related.I think the finally tagless DSL I gave needs some work to properly fit it into Conal Elliot's framework. Also, it's probably best to build up with fragments. I am hoping to start this next week.

`Wow Juan! You skipped past puzzle #1 and answered #2! My answer to #1 was based on Oleg's lecture notes (page 27): <pre> newtype R h a = R {unR :: h -> a} --- ... run e = unR e () </pre> I later saw the slick solution. You skipped to it right away! Also, I love these explanations you are giving. I had a random thought regarding your first puzzle: > *What property of the Galois connection is proved by the implementation of bind `(>>=)` ?* Consider `flip (>>=) :: Monad m => (a -> m b) -> m a -> m b`. Prelude calls this `(=<<)`. This is intimately related to the definition of the closure of `a` in topology. From [Wikipedia](https://en.wikipedia.org/wiki/Closure_(topology)#Definitions): > cl(*S*) is the smallest closed set containing *S* Symbolically: $$ (a \subseteq cl(b)) \Longrightarrow cl(a) \subseteq cl(b) $$ Every topology gives rise to a preorder, called its [*specialization order*](https://en.wikipedia.org/wiki/Specialization_(pre)order). I mentioned this in the Chapter 1 thread. And you can recover an isomorphic [Alexandrov topology](https://en.wikipedia.org/wiki/Alexandrov_topology) from every preorder. You can also map all of the monotonically increasing functions \\(f\\) to continuous functions and vice versa. So these topics are related. ---------------------------------------------------- I think the finally tagless DSL I gave needs some work to properly fit it into Conal Elliot's framework. Also, it's probably best to build up with fragments. I am hoping to start this next week.`

Matthew wrote

I was suspecting that !! My

faultwas not to arrive to page 27 andfeelingthe right type for`l`

;-)Yes, yesterday I also thought about flipping

`>>=`

parameters but I got distracted by monads and comonads :-D.And yes, I think this works because then, if we interpret the type of

`=<<`

in the "preorder language", we get:$$ p \le g(f(p\prime)) => g(f(p)) \le g(f(p\prime)) $$ And this can be proved by:

From \(p \le g(f(p\prime)) \); by monotonicity of both \(f\) and \(g\) we have \( g(f(p)) \le g(f(g(f(p\prime)))) \); and then the isomorphism \( g(f(g(f(p\prime)))) \cong g(f(p\prime)) \) gives us \( g(f(p)) \le g(f(p\prime)) \).

Thanks !!!!

`[Matthew wrote](https://forum.azimuthproject.org/profile/1818/Matthew%20Doty) > You skipped past puzzle #1 and answered #2! I was suspecting that !! My _fault_ was not to arrive to page 27 and _feeling_ the right type for `l` ;-) > Consider `flip (>>=) :: Monad m => (a -> m b) -> m a -> m b` ... Yes, yesterday I also thought about flipping `>>=` parameters but I got distracted by monads and comonads :-D. And yes, I think this works because then, if we interpret the type of `=<<` in the "preorder language", we get: $$ p \le g(f(p\prime)) => g(f(p)) \le g(f(p\prime)) $$ And this can be proved by: From \\(p \le g(f(p\prime)) \\); by monotonicity of both \\(f\\) and \\(g\\) we have \\( g(f(p)) \le g(f(g(f(p\prime)))) \\); and then the isomorphism \\( g(f(g(f(p\prime)))) \cong g(f(p\prime)) \\) gives us \\( g(f(p)) \le g(f(p\prime)) \\). Thanks !!!!`

I don't think such a feat is possible. I get the feeling, that since

Catis Cartesian Closed with Delta morphisms that general Categorical theorem proving might actually be undecidable.The proof is would be simular to the ones given in, A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points.

`>**Implement a Categorical Theorem Prover.** Modern theorem provers for first-order logic are not particularly well-suited for reasoning about categories, which requires purely equational reasoning, empty sorts, ground completeness, and other niche features. The goal of this project is to implement a theorem prover specifically tailored to categorical needs. I don't think such a feat is possible. I get the feeling, that since **Cat** is Cartesian Closed with Delta morphisms that general Categorical theorem proving might actually be undecidable. The proof is would be simular to the ones given in, [ A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points](https://arxiv.org/pdf/math/0305282.pdf).`

In fact. if such a generalized Categorical theorem prover existed, then a generalized Set theorem prover would also exist: simply truncate the result!

No such prover can exist since it would contradict Godel’s First Incompleteness Theorem.

`In fact. if such a generalized Categorical theorem prover existed, then a generalized Set theorem prover would also exist: simply truncate the result! No such prover can exist since it would contradict Godel’s First Incompleteness Theorem.`

@ Keith - I don't think they are asking to make a universal categorical theorem proving

algorithm. They want something like Coq but specially tailored to category theory. The underlying theory for Coq is undecidable too. This is why these proof assistants need a lot of human effort to get them to prove anything significant.While it looks like they want to stay away from FOL, Saul Feferman famously tried to formulate category theory in FOL for nearly 50 years. He built on an alternate formulation of set theory due to Quine called New Foundations. His idea was to use Quine's formulation so he could always have hom-sets and not worry about big categories. Here is a recent review paper of his effort from 2016.

If you wanted to take this approach, it might be something to implement in Isabelle like Paulson's Isabelle/ZF.

But Coq looks good enough for the Homotopy Type Theory research program. I'm a little curious why others aren't satisfied.

`@ Keith - I don't think they are asking to make a universal categorical theorem proving *algorithm*. They want something like Coq but specially tailored to category theory. The underlying theory for Coq is undecidable too. This is why these proof assistants need a lot of human effort to get them to prove anything significant. While it looks like they want to stay away from FOL, Saul Feferman famously tried to formulate category theory in FOL for nearly 50 years. He built on an alternate formulation of set theory due to Quine called [New Foundations](https://en.wikipedia.org/wiki/New_Foundations). His idea was to use Quine's formulation so he could always have hom-sets and not worry about big categories. Here is a [recent review paper](https://arxiv.org/pdf/1603.03272.pdf) of his effort from 2016. If you wanted to take this approach, it might be something to implement in Isabelle like Paulson's [Isabelle/ZF](http://isabelle.in.tum.de/library/ZF/index.html). But Coq looks good enough for the [Homotopy Type Theory](https://homotopytypetheory.org/book/) research program. I'm a little curious why others aren't satisfied.`

@ John: "Interpret Learn Reject. It may be possible for two people with no common ground to nevertheless develop a shared understanding of a domain by repeatedly following a loop that develops a span between schemas."

This sounds intriguing (particularly since I work on game theoretic models of human linguistic coordination strategies) - is there somewhere I could find a little more information on what this means?

`@ John: "Interpret Learn Reject. It may be possible for two people with no common ground to nevertheless develop a shared understanding of a domain by repeatedly following a loop that develops a span between schemas." This sounds intriguing (particularly since I work on game theoretic models of human linguistic coordination strategies) - is there somewhere I could find a little more information on what this means?`

Have any of you cats tried https://blog.jupyter.org/a-diagram-editor-for-jupyterlab-a254121ff919 ?

Should be able to do string diagrams, among other category theory stuff...I haven't tried it yet, looking for experience reports from catsters who have.

`Have any of you cats tried https://blog.jupyter.org/a-diagram-editor-for-jupyterlab-a254121ff919 ? Should be able to do string diagrams, among other category theory stuff...I haven't tried it yet, looking for experience reports from catsters who have.`

Hi Matthew, I've been working on your Puzzle3 and I'm stuck with the last twi pieces:

`run`

and`interpret`

.My code from Conal's paper is this:

And my implementation for

`Language`

and`Interpreted`

is:It compiles, but althougth this is Haskell, maybe there are some errors :-D

Any ideas, hints, comments to advance further in the Puzzle?

Thanks !!!

`Hi [Matthew](https://forum.azimuthproject.org/profile/1818/Matthew%20Doty), I've been working on your [Puzzle3](https://forum.azimuthproject.org/discussion/comment/16735/#Comment_16735) and I'm stuck with the last twi pieces: `run` and `interpret`. My code from Conal's paper is this: {-# LANGUAGE TypeOperators #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleInstances #-} module CompilingToCategories where import Prelude hiding (it, (.), curry, uncurry, const) -- Classes infixr 9 . class Category k where id :: a `k` a (.) :: (b `k` c) -> (a `k` b) -> (a `k` c) infixr 3 |*| class Category k => Cartesian k where (|*|) :: (a `k` c) -> (a `k` d) -> (a `k` (c, d)) exl :: (a, b) `k` a exr :: (a, b) `k` b -- How to generalize () for any category? class Category k => Terminal k where it :: a `k` () class Cartesian k => Closed k where applyC :: ((a -> b), a) `k` b curry :: ((a, b) `k` c) -> (a `k` (b -> c)) uncurry :: (a `k` (b -> c)) -> ((a, b) `k` c) class Terminal k => ConstCat k b where unitArrow :: b -> (() `k` b) const :: ConstCat k b => b -> (a `k` b) const b = unitArrow b . it class Cartesian k => BoolCat k where notC :: Bool `k` Bool andC, orC :: (Bool, Bool) `k` Bool ifteC :: (Bool, (a, a)) `k` a class NumCat k a where negateC :: a `k` a addC, mulC :: (a, a) `k` a class OrdCat k a where gteC :: (a, a) `k` Bool -- Instances instance Category (->) where id = \x -> x g . f = \x -> g (f x) instance Cartesian (->) where f |*| g = \x -> (f x, g x) exl = \(a, b) -> a exr = \(a, b) -> b instance Terminal (->) where it = \a -> () instance Closed (->) where applyC (f, a) = f a curry f = \a b -> f (a, b) uncurry f = \(a, b) -> f a b instance ConstCat (->) b where unitArrow b = \() -> b instance BoolCat (->) where notC = not andC = uncurry (&&) orC = uncurry (||) ifteC = \(b, (t, e)) -> if b then t else e instance Num a => NumCat (->) a where negateC = negate addC = uncurry (+) mulC = uncurry (*) instance Ord a => OrdCat (->) a where gteC = uncurry (>=) And my implementation for `Language` and `Interpreted` is: {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module LanguageCat where import Prelude hiding (it, (.), curry, uncurry, const) import CompilingToCategories import Language -- In the code below -- find a concrete value for `l` -- and elide all the mocks swap :: Cartesian k => (a, b) `k` (b, a) swap = exr |*| exl instance (Closed k ,ConstCat k Int, NumCat k Int, OrdCat k Int ,ConstCat k Bool, BoolCat k ) => Language k where here = exl before f = f . exr lambda f = curry (f . swap) apply f g = applyC . (f |*| g) loop f = applyC . ( f |*| loop f) int = const add a b = addC . (a |*| b) mult a b = mulC . (a |*| b) down a = add a (int (-1)) up a = add a (int 1) gte a b = gteC . (a |*| b) bool = const and a b = andC . (a |*| b) or a b = orC . (a |*| b) neg a = notC . a ifte b t e = ifteC . (b |*| t |*| e) instance (Closed k ,ConstCat k Int, NumCat k Int, OrdCat k Int ,ConstCat k Bool, BoolCat k) => Interpreted k where run = undefined --interpret :: Term a -> a --interpret t = (run :: h `l` a -> h -> a) t () It compiles, but althougth this is Haskell, maybe there are some errors :-D Any ideas, hints, comments to advance further in the Puzzle? Thanks !!!`