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 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! 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
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}
Hi Max, very interesting observations!
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} -- Underestimating the novelty of the future is a time-honored tradition. (D.G.)
On Sun, Jun 27, 2010 at 1:26 PM, Sebastian Fischer
Hi Max,
very interesting observations!
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.
--
Dave Menendez
On Sun, Jun 27, 2010 at 6:25 AM, Max Bolingbroke wrote: 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
On 27 June 2010 22:20, Edward Kmett
I've pointed out the Codensity Set monad on the Haskell channel.
I spend no time on #haskell but clearly I should :)
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.
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
On Sun, Jun 27, 2010 at 6:45 PM, Max Bolingbroke wrote: On 27 June 2010 22:20, Edward Kmett I've pointed out the Codensity Set monad on the Haskell channel. I spend no time on #haskell but clearly I should :) 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. 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 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
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
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
On 27 June 2010 13:16, 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 }
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
On 27 June 2010 18:28, 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 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
On 27 June 2010 19:14, 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 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
On Sun, Jun 27, 2010 at 7:43 AM, Sjoerd Visscher
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
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
On 27 June 2010 14:30, Roman Leshchinskiy
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
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.
On 27 June 2010 16:07, Felipe Lessa
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
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
participants (8)
-
David Menendez -
Edward Kmett -
Felipe Lessa -
Max Bolingbroke -
Roman Leshchinskiy -
Sebastian Fischer -
Sjoerd Visscher -
Twan van Laarhoven