Simply Typed Lambda Calculus with GADTs (doodle made while reading a SO answer).

General.hs

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

-- https://stackoverflow.com/questions/27831223/simply-typed-lambda-calculus-with-failure-in-haskell
-- https://www.youtube.com/watch?v=6snteFntvjM

module General where

data Elem as a where
  EZ :: Elem (x:xs) x
  ES :: Elem xs x -> Elem (y:xs) x

deriving instance Show (Elem as a)

data Expr as a where
  Ref  :: Elem as a -> Expr as a
  Lam  :: Expr (a:as) b -> Expr as (a -> b)
  App  :: Expr as (a -> b) -> Expr as a -> Expr as b
  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)
  Number  :: Integer -> Value Integer
  Boolean :: Bool -> Value Bool

deriving instance Show (Value a)

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

deriving instance Show (Env as)

eval :: Expr '[] a -> Value a
eval expr = eval' Empty expr
  where eval' :: Env as -> Expr as a -> Value a
        eval' env (Ref x)   = lookup' x env
        eval' env (Lam x)   = Closure env (Lam x)
        eval' env (App x y) = apply (eval' env x) (eval' env y)
        eval' _ (Num x)     = Number x
        eval' _ (Bool x)    = Boolean x

        apply :: Value (a -> b) -> Value a -> Value b
        apply (Closure env (Lam body)) x = eval' (Cons x env) body
        apply _ _ = undefined

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

-- eval $ App (Lam (Ref EZ)) (App (Lam (Num 10)) (Bool False))
-- eval $ App (Lam (App (Ref EZ) (Num 10))) (Lam (Ref EZ))
-- eval $ Lam (Ref EZ)

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

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

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

-- eval $ (App (App s k) k)
-- eval $ (App (App (App s k) k) (Num 10))