[Haskell-cafe] The mother of all functors/monads/categories

[Max Bolingbroke]

I'm wondering if someone can cast some light on a pattern I've come
across, which I'm calling the "mother of all X" pattern after Dan
Piponi's blog post
(http://blog.sigfpe.com/2008/12/mother-of-all-monads.html). Edward
Kmett has also explored these ideas here:
http://www.mail-archive.com/haskell-***@haskell.org/msg57738.html

Preliminaries
===

Q: What is the "mother of all X", where X is some type class?

lift :: X d => d a -> D a
lower :: X d => D a -> d a
instance X D

With *no superclass constraints*.

3. (We may also add the constraint that D is somehow the "smallest
such" data type, but I don't know in exactly what sense I mean this).

So the "mother of all X" is a data type that somehow encodes all of
the functions that the X type class gives you.

An example is in order!


Example 1: Yoneda is the mother of all Functors
===

The code in this example and the next one is shamelessly stolen from

-- flip fmap :: forall a. f a -> (forall b. (a -> b) -> f b)
newtype Yoneda f a = Yoneda { runYoneda :: forall b. (a -> b) -> f b }

And the injections. As it turns out, we don't need the Functor

liftYoneda :: Functor f => f a -> Yoneda f a
liftYoneda f = Yoneda (flip fmap f)
lowerYoneda :: Yoneda f a -> f a
lowerYoneda f = runYoneda f id

Finally, we can write the Functor instance. Notice that we don't need
to make use of the Functor instance for f: all of the methods of
Functor f have been somehow encoded into the Yoneda data type!

instance Functor (Yoneda f) where
fmap f m = Yoneda (\k -> runYoneda m (k . f))

Note that we can also write an instance (Y f => Y (Yoneda f)) for any
Functor subclass Y. But (Yoneda f) is not the mother of all Y, because

instance Applicative f => Applicative (Yoneda f) where
pure = liftYoneda . pure
mf <*> mx = liftYoneda (lowerYoneda mf <*> lowerYoneda mx)

Why is (Yoneda f) interesting? Because if I take some expression whose
type is quantified over any superclass of Functor, and we want to run
it with Functor instantiated to some F, if we instead run it with
Functor instantiated to (Yoneda f) and then use lowerYoneda, we will
automatically get guaranteed fmap fusion.


Example 2: Codensity is the mother of all Monads
===

-- (>>=) :: forall a. m a -> (forall b. (a -> m b) -> m b)
newtype Codensity m a = Codensity { runCodensity :: forall b. (a -> m b) -> m b }
liftCodensity :: Monad m => m a -> Codensity m a
liftCodensity m = Codensity ((>>=) m)
lowerCodensity :: Monad m => Codensity m a -> m a
lowerCodensity m = runCodensity m return
instance Functor (Codensity f) where
fmap f m = Codensity (\k -> runCodensity m (k . f))
instance Applicative (Codensity f) where
pure x = Codensity (\k -> k x)
mf <*> mx = Codensity (\k -> runCodensity mf (\f -> runCodensity mx (\x -> k (f x))))
instance Monad (Codensity f) where
return = pure
m >>= k = Codensity (\c -> runCodensity m (\a -> runCodensity (k a) c))

Again, using (Codensity m) where you used m before can yield a
performance improvement, notably in the case of free monads. See
http://haskell.org/haskellwiki/Performance/Monads or
http://wwwtcs.inf.tu-dresden.de/~voigt/mpc08.pdf.


Example 3: Wotsit is the mother of all Categories
===

I don't actually know what the right name for this data type is, I

-- (>>>) :: forall a b. t a b -> (forall c. t b c -> t a c)
newtype Wotsit t a b = Wotsit { runWotsit :: forall c. t b c -> t a c }
liftWotsit :: Category t => t a b -> Wotsit t a b
liftWotsit t = Wotsit ((>>>) t)
lowerWotsit :: Category t => Wotsit t a b -> t a b
lowerWotsit t = runWotsit t id
instance Category (Wotsit t) where
id = Wotsit id
t1 . t2 = Wotsit (runWotsit t2 . runWotsit t1)

This is *strongly* reminiscent of normalisation-by-evaluation for
monoids (reassociation realised by assocativity of function
application), which is not surprising because Category is just a
monoid. There is probably some connection between NBE and Yoneda (e.g.
"Normalization and the Yoneda embedding", but I can't get access to
this paper electronically).


Conclusion
===

So I have a lot of questions about this stuff:

1. Is there a way to mechanically derive the "mother of all X" from
the signature of X? Are these all instances of a single categorical
framework?
2. Is there a mother of all idioms? By analogy with the previous three

-- (<**>) :: forall a. i a -> (forall b. i (a -> b) -> i b)
newtype Thingy i a = Thingy { runThingy :: forall b. i (a -> b) -> i b }

But I can't see how to write either pure or <*> with that data type.

newtype Thingy i a = Thingy { runThingy :: forall b. Yoneda i (a -> b) -> i b }

Because you can write pure (pure x = Thingy (\k -> lowerYoneda (fmap
($ x) k))). But <*> still eludes me!

3. Since (Codensity m) enforces >>= associativity, perhaps it can be
used to define correct-by-construction monads in the style of
operational or MonadPrompt?

Any insight offered would be much appreciated :-)

Cheers,
Max

[Max Bolingbroke]

By the way, you can use this stuff to solve the restricted monad
problem (e.g. make Set an instance of Monad). This is not that useful
until we find out what the mother of all MonadPlus is, though, because
we really need a MonadPlus Set instance.

Code below.

Cheers,
Max

\begin{code}
{-# LANGUAGE RankNTypes #-}
import Control.Applicative

import Data.Set (Set)
import qualified Data.Set as S


newtype CodensityOrd m a = CodensityOrd { runCodensityOrd :: forall b.
Ord b => (a -> m b) -> m b }

-- liftCodensityOrd :: Monad m => m a -> CodensityOrd m a
-- liftCodensityOrd m = CodensityOrd ((>>=) m)

-- lowerCodensityOrd :: (Ord a, Monad m) => CodensityOrd m a -> m a
-- lowerCodensityOrd m = runCodensityOrd m return

instance Functor (CodensityOrd f) where
fmap f m = CodensityOrd (\k -> runCodensityOrd m (k . f))

instance Applicative (CodensityOrd f) where
pure x = CodensityOrd (\k -> k x)
mf <*> mx = CodensityOrd (\k -> runCodensityOrd mf (\f ->
runCodensityOrd mx (\x -> k (f x))))

instance Monad (CodensityOrd f) where
return = pure
m >>= k = CodensityOrd (\c -> runCodensityOrd m (\a ->
runCodensityOrd (k a) c))



liftSet :: Ord a => Set a -> CodensityOrd Set a
liftSet m = CodensityOrd (bind m)
where bind :: (Ord a, Ord b) => Set a -> (a -> Set b) -> Set b
mx `bind` fxmy = S.fold (\x my -> fxmy x `S.union` my) S.empty mx

lowerSet :: Ord a => CodensityOrd Set a -> Set a
lowerSet m = runCodensityOrd m S.singleton


main = print $ lowerSet $ monadicPlus (liftSet $ S.fromList [1, 2, 3])
(liftSet $ S.fromList [1, 2, 3])

monadicPlus :: Monad m => m Int -> m Int -> m Int
monadicPlus mx my = do
x <- mx
y <- my
return (x + y)

\end{code}

[Sebastian Fischer]

Hi Max,

very interesting observations!

Post by Max Bolingbroke
By the way, you can use this stuff to solve the restricted monad
problem (e.g. make Set an instance of Monad). This is not that useful
until we find out what the mother of all MonadPlus is, though, because
we really need a MonadPlus Set instance.

I'm not sure whether this is TMOA MonadPlus, but here is a set monad
with MonadPlus instance (code below).

Cheers,
Sebastian

\begin{code}
{-# LANGUAGE RankNTypes #-}

module SetMonad where

import Data.Set ( Set )
import qualified Data.Set as Set

import Control.Monad ( MonadPlus(..) )

newtype SetMonad a
= SetMonad { (>>-) :: forall b . Ord b => (a -> Set b) -> Set b }

fromSet :: Set a -> SetMonad a
fromSet = Set.fold (mplus . return) mzero

toSet :: Ord a => SetMonad a -> Set a
toSet s = s >>- Set.singleton

instance Monad SetMonad where
return x = SetMonad ($x)
a >>= f = SetMonad (\k -> a >>- \x -> f x >>- k)

instance MonadPlus SetMonad where
mzero = SetMonad (\_ -> Set.empty)
a `mplus` b = SetMonad (\k -> Set.union (a >>- k) (b >>- k))

\end{code}

[David Menendez]

On Sun, Jun 27, 2010 at 1:26 PM, Sebastian Fischer

Post by Sjoerd Visscher
Hi Max,
very interesting observations!

Post by Max Bolingbroke
By the way, you can use this stuff to solve the restricted monad
problem (e.g. make Set an instance of Monad). This is not that useful
until we find out what the mother of all MonadPlus is, though, because
we really need a MonadPlus Set instance.

I'm not sure whether this is TMOA MonadPlus, but here is a set monad with
MonadPlus instance (code below).

Any continuation monad can be made an instance of MonadPlus if the
final value is a monoid. But whether that serves your purposes or not
depends on what specific properties you want mplus to have.

It's also worth asking why you might prefer the set monad to the list
monad. It has some nice properties (it's commutative and idempotent),
but you can get that by using the list monad internally and only
allowing observation of the values after converting to Set.

There's also the efficiency angle. In the list monad, this expression:

return x `mplus` return x >>= f

will calculate (f x) twice. In principle, the set monad can avoid
this, but in the continuation-based implementation, this evaluates to
\k -> Set.union (f x >>- k) (f x >>- k), which is just as inefficient
as the list monad.

[Edward Kmett]

Post by Max Bolingbroke
By the way, you can use this stuff to solve the restricted monad
problem (e.g. make Set an instance of Monad). This is not that useful
until we find out what the mother of all MonadPlus is, though, because
we really need a MonadPlus Set instance.
Code below.
Cheers,
Max
\begin{code}
{-# LANGUAGE RankNTypes #-}
import Control.Applicative
import Data.Set (Set)
import qualified Data.Set as S
newtype CodensityOrd m a = CodensityOrd { runCodensityOrd :: forall b.
Ord b => (a -> m b) -> m b }
-- liftCodensityOrd :: Monad m => m a -> CodensityOrd m a
-- liftCodensityOrd m = CodensityOrd ((>>=) m)
-- lowerCodensityOrd :: (Ord a, Monad m) => CodensityOrd m a -> m a
-- lowerCodensityOrd m = runCodensityOrd m return
instance Functor (CodensityOrd f) where
fmap f m = CodensityOrd (\k -> runCodensityOrd m (k . f))
instance Applicative (CodensityOrd f) where
pure x = CodensityOrd (\k -> k x)
mf <*> mx = CodensityOrd (\k -> runCodensityOrd mf (\f ->
runCodensityOrd mx (\x -> k (f x))))
instance Monad (CodensityOrd f) where
return = pure
m >>= k = CodensityOrd (\c -> runCodensityOrd m (\a ->
runCodensityOrd (k a) c))
liftSet :: Ord a => Set a -> CodensityOrd Set a
liftSet m = CodensityOrd (bind m)
where bind :: (Ord a, Ord b) => Set a -> (a -> Set b) -> Set b
mx `bind` fxmy = S.fold (\x my -> fxmy x `S.union` my) S.empty mx
lowerSet :: Ord a => CodensityOrd Set a -> Set a
lowerSet m = runCodensityOrd m S.singleton
main = print $ lowerSet $ monadicPlus (liftSet $ S.fromList [1, 2, 3])
(liftSet $ S.fromList [1, 2, 3])
monadicPlus :: Monad m => m Int -> m Int -> m Int
monadicPlus mx my = do
x <- mx
y <- my
return (x + y)
\end{code}

I've pointed out the Codensity Set monad on the Haskell channel. It is an
interesting novelty, but it unfortunately has somewhat funny semantics in
that the intermediate sets that you obtain are based on what you would get
if you reparenthesized all of your binds and associating them to the right.

One way to think about how Codensity adjusts a monad is that it can take
something that is almost a monad (you need to get in and out of Codensity).
Another thing to note is that Codensity is slightly more powerful than the
original type you embedded.

An interesting example is that you can show that Codensity Reader ~ State.
Take a look at the code in monad-ran on hackage for how Ran (StateT s m) is
implemented for an example.

-Edward Kmett

[Max Bolingbroke]

Post by Edward Kmett
I've pointed out the Codensity Set monad on the Haskell channel.

I spend no time on #haskell but clearly I should :)

Post by Edward Kmett
It is an
interesting novelty, but it unfortunately has somewhat funny semantics in
that the intermediate sets that you obtain are based on what you would get
if you reparenthesized all of your binds and associating them to the right.

But by the monad laws this is a totally fine thing to do, so this
shouldn't lead to any unfortunate behaviour in practice, I hope.

Post by Edward Kmett
Another thing to note is that Codensity is slightly more powerful than the
original type you embedded.

That is a very interesting observation. I'll be sure to look at monad-ran.

Can you cast any light on the connection with NBE? It seems like a
deep and powerful connection, so I'm sure it must correspond to some
interesting categorical principal.

All the best,
Max

[Edward Kmett]

Post by Max Bolingbroke

Post by Edward Kmett
I've pointed out the Codensity Set monad on the Haskell channel.

I spend no time on #haskell but clearly I should :)

Post by Edward Kmett
It is an
interesting novelty, but it unfortunately has somewhat funny semantics in
that the intermediate sets that you obtain are based on what you would

get

Post by Edward Kmett
if you reparenthesized all of your binds and associating them to the

right.
But by the monad laws this is a totally fine thing to do, so this
shouldn't lead to any unfortunate behaviour in practice, I hope.

Actually the resulting behavior _is_ rather unfortunate because it never
collapses the contained values until you go through the 'normalization by
evaluation' phase and lower it back down. So even even if you only generate
2 elements at each step, (which are already present in the set!), and run
the calculation for 100 operations or so you can take longer that the life
expectancy of the universe to terminate. ;)

Can you cast any light on the connection with NBE? It seems like a

Post by Max Bolingbroke
deep and powerful connection, so I'm sure it must correspond to some
interesting categorical principal.

You're looking at initial objects in various categories, effectively these
are given rise to by colimits, and as initial objects, there exist morphisms
from them to all other objects in their respective categories. The trick is
learning to see the category you're asking for in the right terms.

For instance Mendler-style catamorphisms, can serve as the "mother of all
folds"

type MendlerAlgebra f c = forall a. (a -> c) -> f a -> c

mcata :: MendlerAlgebra f c -> Mu f -> c

mcata phi = phi (mcata phi) . outF

http://knol.google.com/k/catamorphisms#

and like many of these constructs in Haskell, is built around a Kan
extension (or in this case, you can see it more directly as the
contravariant Yoneda lemma in negative position).

-Edward Kmett

[Sjoerd Visscher]

Hi Max,

This is really interesting!

Post by Max Bolingbroke

lift :: X d => d a -> D a
lower :: X d => D a -> d a
instance X D

With *no superclass constraints*.
lift :: X d => d a -> D d a
lower :: X d => D d a -> d a
instance X (D d)

This might help when looking for a matching categorical concept. With your original signatures I was thinking of initial/terminal objects, but that's not the case.

Post by Max Bolingbroke
2. Is there a mother of all idioms? By analogy with the previous three

-- (<**>) :: forall a. i a -> (forall b. i (a -> b) -> i b)
newtype Thingy i a = Thingy { runThingy :: forall b. i (a -> b) -> i b }

But I can't see how to write either pure or <*> with that data type.

newtype Thingy i a = Thingy { runThingy :: forall b. Yoneda i (a -> b) -> i b }

Because you can write pure (pure x = Thingy (\k -> lowerYoneda (fmap
($ x) k))). But <*> still eludes me!

It's usually easier to switch to Monoidal functors when playing with Applicative. (See the original Functional Pearl "Applicative programming with effects".)

Then I got this:

newtype Thingy i a = Thingy { runThingy :: forall b. Yoneda i b -> Yoneda i (a, b) }

(&&&) :: Thingy i c -> Thingy i d -> Thingy i (c, d)
mf &&& mx = Thingy $ fmap (\(d, (c, b)) -> ((c, d), b)) . runThingy mx . runThingy mf

instance Functor (Thingy i) where
fmap f m = Thingy $ fmap (first f) . runThingy m

instance Applicative (Thingy i) where
pure x = Thingy $ fmap (x,)
mf <*> mx = fmap (\(f, x) -> f x) (mf &&& mx)

Note that Yoneda is only there to make it possible to use fmap without the Functor f constraint. So I'm not sure if requiring no class constraints at all is a good requirement. It only makes things more complicated, without providing more insights.

I'd say that if class X requires a superclass constraint Y, then the instance of X (D d) is allowed to have the constraint Y d. The above code then stays the same, only with Yoneda removed and constraints added.

greetings,
--
Sjoerd Visscher
http://w3future.com

[Sjoerd Visscher]

Allowing Functor i also makes defining Thingy directly (without going though Monoidal) easy:

newtype Thingy i a = Thingy { runThingy :: forall b. i (a -> b) -> i b }

instance Functor i => Functor (Thingy i) where
fmap f m = Thingy $ runThingy m . fmap (. f)

instance Functor i => Applicative (Thingy i) where
pure x = Thingy $ fmap ($ x)
mf <*> mx = Thingy $ runThingy mx . runThingy mf . fmap (.)

Not allowing Functor i and adding Yoneda also works.

Post by Sjoerd Visscher
Hi Max,
This is really interesting!

Post by Max Bolingbroke

lift :: X d => d a -> D a
lower :: X d => D a -> d a
instance X D

With *no superclass constraints*.
lift :: X d => d a -> D d a
lower :: X d => D d a -> d a
instance X (D d)

This might help when looking for a matching categorical concept. With your original signatures I was thinking of initial/terminal objects, but that's not the case.

Post by Max Bolingbroke
2. Is there a mother of all idioms? By analogy with the previous three

-- (<**>) :: forall a. i a -> (forall b. i (a -> b) -> i b)
newtype Thingy i a = Thingy { runThingy :: forall b. i (a -> b) -> i b }

But I can't see how to write either pure or <*> with that data type.

newtype Thingy i a = Thingy { runThingy :: forall b. Yoneda i (a -> b) -> i b }

Because you can write pure (pure x = Thingy (\k -> lowerYoneda (fmap
($ x) k))). But <*> still eludes me!

It's usually easier to switch to Monoidal functors when playing with Applicative. (See the original Functional Pearl "Applicative programming with effects".)
newtype Thingy i a = Thingy { runThingy :: forall b. Yoneda i b -> Yoneda i (a, b) }
(&&&) :: Thingy i c -> Thingy i d -> Thingy i (c, d)
mf &&& mx = Thingy $ fmap (\(d, (c, b)) -> ((c, d), b)) . runThingy mx . runThingy mf
instance Functor (Thingy i) where
fmap f m = Thingy $ fmap (first f) . runThingy m
instance Applicative (Thingy i) where
pure x = Thingy $ fmap (x,)
mf <*> mx = fmap (\(f, x) -> f x) (mf &&& mx)
Note that Yoneda is only there to make it possible to use fmap without the Functor f constraint. So I'm not sure if requiring no class constraints at all is a good requirement. It only makes things more complicated, without providing more insights.
I'd say that if class X requires a superclass constraint Y, then the instance of X (D d) is allowed to have the constraint Y d. The above code then stays the same, only with Yoneda removed and constraints added.
greetings,
--
Sjoerd Visscher
http://w3future.com
_______________________________________________
Haskell-Cafe mailing list
http://www.haskell.org/mailman/listinfo/haskell-cafe

--
Sjoerd Visscher
http://w3future.com

[Max Bolingbroke]

newtype Thingy i a = Thingy { runThingy :: forall b. i (a -> b) -> i b }

Great stuff! I particularly like your <*> definition, because it
mirrors the composition law for Applicative nicely:
-- pure id <*> v = v -- Identity
-- pure (.) <*> u <*> v <*> w = u <*> (v <*> w) -- Composition
-- pure f <*> pure x = pure (f x) -- Homomorphism
-- u <*> pure y = pure ($ y) <*> u -- Interchange

I think it's very important that we use Yoneda here. The reason is
that all the examples I have so far express some sort of normalisation
property:
1) Functors can be normalised by fusing together fmap compositions
into single fmaps
2) Categories can be normalised by reassocating (.) applications into
a canonical form, and using identity to discard compositions with id.
This is achieved in Wotsit by using the associativity and id property
of (.) for functions.
3) Monads can be normalised using the monad laws to reassociate (>>=)
rightwards and using left and right identity to discard parts of the
computation. The resulting form seems to correspond to the "monadic
normal form" from the literature.

Applicatives also have a normalisation property. I first saw this in
Malcolm Wallaces's Flatpack presentation at Fun In The Afternoon:
http://sneezy.cs.nott.ac.uk/fun/feb-10/. Unfortunately the slides are
not online. The normalisation rules are something like this, each
corresponds to an applicative law:

v ==> pure id <*> v -- Identity
u <*> (v <*> w) ==> pure (.) <*> u <*> v <*> w -- Composition
pure f <*> pure x ==> pure (f x) -- Homomorphism
u <*> pure y ==> pure ($ y) <*> u -- Interchange

Some critical side conditions are needed here and there to ensure
termination. But the idea as I remember it was to rewrite all
applicative expressions to a form (pure f <*> u1 <*> ... <*> un) where
f is a pure function and each ui is a side-effecting computation which
is not of the form (v <*> w) or (pure f) -- i.e. it uses some
non-Applicative combinators to get its side effects.

Somehow the "mother of all applicatives" should encode this
normalisation property. If we didn't use Yoneda in our current
definition, then my intuition tells me that we wouldn't be able to get
guaranteed fusion adjacent pure f <*> pure x computations, so the
normalisation property corresponding to the modified Thingy would be
weaker.

I'm going to try automatically deriving a NBE algorithm for Moggi's
monadic metalanguage from the Codensity monad - with luck it will
correspond to the one-pass algorithm of Danvy. If this is possible it
will further strengthen the connection between "mothers" and NBE. By
repeating this exercise for Applicative and Thingy we should get a
beautiful algorithm for finding applicative normal forms.

Exciting stuff! Will report back if I make progress :-)

