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

- All Categories 2.2K
- Applied Category Theory Course 356
- Applied Category Theory Seminar 4
- Exercises 149
- Discussion Groups 50
- How to Use MathJax 15
- Chat 482
- Azimuth Code Project 108
- News and Information 145
- Azimuth Blog 149
- Azimuth Forum 29
- Azimuth Project 189
- - Strategy 108
- - Conventions and Policies 21
- - Questions 43
- Azimuth Wiki 711
- - Latest Changes 701
- - - Action 14
- - - Biodiversity 8
- - - Books 2
- - - Carbon 9
- - - Computational methods 38
- - - Climate 53
- - - Earth science 23
- - - Ecology 43
- - - Energy 29
- - - Experiments 30
- - - Geoengineering 0
- - - Mathematical methods 69
- - - Meta 9
- - - Methodology 16
- - - Natural resources 7
- - - Oceans 4
- - - Organizations 34
- - - People 6
- - - Publishing 4
- - - Reports 3
- - - Software 21
- - - Statistical methods 2
- - - Sustainability 4
- - - Things to do 2
- - - Visualisation 1
- General 41

## Comments

Hey Juan!

Actually, I got side tracked with thinking about something you asked in another thread.

I wanted to share because I'm sort of proud of this wackiness, but I'll get back to working through Conal's paper soon!

In Lecture 9 - Chapter 1: Adjoints and the Logic of Subsets

Oh,

`_|_`

is just me trying to be cute and represent \(\bot\). The symbol \(\bot\) denotes \(\bigvee\{\}\) or "the minimal element in a preorder".David Hilbert derived this rule in his essay The Foundations of Mathematics (1927). It is the first consequence he gives after stating his 12 axioms.

Philosophers also call this rule

ex falso (sequiter) quadlibetin Latin andThe Principle Of Pseudo-Scotus.Now that we have

`Bottom`

(I prefer`Falsum`

so I will use that), we can plug it into John's definition of negation, and combine it with Glivenko's Theorem.This gives us a

monadin Haskell which re-purposes Haskell's type checker as a simple proof checker for classical logic!I will be following Hilbert's formalism for logic.

Haskell lacks

impredicative polymorphismsadly. This means if we want to do anything fancy with the type system we have to box stuff all over the place.The first thing to note is that John's negation gives rise to a

contravariantfunctor, which is a functor with a rule`contramap :: (a -> b) -> f b -> f a`

. This map has an old name in logic - contraposition$$ \vdash (\phi \to \psi) \to (\neg \psi \to \neg \phi) $$ Here's how we construct it:

I also like to use the unboxed version of contraposition:

We have enough to start with the

Classical Logic Theorem MonadThe first thing to show is that this is a

functor. Here is the instance:Next, we want to show it is an

Applicative. The`pure`

operation reflects that intuitionistic logic (captured by the`Identity`

functor in Haskell, as per the celebrated Curry-Howard correspondence) is a sublogic of classical logic.Apply

`<*>`

for this monad reflects the rule philosophers traditionally callmodus ponens:$$ \vdash \phi \to \psi \Longrightarrow\; \vdash \phi \Longrightarrow \; \vdash \psi $$ My instance uses the unboxed definitions for

`Classical`

, which are given by:Here's the applicative instance:

Along with

modus ponens, classical logic has several axioms. The axiomatization varies amongst logicians, but one system commonly used is:$$ \begin{eqnarray} & \vdash \phi \to \psi \to \phi & \\ & \vdash (\phi \to \psi \to \chi) \to (\phi \to \psi) \to \phi \to \chi & \\ & \vdash \neg \neg \phi \to \phi \end{eqnarray} $$ And we can indeed construct and check proofs for all three axioms.

The first two correspond to the

KandScombinators, which are`pure`

and`<*>`

for the`(->) e`

functor. See Conor McBride'sIdioms: applicative programming with effects(2009) for a discussion of this.Finally, what's left is to show \(\vdash \neg\neg \phi \to \phi\). I like to follow Dirk van Dalen's presentation on page 159 of Logic and Structure (2013).

First, we can write

`unApply`

, which is the inverse of`(<*>)`

:We can then use it and the intuitionistic identity \(\neg \neg \neg \phi \to \neg \phi\) to prove the final axiom:

All that's left to show is that this is

`Monad`

. This isn't super hard, but I'll leave it as an exercise for anyone reading who wants to try...`Hey Juan! Actually, I got side tracked with thinking about something you asked in another thread. I wanted to share because I'm sort of proud of this wackiness, but I'll get back to working through Conal's paper soon! ---------------------------------------- In [Lecture 9 - Chapter 1: Adjoints and the Logic of Subsets](https://forum.azimuthproject.org/discussion/comment/16866/#Comment_16866) > @Matthew, I don't know if I have understood exactly what you meant with `_|_`, but my answer is this: > <pre> type Bottom = forall t. t hilbertExplosion :: Bottom -> a hilbertExplosion bottom = id bottom </pre> Oh, `_|_` is just me trying to be cute and represent \\(\bot\\). The symbol \\(\bot\\) denotes \\(\bigvee\\{\\}\\) or "the [minimal element](https://en.wikipedia.org/wiki/Maximal_and_minimal_elements) in a preorder". > Why is it called `hilbertExplosion`? David Hilbert derived this rule in his essay [The Foundations of Mathematics (1927)](https://www.marxists.org/reference/subject/philosophy/works/ge/hilbert.htm). It is the first consequence he gives after stating his 12 axioms. Philosophers also call this rule *ex falso (sequiter) quadlibet* in Latin and *The Principle Of Pseudo-Scotus*. Now that we have `Bottom` (I prefer `Falsum` so I will use that), we can plug it into John's definition of negation, and combine it with [Glivenko's Theorem](https://plato.stanford.edu/entries/logic-intuitionistic/#TraClaIntLog). This gives us a *monad* in Haskell which re-purposes Haskell's type checker as a simple proof checker for classical logic! I will be following Hilbert's formalism for logic. Haskell lacks [*impredicative polymorphism*](https://ghc.haskell.org/trac/ghc/wiki/ImpredicativePolymorphism) sadly. This means if we want to do anything fancy with the type system we have to box stuff all over the place. <pre> {-# LANGUAGE Rank2Types #-} module Classical where newtype Falsum = Falsum { efq :: forall a . a } -- `efq` stands for *ex falso quodlibet* -- John Baez's definition of negation newtype Not a = Not { unNot :: a -> Falsum } </pre> The first thing to note is that John's negation gives rise to a *contravariant* functor, which is a functor with a rule `contramap :: (a -> b) -> f b -> f a`. This map has an old name in logic - [contraposition](https://en.wikipedia.org/wiki/Contraposition) $$ \vdash (\phi \to \psi) \to (\neg \psi \to \neg \phi) $$ Here's how we construct it: <pre> contraposition :: (a -> b) -> Not b -> Not a contraposition = (flip . curry . (Not .) . uncurry . ((.) .)) unNot </pre> I also like to use the unboxed version of contraposition: <pre> contraposition' :: (a -> b) -> (b -> Falsum) -> a -> Falsum contraposition' = (flip . curry . uncurry) (.) </pre> We have enough to start with the *Classical Logic Theorem Monad* <pre> newtype Classical a = Thm { getProof :: Not (Not a) } </pre> The first thing to show is that this is a *functor*. Here is the instance: <pre> instance Functor Classical where fmap = ( flip . curry . (Thm .) . uncurry . (flip (contraposition . contraposition) .) ) getProof </pre> Next, we want to show it is an *Applicative*. The `pure` operation reflects that intuitionistic logic (captured by the `Identity` functor in Haskell, as per the celebrated [Curry-Howard correspondence](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence)) is a sublogic of classical logic. Apply `<*>` for this monad reflects the rule philosophers traditionally call *modus ponens*: $$ \vdash \phi \to \psi \Longrightarrow\; \vdash \phi \Longrightarrow \; \vdash \psi $$ My instance uses the unboxed definitions for `Classical`, which are given by: <pre> toDoubleNeg :: Classical a -> (a -> Falsum) -> Falsum toDoubleNeg = flip (flip (unNot . getProof) . Not) fromDoubleNeg :: ((a -> Falsum) -> Falsum) -> Classical a fromDoubleNeg = Thm . Not . contraposition' unNot </pre> Here's the applicative instance: <pre> instance Applicative Classical where pure = Thm . Not . flip unNot (<*>) = ( curry . (fromDoubleNeg .) . uncurry . (. toDoubleNeg) . flip . (. toDoubleNeg) . (contraposition' .) . flip . (contraposition' .) . flip ) contraposition' </pre> Along with *modus ponens*, classical logic has several axioms. The axiomatization varies amongst logicians, but one system commonly used is: $$ \begin{eqnarray} & \vdash \phi \to \psi \to \phi & \\\\ & \vdash (\phi \to \psi \to \chi) \to (\phi \to \psi) \to \phi \to \chi & \\\\ & \vdash \neg \neg \phi \to \phi \end{eqnarray} $$ And we can indeed construct and check proofs for all three axioms. The first two correspond to the [**K** and **S** combinators](https://en.wikipedia.org/wiki/SKI_combinator_calculus), which are `pure` and `<*>` for the `(->) e` functor. See Conor McBride's [*Idioms: applicative programming with effects* (2009)](http://www.staff.city.ac.uk/~ross/papers/Applicative.html) for a discussion of this. <pre> ax1 :: Classical (a -> b -> a) ax1 = pure const -- or `ax1 = pure const` ax2 :: Classical ((a -> b -> c) -> (a -> b) -> a -> c) ax2 = pure (<*>) -- or `ax2 = pure (\f x -> f x x)` </pre> Finally, what's left is to show \\(\vdash \neg\neg \phi \to \phi\\). I like to follow Dirk van Dalen's presentation on page 159 of [Logic and Structure (2013)](https://www.researchgate.net/file.PostFileLoader.html?id=5518f022d5a3f25c318b4611&assetKey=AS%3A273746110156809%401442277566498). First, we can write `unApply`, which is the inverse of `(<*>)`: <pre> unApply :: (Classical a -> Classical b) -> Classical (a -> b) unApply = ( fromDoubleNeg . ((<*>) (<*>) ((<*>) pure)) . ( curry . flip ) ( ( flip . uncurry . flip . (flip ($) .) ) (. (efq .)) . (. pure) ) ) . (toDoubleNeg .) . (. fromDoubleNeg) </pre> We can then use it and the intuitionistic identity \\(\neg \neg \neg \phi \to \neg \phi\\) to prove the final axiom: <pre> ax3 :: Classical ((Not (Not a)) -> a) ax3 = (. (toDoubleNeg . Thm)) <$> unApply ( fromDoubleNeg . flip ((flip ($)) . toDoubleNeg . pure) . toDoubleNeg) </pre> All that's left to show is that this is `Monad`. This isn't super hard, but I'll leave it as an exercise for anyone reading who wants to try...`

