[Haskell-cafe] The mother of all functors/monads/categories
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-cafe@haskell.org/msg57738.html
Preliminaries
===
Q: What is the mother of all X, where X is some type class?
A: It is a data type D such that:
1. There exist total functions:
lift :: X d = d a - D a
lower :: X d = D a - d a
2. And you can write a valid instance:
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
the category-extras package (thanks Edward!). Here is the data type:
-- 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
constraint on the lowerYoneda call:
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
we will need the Y f constraint to do so. Here is an example:
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
===
Data type:
-- (=) :: forall a. m a - (forall b. (a - m b) - m b)
newtype Codensity m a = Codensity { runCodensity :: forall b. (a - m b) - m
b }
Isomorphism. We need Monad constraints on both ends now:
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
Instances:
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
just invented it and it seems to work:
-- () :: 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 }
Isomorphism:
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
And finally the instance:
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
examples, I tried this:
-- (**) :: 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.
This version seems to work slightly
Re: [Haskell-cafe] The mother of all functors/monads/categories
Hi Max,
This is really interesting!
1. There exist total functions:
lift :: X d = d a - D a
lower :: X d = D a - d a
2. And you can write a valid instance:
instance X D
With *no superclass constraints*.
All your examples have a more specific form:
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.
2. Is there a mother of all idioms? By analogy with the previous three
examples, I tried this:
-- (**) :: 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.
This version seems to work slightly better:
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] The mother of all functors/monads/categories
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.
On Jun 27, 2010, at 1:43 PM, Sjoerd Visscher wrote:
Hi Max,
This is really interesting!
1. There exist total functions:
lift :: X d = d a - D a
lower :: X d = D a - d a
2. And you can write a valid instance:
instance X D
With *no superclass constraints*.
All your examples have a more specific form:
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.
2. Is there a mother of all idioms? By analogy with the previous three
examples, I tried this:
-- (**) :: 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.
This version seems to work slightly better:
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
--
Sjoerd Visscher
http://w3future.com
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] The mother of all functors/monads/categories
On 27/06/2010, at 19:54, Max Bolingbroke wrote:
Q: What is the mother of all X, where X is some type class?
A: It is a data type D such that:
1. There exist total functions:
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] The mother of all functors/monads/categories
On Sun, Jun 27, 2010 at 10:54:08AM +0100, Max Bolingbroke wrote: 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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] The mother of all functors/monads/categories
On 27 June 2010 14:30, Roman Leshchinskiy r...@cse.unsw.edu.au wrote:
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 }
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] The mother of all functors/monads/categories
On 27 June 2010 16:07, Felipe Lessa felipe.le...@gmail.com wrote: On Sun, Jun 27, 2010 at 10:54:08AM +0100, Max Bolingbroke wrote: 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] The mother of all functors/monads/categories
On 27 June 2010 13:16, Sjoerd Visscher sjo...@w3future.com wrote:
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 }
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] The mother of all functors/monads/categories
On 27 June 2010 18:28, Max Bolingbroke batterseapo...@hotmail.com wrote:
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
going to use Strings to represent terms of pure type:
type Term = String
Terms of computational type:
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
implementations pretty much verbatim:
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] The mother of all functors/monads/categories
On 27 June 2010 19:14, Max Bolingbroke batterseapo...@hotmail.com wrote:
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
the uses of the Yoneda fmap like so:
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] The mother of all functors/monads/categories
On Sun, Jun 27, 2010 at 7:43 AM, Sjoerd Visscher sjo...@w3future.comwrote:
Hi Max,
This is really interesting!
1. There exist total functions:
lift :: X d = d a - D a
lower :: X d = D a - d a
2. And you can write a valid instance:
instance X D
With *no superclass constraints*.
All your examples have a more specific form:
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.
2. Is there a mother of all idioms? By analogy with the previous three
examples, I tried this:
-- (**) :: 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.
This version seems to work slightly better:
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.
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] The mother of all functors/monads/categories
Max Bolingbroke wrote:
I don't actually know what the right name for this data type is, I
just invented it and it seems to work:
-- () :: 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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