Max

[Max Bolingbroke]

Post by Max Bolingbroke
I'm going to try automatically deriving a NBE algorithm for Moggi's
monadic metalanguage from the Codensity monad - with luck it will
correspond to the one-pass algorithm of Danvy.

Well, that works. On second thoughts, it's more akin to A-normalisation.

What I will show is how to derive an algorithm for A-normalisation
from the definition of the Codensity monad.

First, the language to normalise. Hacked this together, so I'm just

Post by Max Bolingbroke
type Term = String
data MonadSyn = Return Term
| Bind MonadSyn (String -> MonadSyn)
| Foreign String

We have an injection from the pure terms, a bind operation in HOAS
style, and a "Foreign" constructor. I'm going to use Foreign to
introduce operations that have side effects but don't come from the
Monad type class. For example, we might include "get" and "put x" for
a state monad in here.

Now the meat:

\begin{code}
normalise :: MonadSyn -> MonadSyn
normalise m = go m Return
where
go :: MonadSyn -> (String -> MonadSyn) -> MonadSyn
go (Return x) k = k x
go (Bind m k) c = go m (\a -> go (k a) c)

go (Foreign x) k = Bind (Foreign x) k
\end{code}

What's really fun about this is that I pretty much transcribed the
definition of the Codensity monad instance. The initial "Return" comes
from "lowerCodensity" and then I just typed in the Return and Bind

