YonedaGADT.hs

{-# LANGUAGE GADTs, RankNTypes #-}

import Prelude hiding (read, print)

-- The "operational" form
data Action a where
    Print :: String -> Action ()
    Read :: Action String

{-

Yoneda lemma says these two are isomorphic:

    f a
    forall b. (a -> b) -> f b

Let's apply that to the result type of each data constructor in the GADT.

-}

-- The "free" form
data Action' a = Print' String (() -> a)
               | Read' (String -> a)

{-

Exercise: can we now simplify the Print' constructor?

-}

{-

Exercise: can we provide an isomorphism using Control.Functor.Yoneda?

-}

instance Functor Action' where
    fmap f (Print' s k) = Print' s (f . k)
    fmap f (Read' k)    = Read' (f . k)

type Yoneda f a = forall r. (a -> r) -> f r

to :: Functor f => Yoneda f a -> f a
to k = k id

from :: Functor f => f a -> Yoneda f a
from ma k = fmap k ma

print :: String -> Action' ()
print s = to $ Print' s

read :: Action' String
read = to Read'

print' :: String -> (() -> a) -> Action' a
print' s = from $ print s

read' :: (String -> a) -> Action' a
read' = from read