#### Howdy, Stranger!

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

Options

# Categories for the Working Hacker - A Discussion Group

edited February 2019

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!

«13

• Options
1.

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.

Comment Source: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.
• Options
2.

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.

Comment Source: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.
• Options
3.
edited March 2018

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 endofunctors as a type class. This type class has two natural transformations: leftAdjunct and rightAdjunct.

{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE Rank2Types             #-}
{-# LANGUAGE TypeOperators          #-}

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


In category theory, this is written as $$f \dashv g$$

In this class, leftAdjunct and rightAdjunct are natural transformations and obey the following laws:

-- leftAdjunct . rightAdjunct === id


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:

-- leftAdjunct counit === id


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 the functor 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)?

Comment Source: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>?
• Options
4.

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

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.

Comment Source: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. 
• Options
5.

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.)

Comment Source: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.)
• Options
6.

Solution to Puzzle 1 Write out the types and then copy them to the term level.

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

Solution to Puzzle 2 This part requires some choices (type unification).

unit :: Adjunction f g => a -> g (f a)
unit = leftAdjunct id

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.

counit :: Adjunction f g => f (g a) -> a
counit = rightAdjunct 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.

Comment Source:<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.
• Options
7.
edited March 2018

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 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 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.

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)...

Comment Source: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)...
• Options
8.
edited April 2018

Scott Fleischman: Thanks for plugging my 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).

Abstract:

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.

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

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.

Questions and comments on these papers are most welcome!

Comment Source: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!
• Options
9.

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.

Comment Source: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.
• Options
10.
edited April 2018

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)
instance (Applicative f, Applicative g) => Applicative (f :.: g)
-- Defined in ‘GHC.Generics’


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

Comment Source: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? 
• Options
11.

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.

Comment Source: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.
• Options
12.

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

Comment Source: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)
• Options
13.

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:

Comment Source: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
• Options
14.

Matthew, thanks a lot.

Comment Source:Matthew, thanks a lot.
• Options
15.

Juan Manuel Gimeno #10 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:

{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE Rank2Types             #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE KindSignatures         #-}
{-# LANGUAGE PolyKinds              #-}
{-# LANGUAGE DeriveFunctor          #-}

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)

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

return = Comp1 . unit
(>>=) = undefined

Comment Source:[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> 
• Options
16.
edited April 2018

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             #-}

class (Functor f, Functor g) => Adjunction f g | f -> g, g -> f where

leftAdjunct  :: (f a -> b) -> a -> g b
leftAdjunct f = fmap f . unit

rightAdjunct :: (a -> g b) -> f a -> b
rightAdjunct f = counit . fmap f

unit :: a -> g (f a)

counit :: f (g a) -> a

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

return  = Comp1 . unit
x >>= f = Comp1 (fmap (rightAdjunct (unComp1 . f)) (unComp1 x))

Comment Source: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)) 
• Options
17.

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.

Comment Source: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. 
• Options
18.
edited April 2018

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.

Comment Source: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.
• Options
19.

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? :)

Comment Source: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? :)
• Options
20.

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

Comment Source:Personally I prefer 4 but, as I often work on my laptop, usually I use only two :-D
• Options
21.

2 for me!

Comment Source:2 for me!
• Options
22.
edited April 2018

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)

Comment Source: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)
• Options
23.

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

Comment Source: 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? 
• Options
24.

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

Comment Source: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
• Options
25.

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

Comment Source: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.
• Options
26.

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

Comment Source:Thanks Juan, I tried to read through the Typeclassopedia once but did find it too terse so I'll check out that other book.
• Options
27.
edited April 2018

@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 μ?

Comment Source:@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 μ?
• Options
28.

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.

Comment Source: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. 
• Options
29.
edited April 2018

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 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 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:

$$\mu f := \bigvee_{\sqsubseteq} \left\{ \underbrace{f(f(f(\cdots(f}_n(\bot)\cdots))) \ :\ n\in \mathbb{N} \right\}$$

...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 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 $$\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 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}}$$]

Comment Source: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}}\$$]
• Options
30.
edited April 2018

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))


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))

Comment Source: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)) 
• Options
31.
edited April 2018

@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))...]

Comment Source:@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))...]
• Options
32.
edited April 2018

@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). 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.

Comment Source:@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.
• Options
33.

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.

Comment Source: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.
• Options
34.
edited April 2018

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 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. 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 .

{-# 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
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 ()


\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:

interpret (apply (lambda here) (int 6)) == 6

interpret (apply (lambda here) (bool True)) == True

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


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.

Comment Source: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)
• Options
35.

@Mathew In the definition

interpret t = run t ()

GHC complains with

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

Comment Source:@Mathew In the definition  interpret t = run t ()  GHC complains with  Variable not in scope: run :: r0 h0 a -> () -> a  
• Options
36.

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?

Comment Source: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?
• Options
37.
edited April 2018

@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.

Comment Source:@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.
• Options
38.

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.

Comment Source: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.
• Options
39.
edited April 2018

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 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 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 Uncertain Information
• Consistency 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.
Comment Source: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> 
• Options
40.

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.

Comment Source: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.
• Options
41.
edited April 2018

@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).

$$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

1. $$f(g(q)) \le q$$
2. $$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. counitand extract in a comonad) follow from their implementations.

Comment Source:@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. counitand extract in a comonad) follow from their implementations. 
• Options
42.
edited April 2018

Nice stuff!

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 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.

Comment Source: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.
• Options
43.
edited April 2018

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

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

newtype R h a = R {unR :: h -> a}

--- ...

run e = unR e ()



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

Also, I love these explanations you are giving.

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:

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. 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.

Comment Source: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.
• Options
44.
edited April 2018

Matthew wrote

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 !!!!

Comment Source:[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 !!!!
• Options
45.

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.

Comment Source:>**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).
• Options
46.

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.

Comment Source: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.
• Options
47.
edited April 2018

@ 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.

Comment Source:@ 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.
• Options
48.

@ 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?

Comment Source:@ 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?
• Options
49.

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.

Comment Source: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.
• Options
50.
edited April 2018

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:

{-# 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
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
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

Comment Source: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 !!!