\begin{code}
{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
module Mar15 where
import qualified Mar11
\end{code}
Learning objectives:
\begin{itemize}
\item GADTs
\item Typed Finally Tagless
\end{itemize}
GADT = Generalized Algebraic Data Type
Basic idea:
\begin{code}
data Foo where
One :: Foo
Two :: Foo
data Bar (a :: Foo) where
Thing1 :: Bar ‘One
Thing2 :: Bar ‘Two
data Baz a where
Toto :: Char -> Baz Char
Tata :: Int -> Baz Int
Tutu :: Char -> Int -> Baz a
funfun :: Baz Char -> Baz Int -> Baz a
funfun (Toto a) (Tata c) = Tutu a c
funfun (Toto a) (Tutu _ i) = Tutu a i
funfun (Tutu a i) _ = Tutu a i
\end{code}
Use it for languages:
\begin{code}
data Lang0 a where
Int :: Integer -> Lang0 Integer
Add :: Lang0 Integer -> Lang0 Integer -> Lang0 Integer
Mul :: Lang0 Integer -> Lang0 Integer -> Lang0 Integer
Bool :: Bool -> Lang0 Bool
And :: Lang0 Bool -> Lang0 Bool -> Lang0 Bool
Or :: Lang0 Bool -> Lang0 Bool -> Lang0 Bool
If :: Lang0 Bool -> Lang0 a -> Lang0 a -> Lang0 a
Leq :: Lang0 Integer -> Lang0 Integer -> Lang0 Bool
\end{code}
Recall the final version:
\begin{spec}
class Symantics (rep :: * -> *) where
int :: Integer -> rep Integer
add :: rep Integer -> rep Integer -> rep Integer
mul :: rep Integer -> rep Integer -> rep Integer
bool :: Bool -> rep Bool
and_ :: rep Bool -> rep Bool -> rep Bool
or_ :: rep Bool -> rep Bool -> rep Bool
if_ :: rep Bool -> rep a -> rep a -> rep a
leq :: rep Integer -> rep Integer -> rep Bool
\end{spec}
\begin{code}
ex1 :: Lang0 Bool
ex1 = If (Leq (Add (Int 3) (Int 5)) (Int 9))
(And (Bool True) (Bool False))
(Or (Bool True) (Bool False))
— This is a bad piece of code, for ALL INTERPRETATIONS
— ex2 :: Lang0 Integer
— ex2 = If (Bool True) (Int 5) (Bool False)
ex3 :: Lang0 Integer
ex3 = let x = Mul (Int 4) (Int 5)
y = Mul (Int (-3)) (Int 134) in
Mul (Add x y) (Mul y y)
\end{code}
\begin{code}
eval :: Lang0 a -> a
eval (Int i) = i
eval (Add x y) = eval x + eval y
eval (Mul x y) = eval x * eval y
eval (Bool b) = b
eval (And x y) = eval x && eval y
eval (Or x y) = eval x || eval y
eval (If b x y) = if eval b then eval x else eval y
eval (Leq x y) = eval x <= eval y
size :: Lang0 a -> Int
size (Int _) = 1
size (Add x y) = 1 + size x + size y
size (Mul x y) = 1 + size x + size y
size (Bool _) = 1
size (And x y) = 1 + size x + size y
size (Or x y) = 1 + size x + size y
size (If b x y) = 2 + size b + size x + size y
size (Leq x y) = 1 + size x + size y
\end{code}
But there is a deeper equivalence:
\begin{code}
instance Mar11.Symantics Lang0 where
int = Int
bool = Bool
add = Add
mul = Mul
and_ = And
or_ = Or
if_ = If
leq = Leq
newtype F a = F {unF :: Lang0 a}
— the strangest way to go in the other direction…
finalToGADT :: Lang0 a -> Lang0 a
finalToGADT = id
gadtToFinal :: Mar11.Symantics rep => Lang0 a -> rep a
gadtToFinal (Int i) = Mar11.int i
gadtToFinal (Add x y) = Mar11.add (gadtToFinal x) (gadtToFinal y)
gadtToFinal (Mul x y) = Mar11.mul (gadtToFinal x) (gadtToFinal y)
gadtToFinal (Bool b) = Mar11.bool b
gadtToFinal (And x y) = Mar11.and_ (gadtToFinal x) (gadtToFinal y)
gadtToFinal (Or x y) = Mar11.or_ (gadtToFinal x) (gadtToFinal y)
gadtToFinal (If b x y) = Mar11.if_ (gadtToFinal b) (gadtToFinal x) (gadtToFinal y)
gadtToFinal (Leq x y) = Mar11.leq (gadtToFinal x) (gadtToFinal y)
\end{code}