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

[Max Bolingbroke]

On 27 June 2010 19:14, Max Bolingbroke <batterseapower at 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