final-initial.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
module Main where

main :: IO ()
main = return ()

-- -------------------------------------------------------------------- --
-- An initial encoding of an untyped LC

data Nat = Z | S Nat

data Term
  = Var String
  | Lam String Term
  | App Term Term
  deriving (Eq, Show)

subst :: String -> Term -> Term -> Term
subst = error "feed me your subst"

eval :: Term -> Term
eval (App t u) = case (t, u) of
  (Lam n t', Lam _ u') -> subst n t' u'
  (Lam n t', u') -> let ua = eval u' in App t ua
  _ -> let t' = eval t in App t' u
eval _ = undefined

-- | A tagless GADT borrowing from Haskell's syntax
--
-- This is initial and tagless because the type system is doing the
-- tagging work via HOAS, instead of embedding the tags as constructors
-- of the term. Also, we typed LC now.
--
data TermA env a where
  AVar :: Var env a -> TermA env a
  ALam :: TermA (a,env) b -> TermA env (a -> b)
  AApp :: TermA env (a -> b) -> TermA env a -> TermA env b

data Var env a where
  VZ :: Var (a,env) a
  VS :: Var env a -> Var (a',env) a

-- -------------------------------------------------------------------- --
-- A final encoding of an typed LC

-- Haskell has a great way of representing a denotational bundle of semantics for a given type.
-- Called "typeclass":
--
class Symantics expr where
  z :: forall env a. expr (a,env) a
  s :: forall env a b. expr env a -> expr (b,env) a
  lam :: forall env a b. expr (a,env) b -> expr env (a -> b)
  app :: forall env a b. expr env (a -> b) -> expr env a -> expr env b

instance Symantics TermA where
  z = AVar VZ
  s a = case a of
    AVar v -> AVar (VS v)
    _ -> undefined
  lam = ALam
  app = AApp