Post by Max Bolingbroke
return x = Codensity (\k -> k x)
m >>= k = Codensity (\c -> runCodensity m (\a -> runCodensity (k a) c))

Foreign didn't come automatically: I had to use intelligence to tell
the normaliser how to deal with non-Monad computations. I'm happy with
that.

Now we can have an example:

\begin{code}
non_normalised = Bind (Return "10") $ \x ->
Bind (Bind (Bind (Foreign "get") (\y -> Return y))
(\z -> Bind (Foreign ("put " ++ x)) (\_ -> Return z))) $ \w ->
Return w

main = do
putStrLn "== Before"
print $ pPrint non_normalised

putStrLn "== After"
print $ pPrint $ normalise non_normalised
\end{code}

Which produces:

== Before
let x2 = 10
in let x0 = let x1 = let x4 = get
in x4
in let x3 = put x2
in x1
in x0
== After
let x2 = get
in let x0 = put 10
in x2

Amazing! A-normalisation of a monadic metalanguage, coming pretty much
mechanically from Codensity :-)

I'm going to try for normalisation of Lindleys idiom calculus now.

Cheers,
Max

[Max Bolingbroke]

Post by Max Bolingbroke
I'm going to try for normalisation of Lindleys idiom calculus now.

Made me sweat, but I got it to work. From "Thingy" you get a free
one-pass normaliser for idioms. Is this a novel result? It's certainly
very cool!

