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

Typed.hs

module Typed where

-- https://stackoverflow.com/questions/27831223/simply-typed-lambda-calculus-with-failure-in-haskell

import Safe (atMay)

data Type
  = LamT Type Type
  | NumT
  deriving (Eq, Show)

data Term
  = Var Int
  | Lam Type Term
  | App Term Term
  | Num Integer
  deriving Show

check :: [Type] -> Term -> Maybe Type
check env (Var x) = atMay env x
check env (Lam a b) = LamT a <$> check (a:env) b
check env (App f a) = do
  f <- check env f
  a <- check env a
  case f of
    LamT a' b | a == a' -> return b
    _ -> Nothing
check _ (Num _) = return NumT

data Value
  = Closure [Value] Term
  | Number Integer
  deriving Show

eval :: Term -> Maybe Value
eval t = go [] t <$ check [] t
  where
  go :: [Value] -> Term -> Value
  go env (Var x) = env !! x
  go env (Lam t x) = Closure env (Lam t x)
  go env (App x y) = apply (go env x) (go env y)
  go _ (Num x) = Number x

  apply :: Value -> Value -> Value
  apply (Closure env (Lam _ body)) x = go (x:env) body
  apply _ _ = undefined

s :: Term
s = Lam (LamT NumT (LamT NumT NumT)) (Lam (LamT NumT NumT) (Lam NumT (App (App (Var 2) (Var 0)) (App (Var 1) (Var 0)))))

k :: Term
k = Lam NumT (Lam NumT (Var 1))

i :: Term
i = Lam NumT (Var 0)

main :: IO ()
main = do
  print . eval $ App (Lam NumT (Var 0)) (App (Lam NumT (Num 10)) (Num 0))
  print . eval $ App (Lam (LamT NumT NumT) (App (Var 0) (Num 10))) (Lam NumT (Var 0))
  print . eval $ Lam NumT (Var 0)
  print . eval $ App (Lam NumT (Var 0)) (Num 10)
  print . eval $ App (App s k) i
  print . eval $ App (App (App s k) i) (Num 10)