Transforming an operational GADT using the Yoneda lemma.

YonedaGADT.hs

{-# LANGUAGE GADTs #-}

-- 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?

-}