Matthew, after sleeping over my problem I think I've arrived at the solution of creating an intance of Interpret for the function (->) category which gets its Language instance from the general category one.

So, getting both

`run`

and`interpret`

for the (->) instance Tagless Puzzle 2, the code for (->) is simply:I've tested over the same examples that worked over the direct implementation of

`Language (->)`

and these work:But I have problems with:

I've needed to add FlexibleContexts because it complained with this:

and after adding it, the type I get is

But now, when I try

I get

And this is all I have.

PS: The

`Monad Classical`

Puzzle will have to wait for now :-)`[Matthew](https://forum.azimuthproject.org/profile/1818/Matthew%20Doty), after sleeping over my problem I think I've arrived at the solution of creating an intance of Interpret for the function (->) category which gets its Language instance from the general category one. So, getting both `run` and `interpret`for the (->) instance [Tagless Puzzle 2](https://forum.azimuthproject.org/discussion/comment/16735/#Comment_16735), the code for (->) is simply: {-# LANGUAGE Rank2Types #-} module LanguageFun2 where import CompilingToCategories import Language import LanguageCat instance Interpreted (->) where run f h = f h interpret :: Term a -> a interpret t = (run :: (h -> a) -> h -> a) t () I've tested over the same examples that worked over the direct implementation of `Language (->)` and these work: interpret (apply (lambda here) (int 6)) interpret (apply (lambda here) (bool True)) interpret (ifte (bool True) (int 3) (int 4)) But I have problems with: ex = lambda (lambda (add (before here) here)) I've needed to add FlexibleContexts because it complained with this: • Non type-variable argument in the constraint: ConstCat k Bool (Use FlexibleContexts to permit this) • When checking the inferred type ex :: forall h (k :: * -> * -> *). (BoolCat k, ConstCat k Bool, ConstCat k Int, OrdCat k Int, NumCat k Int, Closed k) => k h (Int -> Int -> Int) and after adding it, the type I get is ex :: (BoolCat k, ConstCat k Bool, ConstCat k Int, OrdCat k Int, NumCat k Int, Closed k) =>k h (Int -> Int -> Int) But now, when I try interpret (apply (apply ex (int 3)) (int 2)) I get • Could not deduce (BoolCat k) arising from a use of ‘ex’ from the context: Language k bound by a type expected by the context: Language k => k h Int at <playground>:5:1-44 Possible fix: add (BoolCat k) to the context of a type expected by the context: Language k => k h Int • In the first argument of ‘apply’, namely ‘ex’ In the first argument of ‘apply’, namely ‘(apply ex (int 3))’ In the first argument of ‘interpret’, namely ‘(apply (apply ex (int 3)) (int 2))’ And this is all I have. PS: The [`Monad Classical` Puzzle](https://forum.azimuthproject.org/discussion/comment/16975/#Comment_16975) will have to wait for now :-)`

I am not 100%, but I think the issue is you've got some functional dependencies in your classes.

First, I would generalize

`()`

for`Terminal`

like this:The reason I think we can do this is that terminal objects for a category are all

isomorphic, so we can treat whatever instance we make as uniquely determined.Also here:

I don't think you need a

`b`

parameter for`ConstCat`

... instead, I would do:In fact, we can generalize

`ConstCat k u`

and get rid of the`u`

parameter.Observe:

So we can just do:

Sorry if this doesn't compile... :-(

If you want, we make a repo on github so I can pull your code down. That might be easier for us and others who want to join in to communicate code as things get more complicated.

`> Matthew, after sleeping over my problem I think I've arrived at the solution of creating an instance of Interpret for the function `(->)` category which gets its Language instance from the general category one. > > ... > > But I have problems with: > ><code>ex = lambda (lambda (add (before here) here))</code> I am not 100%, but I think the issue is you've got some [functional dependencies](https://wiki.haskell.org/Functional_dependencies) in your classes. First, I would generalize `()` for `Terminal` like this: <pre> class Category k => Terminal k u | k -> u where it :: a `k` u </pre> The reason I think we can do this is that terminal objects for a category are all *isomorphic*, so we can treat whatever instance we make as uniquely determined. Also here: <pre> class Terminal k => ConstCat k b where unitArrow :: b -> (() `k` b) </pre> I don't think you need a `b` parameter for `ConstCat`... instead, I would do: <pre> class Terminal k u => ConstCat k u | k -> u where unitArrow :: b -> (u `k` b) </pre> In fact, we can generalize `ConstCat k u` and get rid of the `u` parameter. Observe: <pre> constArrow :: ConstCat k u => b -> a `k` b constArrow b = (unitArrow b) . it </pre> So we can just do: <pre> class ConstCat k where constArrow :: b -> (a `k` b) </pre> Sorry if this doesn't compile... :-( If you want, we make a repo on github so I can pull your code down. That might be easier for us and others who want to join in to communicate code as things get more complicated.`

Hi Matthew,

The git repository is created at categories-working-hacker.

The last commit includes both your suggestions and an the modified interpreter.

I can enter in

`ghci`

