BiDir.hs

module Main

main = print "hi, I'm an example of bidirectional typechecking"

type Var = String

data Term 
  = Var Var
  | Abs Var Term
  | App Term Term
  | Tru
  | Fls
  | If Term Term Term
  | As Term Type
  deriving (Show, Eq)

data Type
  = BoolT
  | Type :-> Type
  deriving (Show, Eq)

type Context = [(Var, Type)]

infer :: Context -> Term -> Maybe Type
infer ctx (Var x) = lookup x ctx
infer _ Tru = pure BoolT
infer _ Fls = pure BoolT
infer ctx (App t1 t2) = do
  (ty1 :-> ty2) <- infer ctx t1
  ty2' <- check ctx t2 ty2
  pure ty2'
infer ctx (As t ty) = check ctx t ty
infer ctx (If t1 t2 t3) = undefined
infer ctx (Abs var t) = undefined

check :: Context -> Term -> Type -> Maybe Type
check ctx (If t1 t2 t3) ty = do
  p <- check ctx t1 BoolT
  ty2 <- check ctx t2 ty
  ty3 <- check ctx t3 ty
  if ty2 == ty3 then Just ty3 else Nothing
check ctx (Abs var t) (ty1 :-> ty2) = do
  ty2' <- check ((var, ty1) : ctx) t ty2
  pure $ ty1 :-> ty2
check ctx t ty = 
  case infer ctx t of
    Just ty' | ty == ty' -> Just ty
    _ -> Nothing

term :: Term
term = As (Abs "b" (If (Var "b") Fls Tru)) (BoolT :-> BoolT)

ctx :: Context
ctx = [("b", BoolT)]

typ :: Maybe Type
typ = infer ctx term