Term language:

\begin{code}
type Term = String

data IdiomSyn = Pure Term
| Ap IdiomSyn IdiomSyn
| Foreign String
\end{code}

The normalisation algorithm:

\begin{code}
normalise :: IdiomSyn -> IdiomSyn
normalise m = go m (\tt -> Pure (tt "id")) id
where
-- i a -> forall b. (forall c. ((a -> b) -> c) -> i c)
-> (forall d. (b -> d) -> i d)
go :: IdiomSyn -> ( (Term -> Term) ->
IdiomSyn) -> ( (Term -> Term) -> IdiomSyn)

go (Pure x) m = \k -> m (k . (\t -> t ++ " (" ++ x ++ ")"))
go (Ap mf mx) m = go mx (go mf (\k -> m (k . (\t -> "(.) (" ++ t
++ ")"))))
go (Foreign e) m = \k -> m (\t -> "(.) (\\x -> " ++ k "x" ++ ") ("
++ t ++ ")") `Ap` Foreign e
\end{code}

As before, we get Pure and Ap for free from Thingy if we just unfold

Post by Max Bolingbroke
newtype Thingy i a = Thingy { runThingy :: forall b. Yoneda i (a -> b) -> Yoneda i b }
instance Applicative (Thingy i) where
pure x = Thingy $ \m -> Yoneda (\k -> runYoneda m (k . ($ x)))
mf <*> mx = Thingy $ \m -> runThingy mx (runThingy mf (Yoneda (\k -> runYoneda m (k . (.)))))

