GADT implementation Simply Typed Lambda Calculus with Sum and Product types.

Typed.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}

module Typed where

import Prelude hiding (Left, Right, fst, snd)

data Elem as a where
  EZ :: Elem (a:as) a
  ES :: Elem as a -> Elem (b:as) a

instance Show (Elem as a) where
  show EZ     = show 0
  show (ES x) = show (1 + read (show x))

data Expr as a where
  Ref  :: Elem as a -> Expr as a
  Abs  :: Expr (a:as) b -> Expr as (a -> b)
  App  :: Expr as (a -> b) -> Expr as a -> Expr as b
  Pair :: Expr as a -> Expr as b -> Expr as (a, b)
  Fst  :: Expr as (a, b) -> Expr as a
  Snd  :: Expr as (a, b) -> Expr as b
  InL  :: Expr as a -> Expr as (Either a b)
  InR  :: Expr as b -> Expr as (Either a b)
  Case :: Expr as (Either a b) -> Expr (a:as) c -> Expr (b:as) c -> Expr as c
  Num  :: Integer -> Expr as Integer
  Bool :: Bool -> Expr as Bool

deriving instance Show (Expr as a)

data Value a where
  Closure :: Env as -> Expr as (a -> b) -> Value (a -> b)
  Tuple   :: Value a -> Value b -> Value (a, b)
  Left    :: Value a -> Value (Either a b)
  Right   :: Value b -> Value (Either a b)
  Number  :: Integer -> Value Integer
  Boolean :: Bool -> Value Bool

deriving instance Show (Value a)

fst :: Value (a, b) -> Value a
fst (Tuple x _) = x

snd :: Value (a, b) -> Value b
snd (Tuple _ x) = x

data Env as where
  Empty :: Env '[]
  Cons  :: Value a -> Env as -> Env (a:as)

deriving instance Show (Env as)

get :: Elem as a -> Env as -> Value a
get EZ (Cons x _)      = x
get (ES x) (Cons _ xs) = get x xs

eval :: Expr '[] a -> Value a
eval x = go Empty x
  where go :: Env as -> Expr as a -> Value a
        go env (Ref x)    = get x env
        go env (Abs x)    = Closure env (Abs x)
        go env (App x y)  = apply (go env x) (go env y)
        go env (Pair x y) = Tuple (go env x) (go env y)
        go env (Fst x)    = fst $ go env x
        go env (Snd x)    = snd $ go env x
        go env (InL x)    = Left (go env x)
        go env (InR x)    = Right (go env x)
        go env (Case x left right) =
          case (go env x) of
            Left x  -> go (Cons x env) left
            Right x -> go (Cons x env) right
        go _ (Num x)      = Number x
        go _ (Bool x)     = Boolean x

        apply :: Value (a -> b) -> Value a -> Value b
        apply (Closure env (Abs body)) x = go (Cons x env) body
        apply _ _ = undefined

s :: Expr as ((a -> b -> c) -> (a -> b) -> a -> c)
s = Abs (Abs (Abs (App (App (Ref (ES (ES EZ))) (Ref EZ)) (App (Ref (ES EZ)) (Ref EZ)))))

k :: Expr as (a -> b -> a)
k = Abs (Abs (Ref (ES EZ)))

i :: Expr as (a -> a)
i = Abs (Ref EZ)

-- eval $ s `App` k `App` k
-- eval $ s `App` k `App` k `App` Num 10