the expression`ex = lambda (lambda (add (before here) here))`

only if I enable`:seti -XFlexibleContexts`

But when I try to evaluate

`interpret (apply (apply ex (int 3)) (int 2))`

I get the error:I hope the project (using stack) is well configured because I use haskellformac and my

stack-fuis a little bit rusty.`Hi [Matthew](https://forum.azimuthproject.org/profile/1818/Matthew%20Doty), The git repository is created at [categories-working-hacker](https://github.com/jmgimeno/categories-working-hacker). The last commit includes both your suggestions and an the modified interpreter. I can enter in `ghci` the expression `ex = lambda (lambda (add (before here) here))` only if I enable `:seti -XFlexibleContexts` But when I try to evaluate `interpret (apply (apply ex (int 3)) (int 2))` I get the error: <interactive>:4:25: error: • Could not deduce (BoolCat k) arising from a use of ‘ex’ from the context: Language k bound by a type expected by the context: Term Int at <interactive>:4:1-44 Possible fix: add (BoolCat k) to the context of a type expected by the context: Term Int • In the first argument of ‘apply’, namely ‘ex’ In the first argument of ‘apply’, namely ‘(apply ex (int 3))’ In the first argument of ‘interpret’, namely ‘(apply (apply ex (int 3)) (int 2))’ I hope the project (using stack) is well configured because I use haskellformac and my _stack-fu_ is a little bit rusty.`

@Juan,

Okay, I made a test suite and as long as everything is type annotated it looks like this is compiling fine.

I also turned on a bunch of linting and warnings. If you would prefer I can turn them back off.

I see two ways forward from here:

`CategoryFix`

with`fixC :: (y -> y) `k` y`

.Finally, there's a few more adjunction identities I can think of if you are still curious about that!

`@[Juan](https://forum.azimuthproject.org/profile/2083/Juan%20Manuel%20Gimeno), Okay, I made a test suite and as long as everything is type annotated it looks like this is compiling fine. I also turned on a bunch of linting and warnings. If you would prefer I can turn them back off. I see two ways forward from here: 1. Pick a compile target outside of Haskell. For instance LLVM or WASM are cool. We'll have to modify the category classes to suite doing this I think. I suspect there's a few other classes left to be made. In particular, I think we need something like `CategoryFix` with <code>fixC :: (y -> y) `k` y</code>. 2. Move on to the automatic integration paper Finally, there's a few more adjunction identities I can think of if you are still curious about that!`

@Matthew,

what a pull request !!! Most of the code was in need for a cleanup (mainly due to the fact that sometimes I was 'playing by ear', because my knowledge of Haskell is medium-plus at most).

I think that you're referring to "The simple essence of automatic differentiation" paper, aren't you?

After having read over it, the paper mentions "monoidal categories". As the second chapter of the "Seven Sketches" book is about "monoidal preorders", maybe exploring both things in parallel can make sense, don't you think? (Although, I haven't finished the "Compiling to Categories" paper yet)

I'm completely open to new adjunction identities. Adjunctions, at least for me, were a hard wall to smash my head into two years ago. Completely impenetrable. And now, I think, I'm beginning to make a little dent on them. So anything about adjunctions is more than welcome.`@Matthew, what a pull request !!! Most of the code was in need for a cleanup (mainly due to the fact that sometimes I was 'playing by ear', because my knowledge of Haskell is medium-plus at most). I think that you're referring to "The simple essence of automatic differentiation" paper, aren't you? After having read over it, the paper mentions "monoidal categories". As the second chapter of the "Seven Sketches" book is about "monoidal preorders", maybe exploring both things in parallel can make sense, don't you think? (Although, I haven't finished the "Compiling to Categories" paper yet) **I'm completely open to new adjunction identities**. Adjunctions, at least for me, were a hard wall to smash my head into two years ago. Completely impenetrable. And now, I think, I'm beginning to make a little dent on them. So anything about adjunctions is more than welcome.`

Yeah mine is pretty mediocre too. I'm trying to practice every day.

Sounds good.

Okay, so suppose \(g \dashv f\). Then we have the following little theorem I lifted from this mathematics stack exchange discussion:

In other words \(g( a \vee b ) = g(a) \vee g(b)\) and \( f(a \wedge b) = f(a) \wedge f(b)\).

Puzzle: In Haskell, we can think of these two equations as four functions. What are they? How relaxed can we make the type class constraints?`> what a pull request !!! Most of the code was in need for a cleanup (mainly due to the fact that sometimes I was 'playing by ear', because my knowledge of Haskell is medium-plus at most). Yeah mine is pretty mediocre too. I'm trying to practice every day. > After having read over it, the paper mentions "monoidal categories". As the second chapter of the "Seven Sketches" book is about "monoidal preorders", maybe exploring both things in parallel can make sense, don't you think? (Although, I haven't finished the "Compiling to Categories" paper yet) Sounds good. > **I'm completely open to new adjunction identities.** Okay, so suppose \\(g \dashv f\\). Then we have the following little theorem I lifted from this [mathematics stack exchange discussion](https://math.stackexchange.com/a/825966): > **Theorem**: Left adjoints preserve all joins; right adjoints preserve all meets. In other words \\(g( a \vee b ) = g(a) \vee g(b)\\) and \\( f(a \wedge b) = f(a) \wedge f(b)\\). **Puzzle**: In Haskell, we can think of these two equations as four functions. What are they? How relaxed can we make the type class constraints?`

Juan wrote:

Monoidal categories - categories where you can multiply objects and morphisms - are pretty fundamental to mathematics. Just as preorders are a special case of categories, monoidal preorders are a special case of monoidal categories.

Seven Sketchesis highly unorthodox in that it discussses preorders and monoidal preorders before turning to more general categories and monoidal categories. But with luck, by the end, you'll be experts on all these things!`Juan wrote: > After having read over it, the paper mentions "monoidal categories". As the second chapter of the _Seven Sketches_ book is about "monoidal preorders", maybe exploring both things in parallel can make sense, don't you think? Monoidal categories - categories where you can multiply objects and morphisms - are pretty fundamental to mathematics. Just as preorders are a special case of categories, monoidal preorders are a special case of monoidal categories. _Seven Sketches_ is highly unorthodox in that it discussses preorders and monoidal preorders before turning to more general categories and monoidal categories. But with luck, by the end, you'll be experts on all these things!`

Hi @Matthew, here's my take on the puzzle:

I've created two classes, one for each preservation property