It is fairly easy to see how they relate. The "Foreign" rule was
tricky, and I derived the correct form by following the types (please
pardon my lack of variable hygiene too!).

Here are some examples that show how we can derive the applicative
normal forms of a few terms, in exactly the form that I remembered
from Wallace's Flatpack presentation:

"""
== Before
launchMissiles <*> (obtainLaunchCode <*> (getAuthorization))
== After
pure ((.) (\x -> (.) (\x -> (.) (\x -> x) (x)) ((.) (x))) ((.) (id)))
<*> (launchMissiles) <*> (obtainLaunchCode) <*> (getAuthorization)
== Before
pure (launchMissiles') <*> (pure (obtainLaunchCode') <*> (pure
(getAuthorization')))
== After
pure ((.) ((.) (id) (launchMissiles')) (obtainLaunchCode') (getAuthorization'))
== Before
pure (f) <*> (pure (x))
== After
pure ((.) (id) (f) (x))
== Before
launchMissiles <*> (pure (1337))
== After
pure ((.) (\x -> x (1337)) ((.) (id))) <*> (launchMissiles)
"""

Pretty awesome! Perhaps I should write a paper or at least a coherent
note on this topic :-)

Cheers,
Max

[Edward Kmett]

Post by Sjoerd Visscher
Hi Max,
This is really interesting!

