\begin{code}
{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE KindSignatures #-}
module Mar16 where
import Control.Applicative
import Data.Function (fix)
— useful for the implementation below
if’ :: Bool -> a -> a -> a
if’ b x y = if b then x else y
\end{code}
Learning objectives:
\begin{itemize}
\item Typed Finally Tagless — adding more features
\end{itemize}
(First, go back to Mar15 to fill in the one hole…)
First: Pairs
Second: Functions
Third: Fix, aka recursion!
\begin{code}
class Symantics (rep :: * -> *) where
int :: Integer -> rep Integer
add :: rep Integer -> rep Integer -> rep Integer
sub :: 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
— Pairs
pair :: rep a -> rep b -> rep (a , b) — (,) lifted
fst_ :: rep (a, b) -> rep a
snd_ :: rep (a, b) -> rep b
— Functions
app :: rep (a -> b) -> (rep a -> rep b) — ($) lifted
lam :: (rep a -> rep b) -> rep (a -> b) — \ lifted
— Fixpoints
fix_ :: rep (a -> a) -> rep a
\end{code}
Augment the |R| instance with new features:
\begin{code}
newtype R a = R {unR :: a}
instance Functor R where
— fmap f x = R $ f $ unR x
fmap f = R . f . unR
instance Applicative R where
pure = R
f <*> x = R $ (unR f) (unR x)
instance Symantics R where
int = pure
bool = pure
add = liftA2 (+)
sub = liftA2 (-)
mul = liftA2 (*)
and_ = liftA2 (&&)
or_ = liftA2 (||)
if_ = liftA3 (if’)
leq = liftA2 (<=) pair = liftA2 (,) fst_ = fmap fst snd_ = fmap snd app = liftA2 ($) -- the "follow the types version": -- lam f = R $ \x -> unR $ f (R x)
— first put compositions on the rhs
— lam f = R $ \x -> unR . f . R $ x
— eta contract
lam f = pure (unR . f . R)
fix_ = fmap fix
\end{code}
\begin{verbatim}
fst_ is also
fst_ x = R (fst $ unR x)
fst_ x = R . fst . unR $ x
fst_ = R . fst . unR
fst_ = fmap fst
\end{verbatim}
\begin{code}
max’ :: Symantics rep => rep Integer -> rep Integer -> rep Integer
max’ x y = if_ (leq x y) y x
max” :: Symantics rep => rep (Integer -> Integer -> Integer)
max” = lam (\x -> lam (\y -> max’ x y))
swap :: Symantics rep => rep ((a, b) -> (b, a))
swap = lam (\x -> pair (snd_ x) (fst_ x))
fact :: Symantics rep => rep (Integer -> Integer)
fact = fix (\self -> lam (\n -> if_ (leq n (int 1)) (int 1) (mul n (app self (sub n (int 1))))))
\end{code}
When creating a language, have introduction rules and elimination / computation
rules:
— Pairs
pair :: rep a -> rep b -> rep (a , b) — introduce
fst_ :: rep (a, b) -> rep a — eliminate
snd_ :: rep (a, b) -> rep b — eliminate
— Functions
lam :: (rep a -> rep b) -> rep (a -> b) — introduction
app :: rep (a -> b) -> (rep a -> rep b) — eliminate