And then two implementations: (I've needed to add the extentions FlexibleInstances and UndecidableInstances)

Both

`introduceCoproduct`

and`extractProduct`

only need`f`

(or`g`

) to be functors, so they can be put into another instance with a less strong condition.Function

`introduceProduct`

is the uncurried version of`f a -> f b -> f (a, b)`

which can be found in the monoidal presentation forapplicative functors.The last one,

`extractCoproduct`

, I cannot relate with anything I know (besides being the dual of the "monoidal" one).And that's all (for now ;-D)

`Hi @Matthew, here's my take on the puzzle: I've created two classes, one for each preservation property class PreservesCoproduct f where extractCoproduct :: f (Either a b) -> Either (f a) (f b) introduceCoproduct :: Either (f a) (f b) -> f (Either a b) class PreservesProduct f where extractProduct :: f (a, b) -> (f a, f b) introduceProduct :: (f a, f b) -> f (a, b) And then two implementations: (I've needed to add the extentions FlexibleInstances and UndecidableInstances) instance Adjunction f g => PreservesCoproduct f where extractCoproduct = rightAdjunct $ fmap Left . unit ||| fmap Right . unit introduceCoproduct = fmap Left ||| fmap Right instance Adjunction f g => PreservesProduct g where extractProduct = fmap fst &&& fmap snd introduceProduct = leftAdjunct $ counit . fmap fst &&& counit . fmap snd Both `introduceCoproduct` and `extractProduct` only need `f`(or `g`) to be functors, so they can be put into another instance with a less strong condition. Function `introduceProduct` is the uncurried version of `f a -> f b -> f (a, b)` which can be found in the [monoidal presentation](https://en.wikibooks.org/wiki/Haskell/Applicative_functors#The_monoidal_presentation) for **applicative functors**. The last one, `extractCoproduct`, I cannot relate with anything I know (besides being the dual of the "monoidal" one). And that's all (for now ;-D)`

Hmm... let me say my thinking. Taking what you just wrote, we actually have:

These reflect that, for every monotone \(f\):

$$ \begin{eqnarray} f(a) \vee f(b) & \leq & f(a \vee b) \\ f(a \wedge b) & \leq & f(a) \wedge f(b) \\ \end{eqnarray} $$

The Galois connections in Fong and Spivak are defined to be between two preorders \(\leq_A\) and \(\leq_B\).

On the other hand, Ed Kmett's adjunctions are always between

`Category (->)`

and`Category (->)`

.This restricts us from looking at one of the cutest adjunction constructions I know.

If we have a MonadIt's a classic construction. I don't think it's in Fong and Spivak :( It is at the heart of the`m`

, we compute two adjunctions!`>=>`

operator in Haskell if you've ever used it.However, I think I know why Kmett came up his adjunctions library the way he did. He has

anotheradjunction construction he came up with 10 years ago. But his is all in`Category (->)`

.I can talk about these if you like.

`Hmm... let me say my thinking. Taking what you just wrote, we actually have: <pre> introduceCoproduct :: Functor f => Either (f a) (f b) -> f (Either a b) introduceCoproduct = fmap Left ||| fmap Right extractProduct :: f (a, b) -> (f a, f b) extractProduct = fmap fst &&& fmap snd </pre> These reflect that, for every monotone \\(f\\): $$ \begin{eqnarray} f(a) \vee f(b) & \leq & f(a \vee b) \\\\ f(a \wedge b) & \leq & f(a) \wedge f(b) \\\\ \end{eqnarray} $$ ------------------------------------- The Galois connections in Fong and Spivak are defined to be between two preorders \\(\leq_A\\) and \\(\leq_B\\). On the other hand, Ed Kmett's adjunctions are always between `Category (->)` and `Category (->)`. This restricts us from looking at one of the cutest adjunction constructions I know. *If we have a Monad `m`, we compute two adjunctions!* It's a classic construction. I don't think it's in Fong and Spivak :( It is at the heart of the `>=>` operator in Haskell if you've ever used it. However, I think I know why Kmett came up his adjunctions library the way he did. He has *another* adjunction construction he came up with 10 years ago. But his is all in `Category (->)`. I can talk about these if you like.`

Actually, could someone make an implementation that takes a preorder and gives a visualization of it? A visualizer would be useful for authors and teachers (plus anyone else that likes visual proofs).

In fact, why not make a whole library that implements preorders and their various operations?

`Actually, could someone make an implementation that takes a preorder and gives a visualization of it? A visualizer would be useful for authors and teachers (plus anyone else that likes visual proofs). In fact, why not make a whole library that implements preorders and their various operations?`

I understand >=> to be composition of morphisms in the Kleisli category of the relevant monad. But how does >=> relate to adjunctions?

`> This restricts us from looking at one of the cutest adjunction constructions I know. If we have a Monad m, we compute two adjunctions! It's a classic construction. I don't think it's in Fong and Spivak It is at the heart of the >=> operator in Haskell if you've ever used it. I understand >=> to be composition of morphisms in the Kleisli category of the relevant monad. But how does >=> relate to adjunctions?`

Matthew wrote:

I guess you're talking about the adjunctions involving the Kleisli and Eilenberg-Moore categories. Reuben mentioned one of these.

I find these names incredibly intimidating given how simple the ideas are. In particular, the "Eilenberg-Moore category", with the longer and more intimidating name, is arguably the simpler idea. A bunch of us like to call the Eilenberg-Moore category of a monad the

category of algebrasof the monad, and the Kleisli category thecategory of free algebrasof the monad.`Matthew wrote: > If we have a Monad `m`, we compute two adjunctions! I guess you're talking about the adjunctions involving the Kleisli and Eilenberg-Moore categories. Reuben mentioned one of these. I find these names incredibly intimidating given how simple the ideas are. In particular, the "Eilenberg-Moore category", with the longer and more intimidating name, is arguably the simpler idea. A bunch of us like to call the Eilenberg-Moore category of a monad the **category of algebras** of the monad, and the Kleisli category the **category of free algebras** of the monad.`

@Matthew,

You've piqued my curiosity.

`@Matthew, > This restricts us from looking at one of the cutest adjunction constructions I know. If we have a Monad m, we compute two adjunctions! It's a classic construction. I don't think it's in Fong and Spivak **It is at the heart of the >=> operator in Haskell** if you've ever used it. > However, I think I know why Kmett came up his adjunctions library the way he did. He has another adjunction construction he came up with 10 years ago. But his is all in Category (->). > I can talk about these if you like. You've piqued my curiosity.`

Hi @Matthew, in #57 you translate "right adjoints preserve meets" as if saying "preserve the meet operation", but Proposition 1.84 goes beyond, saying that they preserve even the meet of an arbitrary set of elements (not just two). That code starts to take shape, wish I knew some Haskell.

`Hi @Matthew, in [#57](https://forum.azimuthproject.org/discussion/comment/17071/#Comment_17071) you translate "right adjoints preserve meets" as if saying "preserve the meet operation", but Proposition 1.84 goes beyond, saying that they preserve even the meet of an arbitrary set of elements (not just two). That code starts to take shape, wish I knew some Haskell.`

I'd love a reference to materials explaining the "Eilenberg-Moore category", as explanations I've found are incredibly difficult (especially compared to the Kleisli category, which from a programming perspective is very straightforward to understand). Unless that's going to be covered in this course, in which case I can wait!

`> I find these names incredibly intimidating given how simple the ideas are. I'd love a reference to materials explaining the "Eilenberg-Moore category", as explanations I've found are incredibly difficult (especially compared to the Kleisli category, which from a programming perspective is very straightforward to understand). Unless that's going to be covered in this course, in which case I can wait!`

Okay guys, I'll try this.

The following was first established in by Kleisli in

Every standard construction is induced by a pair of adjoint functors(1965)I am going to leave a bunch of puzzles so others can finish the construction.

Let's start with the boilerplate.

The

`Category`

typeclass is defined in`Control.Category`

in base. It introduces`id`

and`(.)`

, which correspond to identity morphisms and morphism composition from category theory.We diverge from the

`Prelude`

below. In traditional category theory, afunctormaps morphisms in one Category into another. The following typeclass captures this.This leads to the first puzzle:

Puzzle 1. What are the laws for CatFunctor? [Hint: They should be familiar...]An

endofunctoris a functor from a category to itself.Haskell's

`Functor`

is a particular kind of endofunctor. It's on the category`(->)`

, which is something calledHask.This is operationally equivalent to the

`Functor`

in base. Here are the two instances:So now we are ready for talking about adjunctions. In category theory, we say two functors \(F: \mathcal{X} \to \mathcal{Y}\) and \(G: \mathcal{Y} \to \mathcal{X}\) are adjoint whenever there is a family of bijections such that:

This is captured with this typeclass:

The usual Haskell adjunctions are just with endofunctors on

`(->)`

.So now to the actualy adjoint constructions. From

`Control.Arrow`

, there is the followingcategorydefined:Puzzle 2. Fill out the category instance for`Kleisli m`

below. You can always cheat if you want, but maybe don't share?Finally, we can construct the adjunction. The

leftadjoint is free and doesn't depend on anything:Puzzle 3. (the hard one) The right adjoint isnotfree.`newtype`

declaration for it.`CatFunctor (Kleisli m) ??? (->)`

for it`Monad m => CatAdjunction (->) (Kleisli m) LeftK ???`

I am free to give hints to Puzzle 3. It might help after we finish it to see what this means for posets...

`Okay guys, I'll try this. The following was first established in by Kleisli in [*Every standard construction is induced by a pair of adjoint functors* (1965)](http://www.ams.org/journals/proc/1965-016-03/S0002-9939-1965-0177024-4/) I am going to leave a bunch of puzzles so others can finish the construction. Let's start with the boilerplate. <pre> {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE MonoLocalBinds #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} module CatAdjunctions where import Control.Category import Control.Monad ((<=<)) -- Hint! import Prelude hiding ((.)) </pre> The `Category` typeclass is defined in [`Control.Category`](https://hackage.haskell.org/package/base-4.11.0.0/docs/Control-Category.html) in base. It introduces `id` and `(.)`, which correspond to identity morphisms and morphism composition from category theory. We diverge from the `Prelude` below. In traditional category theory, a *functor* maps morphisms in one Category into another. The following typeclass captures this. <pre> class (Category x, Category y) => CatFunctor x f y where catMap :: a `x` b -> f a `y` f b </pre> This leads to the first puzzle: **Puzzle 1**. What are the laws for CatFunctor? [Hint: They should be familiar...] An *endofunctor* is a functor from a category to itself. <pre> type EndoFunctor k f = CatFunctor k f k </pre> Haskell's `Functor` is a particular kind of endofunctor. It's on the category `(->)`, which is something called **Hask**. <pre> type HaskFunctor f = EndoFunctor (->) f </pre> This is operationally equivalent to the `Functor` in base. Here are the two instances: <pre> instance Functor f => CatFunctor (->) f (->) where catMap = undefined -- Needs UndecidableInstances and -fno-warn-orphans instance EndoFunctor (->) f => Functor f where fmap = undefined </pre> So now we are ready for talking about adjunctions. In category theory, we say two functors \\(F: \mathcal{X} \to \mathcal{Y}\\) and \\(G: \mathcal{Y} \to \mathcal{X}\\) are adjoint whenever there is a family of bijections such that: <center>![](https://latex.codecogs.com/gif.latex?%5Cmathbf%7Bhom%7D_%7B%5Cmathcal%7BY%7D%7D%28FA%2CB%29%20%5Ccong%20%5Cmathbf%7Bhom%7D_%7B%5Cmathcal%7BX%7D%7D%28A%2CGB%29)</center> This is captured with this typeclass: <pre> class ( CatFunctor x f y , CatFunctor y g x ) => CatAdjunction x y f g where catLeftAdjunct :: (f a `y` b) -> (a `x` g b) catRightAdjunct :: (a `x` g b) -> (f a `y` b) </pre> The usual Haskell adjunctions are just with endofunctors on `(->)`. So now to the actualy adjoint constructions. From [`Control.Arrow`](https://hackage.haskell.org/package/base-4.11.0.0/docs/Control-Arrow.html#g:1), there is the following *category* defined: <pre> newtype Kleisli m a b = Kleisli { runKleisli :: a -> m b } </pre> **Puzzle 2**. Fill out the category instance for `Kleisli m` below. You can always cheat if you want, but maybe don't share? <pre> instance Monad m => Category (Kleisli m) where id = undefined (.) = undefined -- This should be familiar... </pre> Finally, we can construct the adjunction. The *left* adjoint is free and doesn't depend on anything: <pre> newtype LeftK a = LeftK { unLeftK :: a } instance Applicative m => CatFunctor (->) LeftK (Kleisli m) where catMap = Kleisli . (pure .) . haskCatMap where haskCatMap f (LeftK x) = LeftK (f x) </pre> **Puzzle 3**. (the hard one) The right adjoint is **not** free. 1. Write the `newtype` declaration for it. 2. Write the instance `CatFunctor (Kleisli m) ??? (->)` for it 3. Finally, write the instance for `Monad m => CatAdjunction (->) (Kleisli m) LeftK ???` ------------------------------------------------ I am free to give hints to Puzzle 3. It might help after we finish it to see what this means for posets...`

Reuben wrote:

I don't know what's best, but the Eilenberg-Moore category of a monad is the category of "algebras" of a monad, so you should probably start by getting a good understanding of the algebras of a monad. To mathematicians, the most important thing about monads is their algebras: we describe mathematical structures as algebras of monads.

This might help:

This is part of a series of videos by some friends of mine; it might be best to start at the beginning:

`Reuben wrote: > I'd love a reference to materials explaining the "Eilenberg-Moore category", as explanations I've found are incredibly difficult (especially compared to the Kleisli category, which from a programming perspective is very straightforward to understand). I don't know what's best, but the Eilenberg-Moore category of a monad is the category of "algebras" of a monad, so you should probably start by getting a good understanding of the algebras of a monad. To mathematicians, the most important thing about monads is their algebras: we describe mathematical structures as algebras of monads. This might help: * The Catsters, [Monads 3](https://www.youtube.com/watch?v=eBQnysX7oLI). This is part of a series of videos by some friends of mine; it might be best to start at the beginning: * The Catsters, [Monads 1](https://www.youtube.com/watch?v=9fohXBj2UEI&list=PL0E91279846EC843E).`

@Matthew,

the

boilerplatecode in Kleisli puzzle finishes abrupty with`import Control.Monad ((`

, so I think there are some lines missing.I've also needed to change

`Applicative m`

to`Monad m`

because it is needed for`Keisli m`

to be a 'Category'.Would you mind revising it?

`@Matthew, the _boilerplate_ code in [Kleisli puzzle](https://forum.azimuthproject.org/discussion/comment/17174/#Comment_17174) finishes abrupty with `import Control.Monad ((`, so I think there are some lines missing. I've also needed to change`Applicative m` to `Monad m` because it is needed for `Keisli m` to be a 'Category'. Would you mind revising it?`

@Matthew,

this is my take on the puzzles so far:

Puzzle1 solution:are thefunctor lawsexpressed in Category class terms:Puzzle2 solution:islifting`return`

and`>=>`

from`Monad`

to the`Kleisli`

newtype:Puzzle3 solution:1 and 2 are related because I need the`RighK`

values to be in the same monad context as the kleisli arrowsWhat I'm stuck with is the last part of the puzzle. I think I have the correct code but I cannot to make GHC to accept it. The code I have is:

And the error I get has to do with functional dependencies:

Any suggestions?

Of course the problem can be that all my code is completely wrong :-D

`@Matthew, this is my take on the puzzles so far: **Puzzle1 solution:** are the *functor laws* expressed in Category class terms: catMap id = id catMap (f . g) = catMap f . catMap g **Puzzle2 solution:** is _lifting_ `return`and `>=>` from `Monad`to the `Kleisli` newtype: instance Monad m => Category (Kleisli m) where id = Kleisli return (Kleisli f) . (Kleisli g) = Kleisli $ f <=< g **Puzzle3 solution:** 1 and 2 are related because I need the `RighK` values to be in the same monad context as the kleisli arrows newtype RightK m b = RightK { unRightK :: m b } instance Monad m => CatFunctor (Kleisli m) (RightK m) (->) where catMap (Kleisli f) (RightK a) = RightK $ a >>= f What I'm stuck with is the last part of the puzzle. I think I have the correct code but I cannot to make GHC to accept it. The code I have is: instance Monad m => CatAdjunction (->) (Kleisli m) LeftK (RightK m) where catLeftAdjunct f = RightK . f . LeftK catRightAdjunct f = unRightK . f . unLeftK And the error I get has to do with functional dependencies: • Illegal instance declaration for ‘CatAdjunction (->) (Kleisli m) LeftK (RightK m)’ The liberal coverage condition fails in class ‘CatAdjunction’ for functional dependency: ‘f -> g’ Reason: lhs type ‘LeftK’ does not determine rhs type ‘RightK m’ Un-determined variable: m • In the instance declaration for ‘CatAdjunction (->) (Kleisli m) LeftK (RightK m)’ Any suggestions? Of course the problem can be that all my code is completely wrong :-D`

First guesses maybe:

Puzzle 1

Puzzle 2

I didn't understand what not sharing meant?

ACT has already given me much of the stuff I've wanted for years. Especially many thanks MD and JGM for these incredible lessons :).

(Gone for breakfast!)

`First guesses maybe: Puzzle 1 > catMap x f y = catMap x f catMap y? Puzzle 2 > id = return ()? > (.) = something to do with (=<<)? I didn't understand what not sharing meant? ACT has already given me much of the stuff I've wanted for years. Especially many thanks MD and JGM for these incredible lessons :). (Gone for breakfast!)`

@Juan -

Okay, I fixed it. It should read:

You figured it out without the hint of course... next time I promise to make a PR.

For the

`CatFunctor`

instance for`LeftK`

, all it needs it that`m`

be an applicative, since it just calls`pure`

and doesn't use bind in any way. But I see now that's confusing.Okay, it's my bad again. There shouldn't be any functional dependencies in

`CatAdjunction`

(we are going to have to give types for everything like it's Java sadly).You are very close. You just need to fix the definition you gave for`catRightAdjunct`

.`[@Juan](https://forum.azimuthproject.org/profile/2083/Juan%20Manuel%20Gimeno) - > the _boilerplate_ code in [Kleisli puzzle](https://forum.azimuthproject.org/discussion/comment/17174/#Comment_17174) finishes abrupty with `import Control.Monad ((`, so I think there are some lines missing. > I've also needed to change`Applicative m` to `Monad m` because it is needed for `Keisli m` to be a 'Category'. > Would you mind revising it? Okay, I fixed it. It should read: <pre> import Control.Category import Control.Monad ((<=<)) -- Hint! import Prelude hiding ((.)) </pre> You figured it out without the hint of course... next time I promise to make a PR. > I've also needed to change`Applicative m` to `Monad m` because it is needed for `Keisli m` to be a 'Category'. For the `CatFunctor` instance for `LeftK`, all it needs it that `m` be an applicative, since it just calls `pure` and doesn't use bind in any way. But I see now that's confusing. > The code I have is: > > <pre> instance Monad m => CatAdjunction (->) (Kleisli m) LeftK (RightK m) where catLeftAdjunct f = RightK . f . LeftK catRightAdjunct f = unRightK . f . unLeftK </pre> > And the error I get has to do with functional dependencies: > > <pre> • Illegal instance declaration for ‘CatAdjunction (->) (Kleisli m) LeftK (RightK m)’ The liberal coverage condition fails in class ‘CatAdjunction’ for functional dependency: ‘f -> g’ Reason: lhs type ‘LeftK’ does not determine rhs type ‘RightK m’ Un-determined variable: m • In the instance declaration for ‘CatAdjunction (->) (Kleisli m) LeftK (RightK m)’ </pre> Okay, it's my bad again. There shouldn't be any functional dependencies in `CatAdjunction` (we are going to have to give types for everything like it's Java sadly). <pre> class ( CatFunctor x f y , CatFunctor y g x ) => CatAdjunction x y f g where catLeftAdjunct :: (f a `y` b) -> (a `x` g b) catRightAdjunct :: (a `x` g b) -> (f a `y` b) </pre> -------------------------------------------- **You are very close**. You just need to fix the definition you gave for `catRightAdjunct`.`

@Jim,

to exclude the . from importing from the Prelude, you neews two pairs of parentheses

`import Prelude hiring ((.))`

`@Jim, to exclude the . from importing from the Prelude, you neews two pairs of parentheses `import Prelude hiring ((.))``

@Jim -

For puzzle 1, the laws for

`CatFunctor`

should be the same as the laws for`Functor`

. It needs to preserve`id`

and`(.)`

. In traditional Haskell, the laws are:For puzzle 2, we always bump up against Haskell's lack of

impredicative typeswhen we want to do fancy stuff like this.Morphisms in the Kleisli category for a monad

`m`

look like:`a -> m b`

So if

`\ a -> a :: a -> a`

is the identity for`(->)`

, what's the identity for`Kleisli m`

?Also, with regard to category composition

`(.)`

, I have a hint. They call`(<=<)`

in`Control.Monad`

the "right-to-left Kleisli composition", named after the paper I cited.`[@Jim](https://forum.azimuthproject.org/profile/328/Jim%20Stuttard) - For puzzle 1, the laws for `CatFunctor` should be the same as the laws for `Functor`. It needs to preserve `id` and `(.)`. In traditional Haskell, the laws are: <pre> fmap id = id fmap (f . g) = (fmap f) . (fmap g) </pre> For puzzle 2, we always bump up against Haskell's lack of [*impredicative types*](https://wiki.haskell.org/Impredicative_types) when we want to do fancy stuff like this. Morphisms in the Kleisli category for a monad `m` look like: <center><code> a -> m b</code></center> So if `\ a -> a :: a -> a` is the identity for `(->)`, what's the identity for `Kleisli m`? Also, with regard to category composition `(.)`, I have a hint. They call [`(<=<)`](http://hackage.haskell.org/package/base-4.11.0.0/docs/Control-Monad.html#v:-60--61--60-) in `Control.Monad` the "right-to-left Kleisli composition", named after the paper I cited.`

@Matthew,

after taking away the functional dependencies, and changing the definitions of both adjunctions (

`catLeftAdjunct`

was missing a`runKleisli`

) I have finally got:By the way, as

`LeftK`

is the just the`Identity`

and`RightK m`

is just`m`

functor, I think one can simplifypuzzle 3to:And that's all (I think).

`@Matthew, after taking away the functional dependencies, and changing the definitions of both adjunctions (`catLeftAdjunct` was missing a `runKleisli`) I have finally got: instance Monad m => CatAdjunction (->) (Kleisli m) LeftK (RightK m) where catLeftAdjunct f = RightK . runKleisli f . LeftK catRightAdjunct f = Kleisli $ unRightK . f . unLeftK By the way, as `LeftK` is the just the `Identity` and `RightK m` is just `m` functor, I think one can simplify **puzzle 3** to: newtype Identity a = Identity { runIdentity :: a } -- I do not use Data.Functor.Identity because its functor instance -- overlaps with the EndoFunctor's one. instance Monad m => CatFunctor (->) Identity (Kleisli m) where catMap = Kleisli . (pure .) . fmap instance Monad m => CatFunctor (Kleisli m) m (->) where catMap (Kleisli f) ma = ma >>= f instance Monad m => CatAdjunction (->) (Kleisli m) Identity m where catLeftAdjunct f = runKleisli f . Identity catRightAdjunct f = Kleisli $ f . runIdentity And that's all (I think).`

Great job Juan! I saw that

`LeftK`

was just`Identity`

but I didn't think to pull it out of mtl and see the symmetry you did!Here's what I have been thinking about where to go next:

So, we have enough now to do the dual adjunction to

`(,) e`

\(\dashv\)`(->) e`

. Keith Peterson talked about it in another thread. We have`???`

\(\dashv\)`(->) e`

, but the adjunction isnotinHask. It's in a new category based on`Classical`

.Other than that there's still Ed Kmett's construction, which I think is what inspired him to make the

`adjunctions`

library in the first place. This is all purely inHask.Finally, I would love to resume digging through Conal's paper, since I am excited to try to apply his machine learning stuff!

`Great job Juan! I saw that `LeftK` was just `Identity` but I didn't think to pull it out of mtl and see the symmetry you did! Here's what I have been thinking about where to go next: - So, we have enough now to do the dual adjunction to `(,) e` \\(\dashv\\) `(->) e`. Keith Peterson talked about it in another thread. We have `???` \\(\dashv\\) `(->) e`, but the adjunction is *not* in **Hask**. It's in a new category based on `Classical`. - Other than that there's still Ed Kmett's construction, which I think is what inspired him to make the `adjunctions` library in the first place. This is all purely in **Hask**. - Finally, I would love to resume digging through Conal's paper, since I am excited to try to apply his machine learning stuff!`

@Matthew,

Thanks !! I'll push all the code to the repository. If I have time today, I'll try to do some reading, because I'm getting behind with the papers.

`@Matthew, Thanks !! I'll push all the code to the repository. If I have time today, I'll try to do some reading, because I'm getting behind with the papers.`

Hi everyone, I'm very excited to see so many interesting things in this thread! I'd like to add one thing to the mix, which is my attempt at implementation of @Conal's "Simple essence of automatic differentiation" in Haskell, since I see you're talking about it here!

Although most of the code is already in the paper, my implementation is still a work in progress. I'm new to category theory so I'm mostly reading about the concepts before writing the code. I welcome any feedback!

Couple of notes:

reverse-mode autodiff machine learningview of the world. Chapter 12 seems to talk about a way to solve this but I'm struggling to understand it how it can be solved without inverting the (a->b) function!`Hi everyone, I'm very excited to see so many interesting things in this thread! I'd like to add one thing to the mix, which is my attempt at [implementation](https://github.com/bgavran/Backprop_as_Functor/blob/master/src/simple_essence_ad.hs) of @Conal's "Simple essence of automatic differentiation" in Haskell, since I see you're talking about it here! Although most of the code is already in the paper, my implementation is still a work in progress. I'm new to category theory so I'm mostly reading about the concepts before writing the code. I welcome any feedback! Couple of notes: * The paper defines several new datatypes to be instances of classes such as Category, Monoidal, Cartesian and Cocartesian. For all of those except the Control.Category, I've defined my own instances. I do see that Haskell already has those other typeclasses defined but I haven't figured out how to define all the typeclases it requires (the definitions get more abstract as I follow the dependency chain) * In the paper, the Cocartesian typeclass requires only the Category typeclass, but shouldn't it require Monoidal as well, since we're using the monoidal product in the definition? * I'm still confused about the newtype D. I was convinced it should have the opposite way of defining derivative: b -> a instead of a -> b, since that's how I internalized it in my *reverse-mode autodiff machine learning* view of the world. Chapter 12 seems to talk about a way to solve this but I'm struggling to understand it how it can be solved without inverting the (a->b) function!`

@BrunoGavranovic,

We wanted to finish up Conal's Compiling to Categories paper before moving on to automatic differentiation. The reverse-mode autodiff stuff has some overlap with Fong and Spivak's Chapter 2 as they both tackle related concepts.

I can try and read the automatic differentiation paper now, if you like. But could you post the code in particular you are wondering about so I can know what to focus on when I read?

`[@BrunoGavranovic](https://forum.azimuthproject.org/profile/1852/BrunoGavranovic), We wanted to finish up Conal's [Compiling to Categories](http://conal.net/papers/compiling-to-categories/) paper before moving on to automatic differentiation. The reverse-mode autodiff stuff has some overlap with Fong and Spivak's Chapter 2 as they both tackle related concepts. I can try and read the automatic differentiation paper now, if you like. But could you post the code in particular you are wondering about so I can know what to focus on when I read?`

@Matthew,

I'm reading Conal's Compiling to Categories, and I've found some differences in how we represent functions in

`Language k`

.For instance, we have:

But Conal, to represent functions has (page 1:4 of the extended version):

And the representation of neg is then:

(IMHO this seems more natural, because to represent functions we use exponentials objects in the category.)

I don't know if this difference can be significative for what lays ahead.

`@Matthew, I'm reading Conal's Compiling to Categories, and I've found some differences in how we represent functions in `Language k`. For instance, we have: neg :: h `k` Bool -> h `k` Bool neg a = notC . a But Conal, to represent functions has (page 1:4 of the extended version): constFun :: Closed k => (a `k` b) -> (z `k` (a -> b)) constFun f = curry (f . exr) And the representation of neg is then: neg :: h `k` (Bool -> Bool) neg = constFun notC (IMHO this seems more natural, because to represent functions we use exponentials objects in the category.) I don't know if this difference can be significative for what lays ahead.`

@Matthew,

sure, that makes sense. Perhaps it's better to leave all autodiff discussion for after the Compiling to Categories is implemented, so there is less clutter in the thread.

`@Matthew, sure, that makes sense. Perhaps it's better to leave all autodiff discussion for after the Compiling to Categories is implemented, so there is less clutter in the thread.`

By the way: if you guys start working on a project, it makes plenty of sense to start a new discussion thread devoted to that project. It's easy to do.

`By the way: if you guys start working on a project, it makes plenty of sense to start a new discussion thread devoted to that project. It's easy to do.`

@Reuben : I wrote a blog post about Eilenberg-Moore categories and T-algebras, which might be more approachable. https://bartoszmilewski.com/2017/03/14/algebras-for-monads/

`@Reuben : I wrote a blog post about Eilenberg-Moore categories and T-algebras, which might be more approachable. https://bartoszmilewski.com/2017/03/14/algebras-for-monads/`

Functional programming is great, and I'm a huge fan -- but is there any interesting work on representing imperative languages categorically? Everyone and their grandma apparently knows that the simply-typed lambda calculus is the internal language of cartesian closed categories, but what about something like a simple Forth? I haven't had much luck looking for material on the semantics and theory of Forth, so I assume I've been looking in the wrong places (or using the wrong keywords).

`Functional programming is great, and I'm a huge fan -- but is there any interesting work on representing imperative languages categorically? Everyone and their grandma apparently knows that the simply-typed lambda calculus is the internal language of cartesian closed categories, but what about something like a simple Forth? I haven't had much luck looking for material on the semantics and theory of Forth, so I assume I've been looking in the wrong places (or using the wrong keywords).`

@Jonathan,

maybe in A Foundation for Typed Concatenative Languages you'll find some references of your interest.

`@Jonathan, maybe in [A Foundation for Typed Concatenative Languages](https://www2.ccs.neu.edu/racket/pubs/dissertation-kleffner.pdf) you'll find some references of your interest.`

Another reference is Kirby’s Theory of Concatenative Combinators.

Reading over this and Kleffner’s thesis Juan linked (its only 36 pages long) I’m a bit puzzled how to tease a category out. From Juan’s thesis the type signatures of concatenative combinators always seem to have some side condition.

I think it might be that you could model concatenative languages with a Kleisli category, but that feels like cheating.

`Another reference is Kirby’s [Theory of Concatenative Combinators](http://tunes.org/~iepos/joy.html). Reading over this and Kleffner’s thesis Juan linked (its only 36 pages long) I’m a bit puzzled how to tease a category out. From Juan’s thesis the type signatures of concatenative combinators always seem to have some side condition. I think it might be that you could model concatenative languages with a Kleisli category, but that feels like cheating.`

@Bartosz Thanks! I've been reading your blog for a while - it's really excellent!

`@Bartosz Thanks! I've been reading your blog for a while - it's really excellent!`

Joseph Goguen's book Algebraic Semantics of Imperative Programs is "a self-contained and novel 'executable' introduction to formal reasoning about imperative programs." The author writes that it "does not explicitly use category theory, but almost everything in it was inspired in one way or another by category theory."

Goguen's homepage has more about the OBJ language family (and a lot of other very interesting topics).

`Joseph Goguen's book [Algebraic Semantics of Imperative Programs](https://mitpress.mit.edu/books/algebraic-semantics-imperative-programs) is "a self-contained and novel 'executable' introduction to formal reasoning about imperative programs." The author [writes](https://www.mta.ca/~cat-dist/catlist/1999/book-goguen) that it "does not explicitly use category theory, but almost everything in it was inspired in one way or another by category theory." Goguen's homepage has more about the [OBJ language family](http://cseweb.ucsd.edu/~goguen/sys/obj.html) (and a lot of other very interesting topics).`

Jonathan wrote:

Yes, but what people often forget is that cartesian closed categories don't formalize what's really

interestingabout the simply-typed lambda calculus, namely that it can be seen as a simple programming language.The problem is that we get a morphism in a cartesian closed category from an

equivalence classof terms-in-context, where two terms related by beta or eta reduction are considered equal. Thus, a program that huff and puffs and adds 2 and 3, and one that simply prints out 5 count asthe same morphism!So, even in this "well-understood" case, the relation between category theory and programming has not been worked out in detail.

I began trying to deal with this problem in the winter of 2007 when Mike Stay started working with me. Now he's helping run the company Pyrofex, and I'm working with him and my new student Christian Williams to tackle this issue.

A good approach would also handle imperative languages. I will have to read Goguen's book.

`Jonathan wrote: > Everyone and their grandma apparently knows that the simply-typed lambda calculus is the internal language of cartesian closed categories [...] Yes, but what people often forget is that cartesian closed categories don't formalize what's really _interesting_ about the simply-typed lambda calculus, namely that it can be seen as a simple programming language. The problem is that we get a morphism in a cartesian closed category from an _equivalence class_ of terms-in-context, where two terms related by beta or eta reduction are considered equal. Thus, a program that huff and puffs and adds 2 and 3, and one that simply prints out 5 count as _the same morphism!_ So, even in this "well-understood" case, the relation between category theory and programming has not been worked out in detail. I began trying to deal with this problem in [the winter of 2007](http://math.ucr.edu/home/baez/qg-winter2007/index.html#computation) when Mike Stay started working with me. Now he's helping run the company [Pyrofex](https://johncarlosbaez.wordpress.com/2018/02/04/pyrofex/), and I'm working with him and my new student Christian Williams to tackle this issue. A good approach would also handle imperative languages. I will have to read Goguen's book.`

Conal Elliott: Could you briefly explain the universal property in section 2 of Compiling to Categories? I don't understand the syntax of the formula given, notably the "double vee":

`vh. h v f v g v v exl v h v f v exr v h v g`

`Conal Elliott: Could you briefly explain the universal property in section 2 of Compiling to Categories? I don't understand the syntax of the formula given, notably the "double vee": `vh. h v f v g v v exl v h v f v exr v h v g``

We've had lectures on manufacturing, and chemistry + scheduling, but how about manufacturing and scheduling?

Manufacturing has 3 layers. In terms of Chapter 2, they are Recipe, Schedule (Plan in the diagram below), and Reality (what happened) or Observations (what was reported about what happened). And all three layers are similar, in parallel, and interconnected top to bottom to top. The Schedule is generated from the Recipe, and Reality tries to follow the Schedule, but often fails.

How would all those relationships be represented in Category Theory? I'd be happy with hand-wavy pointers or full solutions, but don't expect full solutions.

`We've had lectures on manufacturing, and chemistry + scheduling, but how about manufacturing and scheduling? Manufacturing has 3 layers. In terms of Chapter 2, they are Recipe, Schedule (Plan in the diagram below), and Reality (what happened) or Observations (what was reported about what happened). And all three layers are similar, in parallel, and interconnected top to bottom to top. The Schedule is generated from the Recipe, and Reality tries to follow the Schedule, but often fails. How would all those relationships be represented in Category Theory? I'd be happy with hand-wavy pointers or full solutions, but don't expect full solutions. ![salsa layers](https://raw.githubusercontent.com/valueflows/valueflows/master/release-doc-in-process/process-layer.png)`

Since your question is not mainly about programming, Bob, I might be able to help you with it, and I'm surprised to find it here rather than our discussion of "resource theories".

It's a bit late now, so I'm not up to a detailed analysis right this minute, but the way it would work is that I'd grill you and force you to state your ideas very precisely and translate them into category theory.

If the Schedule is generated in a systematic way from the Plan we might have a functor or other systematic thing going on. It's harder for math to capture relationships where something "tries but often fails", but there are various ways to do it.

On a much simpler level, I've explained:

Petri nets and (equivalently) reaction networks for processes in which resources are combined to give other resources,

Linear programming for helping figure out how to maximize a linear function given linear constraints, and

PERT charts for scheduling.

But in fact all three are different fragments of a unified structure: a

timed Petri net. I'll explain this in a week or so.So, while I probably don't yet know how to do what you want, there's more to the story than I've managed to explain so far.

`Since your question is not mainly about programming, Bob, I might be able to help you with it, and I'm surprised to find it here rather than our discussion of "resource theories". It's a bit late now, so I'm not up to a detailed analysis right this minute, but the way it would work is that I'd grill you and force you to state your ideas very precisely and translate them into category theory. If the Schedule is generated in a systematic way from the Plan we might have a functor or other systematic thing going on. It's harder for math to capture relationships where something "tries but often fails", but there are various ways to do it. On a much simpler level, I've explained: 1. Petri nets and (equivalently) reaction networks for processes in which resources are combined to give other resources, 2. Linear programming for helping figure out how to maximize a linear function given linear constraints, and 3. PERT charts for scheduling. But in fact all three are different fragments of a unified structure: a **timed Petri net**. I'll explain this in a week or so. So, while I probably don't yet know how to do what you want, there's more to the story than I've managed to explain so far.`

Thanks, John. I didn't know where to put it. Seemed beyond where we were at in chapter 2. And I do code this stuff. See https://hillside.net/plop/plop97/Proceedings/haugen.pdf

I'm open to being grilled, but am very slow to read and write the mathematical notation so far (don't have a good math background), so it might be better to wait for your timed petri net explanation and see what it does for me.

`Thanks, John. I didn't know where to put it. Seemed beyond where we were at in chapter 2. And I do code this stuff. See https://hillside.net/plop/plop97/Proceedings/haugen.pdf I'm open to being grilled, but am very slow to read and write the mathematical notation so far (don't have a good math background), so it might be better to wait for your timed petri net explanation and see what it does for me.`

Okay, why don't you wait until we're done with Chapter 2 on Friday May 25th and then post questions/comments on some relevant-seeming lecture.

My questions will mainly be trying to precisely figure out what you mean; often such questions make people get precise about things they'd left vague before, or at least see where the regions of vagueness lie.

`Okay, why don't you wait until we're done with Chapter 2 on Friday May 25th and then post questions/comments on some relevant-seeming lecture. My questions will mainly be trying to precisely figure out what you mean; often such questions make people get precise about things they'd left vague before, or at least see where the regions of vagueness lie.`

Will do. I have running code being used by real people for everything I am thinking about, so it can all be as precise as the code, but the code is not yet categorized, so will not be precise in that sense.

`Will do. I have running code being used by real people for everything I am thinking about, so it can all be as precise as the code, but the code is not yet categorized, so will not be precise in that sense.`

What do you write in?

`> I have running code being used by real people for everything I am thinking about, so it can all be as precise as the code, but the code is not yet categorized, so will not be precise in that sense. What do you write in?`

Mostly Python.

`> What do you write in? Mostly Python.`

Great - if you've got code, I won't wind up saying "hmm, that could be a nice idea if you made it precise". At worst we'll wind up saying "hmm, it would be nice if either I understood your code better or you could talk to me using more category theory".

`Great - if you've got code, I won't wind up saying "hmm, that could be a nice idea if you made it precise". At worst we'll wind up saying "hmm, it would be nice if either I understood your code better or you could talk to me using more category theory".`

When you wind up on chapter 2, I will devote some concentrated time to be able to talk to y'all using category theory + code and we'll see where it goes. Figure it will take me a week after May 25, so I will commit to be ready June 4, and will post something wherever you want it that you will be welcome to destruct.

`When you wind up on chapter 2, I will devote some concentrated time to be able to talk to y'all using category theory + code and we'll see where it goes. Figure it will take me a week after May 25, so I will commit to be ready June 4, and will post something wherever you want it that you will be welcome to destruct.`

Work in progress, produced by python code and http://www.cytoscape.org/ :

Eventually this could go in Ignoring Externalities but the discussion there was so focused I thought it would be disruptive right now. (And I am ignoring egg yolk and egg white for now, too.)

`Work in progress, produced by python code and http://www.cytoscape.org/ : ![eggs to compost](https://user-images.githubusercontent.com/117439/40447738-303ec846-5e99-11e8-953f-2be02a9a0272.png) Eventually this could go in [Ignoring Externalities](https://forum.azimuthproject.org/discussion/2105/lecture-28-chapter-2-ignoring-externalities) but the discussion there was so focused I thought it would be disruptive right now. (And I am ignoring egg yolk and egg white for now, too.)`