Post by Max Bolingbroke

lift :: X d => d a -> D a
lower :: X d => D a -> d a
instance X D

With *no superclass constraints*.
lift :: X d => d a -> D d a
lower :: X d => D d a -> d a
instance X (D d)

This might help when looking for a matching categorical concept. With your
original signatures I was thinking of initial/terminal objects, but that's
not the case.

Post by Max Bolingbroke
2. Is there a mother of all idioms? By analogy with the previous three

-- (<**>) :: forall a. i a -> (forall b. i (a -> b) -> i b)
newtype Thingy i a = Thingy { runThingy :: forall b. i (a -> b) -> i b }

But I can't see how to write either pure or <*> with that data type.

newtype Thingy i a = Thingy { runThingy :: forall b. Yoneda i (a -> b)

-> i b }

Post by Max Bolingbroke
Because you can write pure (pure x = Thingy (\k -> lowerYoneda (fmap
($ x) k))). But <*> still eludes me!

It's usually easier to switch to Monoidal functors when playing with
Applicative. (See the original Functional Pearl "Applicative programming
with effects".)
newtype Thingy i a = Thingy { runThingy :: forall b. Yoneda i b -> Yoneda i (a, b) }
(&&&) :: Thingy i c -> Thingy i d -> Thingy i (c, d)
mf &&& mx = Thingy $ fmap (\(d, (c, b)) -> ((c, d), b)) . runThingy mx . runThingy mf
instance Functor (Thingy i) where
fmap f m = Thingy $ fmap (first f) . runThingy m
instance Applicative (Thingy i) where
pure x = Thingy $ fmap (x,)
mf <*> mx = fmap (\(f, x) -> f x) (mf &&& mx)
Note that Yoneda is only there to make it possible to use fmap without the
Functor f constraint. So I'm not sure if requiring no class constraints at
all is a good requirement. It only makes things more complicated, without
providing more insights.
I'd say that if class X requires a superclass constraint Y, then the
instance of X (D d) is allowed to have the constraint Y d. The above code
then stays the same, only with Yoneda removed and constraints added.

This is an encoding of the fact that all Functors in Haskell are strong, and
that Yoneda i is a Functor for any i :: * -> *.

-Edward Kmett

[Roman Leshchinskiy]

Post by Max Bolingbroke
Q: What is the "mother of all X", where X is some type class?

lift :: X d => d a -> D a
lower :: X d => D a -> d a

Are those universally quantified over d? If so, then none of your examples fit this definition. I assume you mean this:

lift :: X d => d a -> D d a
lower :: X d => D d a -> d a

In that case, isn't D just the dictionary for (X d) and a value of type (d a)? I.e., couldn't we always define it as:

data D d a where { D :: X d => d a -> D d a }

Roman

[Max Bolingbroke]

Post by Roman Leshchinskiy
data D d a where { D :: X d => d a -> D d a }

I wondered about this, but how would you write e.g. the "return"
method for Codensity? You don't have an input dictionary to work with.

Cheers,
Max

[Felipe Lessa]

Post by Max Bolingbroke
Example 2: Codensity is the mother of all Monads

I thought the continuation monad was the mother of all monads. :)
For example, see [1].

