Simply Typed Lambda Calculus

Main.hs

module Main where
import Data.Maybe

--  ____  _                 _         _____                     _
-- / ___|(_)_ __ ___  _ __ | |_   _  |_   _|   _ _ __   ___  __| |
-- \___ \| | '_ ` _ \| '_ \| | | | |   | || | | | '_ \ / _ \/ _` |
--  ___) | | | | | | | |_) | | |_| |   | || |_| | |_) |  __/ (_| |
-- |____/|_|_| |_| |_| .__/|_|\__, |   |_| \__, | .__/ \___|\__,_|
--  _                |_| _    |___/_       |___/|_|     _            _
-- | |    __ _ _ __ ___ | |__   __| | __ _   / ___|__ _| | ___ _   _| |_   _ ___
-- | |   / _` | '_ ` _ \| '_ \ / _` |/ _` | | |   / _` | |/ __| | | | | | | / __|
-- | |__| (_| | | | | | | |_) | (_| | (_| | | |__| (_| | | (__| |_| | | |_| \__ \
-- |_____\__,_|_| |_| |_|_.__/ \__,_|\__,_|  \____\__,_|_|\___|\__,_|_|\__,_|___/

--------------------------------------------------------------------------------
--- AST ------------------------------------------------------------------------
--------------------------------------------------------------------------------

data Typ
  = Boolean
  | Number
  | Arrow Typ Typ
  deriving (Show, Eq)

data Exp
  = Add Exp Exp
  | And Exp Exp
  | App Exp Exp
  | Lam String Typ Exp
  | Var String
  | Num Integer
  | Booln Bool
  deriving (Show, Eq)

type ContextT = [(String, Typ)]
type ContextV = [(String, Exp)]

--------------------------------------------------------------------------------
--- TYPECHECKER ----------------------------------------------------------------
--------------------------------------------------------------------------------

check :: ContextT -> Exp -> Typ
check context (Add e e')   = let t  = check context e
                                 t' = check context e'
                             in
                               case (t, t') of
                                 (Number, Number) -> Number
                                 _                -> error "Addition on non-number types"
check context (And e e')   = let t  = check context e
                                 t' = check context e'
                             in
                               case (t, t') of
                                 (Boolean, Boolean) -> Boolean
                                 _                  -> error "And on non-boolean types"
check context (App e e')   = let t  = check context e
                                 t' = check context e'
                             in
                               case t of
                                 (Arrow from to) -> if from /= t' then error "Application type mismatch" else to
                                 _               -> error "Applying non-arrow type"
check context (Lam p pt b) = let context' = (p, pt):context
                                 t        = check context' b
                             in
                               Arrow pt t
check context (Var x)      = let mt = lookup x context
                             in
                               fromMaybe (error "Type for variable not defined") mt
check context (Num i)      = Number
check context (Booln b)    = Boolean

--------------------------------------------------------------------------------
--- EVALUATOR ------------------------------------------------------------------
--------------------------------------------------------------------------------

eval :: ContextV -> Exp -> Exp
eval context (Add e e')  = let (Num x) = eval context e
                               (Num y) = eval context e'
                           in
                             Num $ x + y
eval context (And e e')  = let (Booln x) = eval context e
                               (Booln y) = eval context e'
                           in
                             Booln $ x && y
eval context (App e e')  = let par         = eval context e'
                               (Lam s _ b) = eval context e
                               context'    = (s, par):context
                           in
                             eval context' b
eval context (Lam s t b) = Lam s t b
eval context (Var x)     = let Just val = lookup x context
                           in
                             val
eval context (Num i)     = Num i
eval context (Booln b)   = Booln b

--------------------------------------------------------------------------------
--- MAIN -----------------------------------------------------------------------
--------------------------------------------------------------------------------

main :: IO ()
main =
  let anumber = Num 5
      abool   = Booln False
      test1   = Add anumber anumber
      test2   = And abool abool
      test3   = Lam "x" Boolean (And (Var "x") (Var "x"))
      test4   = App test3 abool
      test5   = Lam "x" Boolean (And (Booln True) (Var "x"))
      test6   = App test5 (Booln True)
  in
    do mapM_ (print . check []) [test1, test2, test3, test4, test5, test6]
       mapM_ (print . eval [])  [test1, test2, test3, test4, test5, test6]