type Id = String data Exp = Var Id | App Exp Exp | Type | Abs Id Exp | Pi Id Exp Exp | Let Id Exp Exp Exp data Val = VGen Int | VApp Val Val | VType | VAbs FVal | VPi Val FVal type FVal = (Id,Exp,Env) type Env = [(Id,Val)] update :: Env -> Id -> Val -> Env update env x u = (x,u):env lookUp :: Id -> Env -> Val lookUp x ((y,u):env) = if x == y then u else lookUp x env lookUp x [] = error"lookUp" -- the whnf algorithm fapp :: FVal -> Val -> Val app :: Val -> Val -> Val eval :: Env -> Exp -> Val fapp (x,e,env) u = eval (update env x u) e app (VAbs f) = fapp f app v = VApp v eval env e = case e of Var x -> lookUp x env App e1 e2 -> app (eval env e1) (eval env e2) Let x e1 _ e3 -> eval (update env x (eval env e1)) e3 Type -> VType Abs x e1 -> VAbs (x,e1,env) Pi x a b -> VPi (eval env a) (x,b,env) -- the conversion algorithm; the integer is -- used to represent the introduction of a fresh variable eqVal :: (Int,Val,Val) -> Bool eqVal (k,u1,u2) = case (u1,u2) of (VType,VType) -> True (VApp t1 w1,VApp t2 w2) -> eqVal (k,t1,t2) && eqVal (k,w1,w2) (VGen k1,VGen k2) -> k1 == k2 (VAbs f1,VAbs f2) -> let v = VGen k in eqVal (k+1,fapp f1 v,fapp f2 v) (VPi w1 f1,VPi w2 f2) -> let v = VGen k in eqVal (k,w1,w2) && eqVal (k+1,fapp f1 v,fapp f2 v) _ -> False -- type-checking and type inference checkExp :: (Int,Env,Env) -> Exp -> Val -> Bool inferExp :: (Int,Env,Env) -> Exp -> Val checkType :: (Int,Env,Env) -> Exp -> Bool checkType (k,rho,gamma) e = checkExp (k,rho,gamma) e VType checkExp (k,rho,gamma) e v = case (e,v) of (Abs x e1,VPi w f) -> let v = VGen k in checkExp (k+1,update rho x v,update gamma x w) e1 (fapp f v) (Pi x a b,VType) -> checkType (k,rho,gamma) a && checkType (k+1,update rho x (VGen k),update gamma x (eval rho a)) b (Let x e1 e2 e3,v) -> checkType (k,rho,gamma) e1 && let v1 = eval rho e1 in checkExp (k,rho,gamma) e2 v1 && checkExp (k,update rho x (eval rho e1),update gamma x (eval rho e2)) e3 v _ -> eqVal (k,inferExp (k,rho,gamma) e,v) inferExp (k,rho,gamma) e = case e of Var id -> lookUp id gamma App e1 e2 -> case (inferExp (k,rho,gamma) e1) of VPi w f -> if checkExp (k,rho,gamma) e2 w then fapp f (eval rho e2) else error"application error" _ -> error"application, expected Pi" Type -> VType _ -> error"cannot infer type"