Cheers!

[1] http://blog.sigfpe.com/2008/12/mother-of-all-monads.html

--
Felipe.

[Max Bolingbroke]

Post by Felipe Lessa

Post by Max Bolingbroke
Example 2: Codensity is the mother of all Monads

I thought the continuation monad was the mother of all monads. :)

I actually already referenced Dan's article, and stole the vocabulary
from him :-). Codensity is a better model, see e.g. Edward Kmett's
first comment on Dan's post
(http://blog.sigfpe.com/2008/12/mother-of-all-monads.html#comment-1).

Cheers,
Max

[Twan van Laarhoven]

Post by Max Bolingbroke
I don't actually know what the right name for this data type is, I

-- (>>>) :: forall a b. t a b -> (forall c. t b c -> t a c)
newtype Wotsit t a b = Wotsit { runWotsit :: forall c. t b c -> t a c }

There is of course no reason to prefer (>>>) to (<<<), so you can instead
quantify over the first argument as opposed to second one:

newtype Wotsit' t a b = Wotsit' { runWotsit' :: forall c. t c a -> t c b }

liftWotsit' :: Category t => t a b -> Wotsit' t a b
liftWotsit' t = Wotsit' ((<<<) t)

lowerWotsit' :: Category t => Wotsit' t a b -> t a b
lowerWotsit' t = runWotsit' t id

instance Category (Wotsit' t) where
id = Wotsit' id
t1 . t2 = Wotsit' (runWotsit' t1 . runWotsit' t2)


Twan