An implementation of Martin-Löf's Logical Framework (MLF) with dependent pairs using call-by-name weak head evaluation, untyped conversion and bidirectional type-checking. Author: Andreas Abel Date : Nov 2, 2004 \begin{code} module MLFSigma where import Prelude hiding (const, fst, snd) import Data.FiniteMap import Control.Monad.Error \end{code} Raw expressions. \begin{code} type Name = String data Const = Set | El | Fun | Sig deriving Eq data Exp = Const Const | Var Name | Abs Name Exp | App Exp Exp | Pair Exp Exp | Fst Exp | Snd Exp set = Const Set el t = Const El App t fun x a b = Const Fun App a App (Abs x b) a ==> b = fun "_" a b sig x a b = Const Sig App a App (Abs x b) prod a b = sig "_" a b \end{code} Parameters, closures and values. \begin{code} type Par = Int -- p data Atom = Cst Const | Par Par deriving Eq -- a type Env = FiniteMap Name Clos -- rho data Clos = Atom Par | Clos Exp Env -- w data Proj = L | R deriving Eq -- p data Elim = FunE Clos | PairE Proj -- e \end{code} Values are either neutral, i.e., an atom followed by a list of eliminations, where the last elimination is the head of the list for efficiency reasons. Or, values are introductions. \begin{code} data Val = Ne Atom [Elim] | Lam Name Exp Env | Comma Exp Exp Env -- v atom :: Atom -> Val atom a = Ne a [] const :: Const -> Val const c = atom (Cst c) par :: Par -> Val par p = atom (Par p) \end{code} Call-by-name weak head evaluation. (Always succeeds if rho binds all vars.) \begin{code} eval :: Exp -> Env -> Val eval (Const c) rho = const c eval (Var x) rho = evalClos (lookupWithDefaultFM rho (error "unbound Var") x) eval (Abs x t) rho = Lam x t rho eval (App r s) rho = app (eval r rho) (Clos s rho) eval (Pair r s) rho = Comma r s rho eval (Fst r) rho = fst (eval r rho) eval (Snd r) rho = snd (eval r rho) app :: Val -> Clos -> Val app (Ne a es) w = Ne a (FunE w : es) app (Lam x t rho) w = eval t (addToFM rho x w) app _ _ = error "app: Not a function" fst :: Val -> Val fst (Ne a es) = Ne a (PairE L : es) fst (Comma r s rho) = eval r rho fst _ = error "fst: Not a pair" snd :: Val -> Val snd (Ne a es) = Ne a (PairE R : es) snd (Comma r s rho) = eval s rho snd _ = error "snd: Not a pair" evalClos :: Clos -> Val evalClos (Atom p) = par p evalClos (Clos t rho) = eval t rho \end{code} Monadic Bool. \begin{code} type Result a = Either String a type MBool = Result () true = return () false = fail "" fromBool :: Bool -> MBool fromBool b = if b then true else false eq :: Eq a => a -> a -> MBool eq x y = if (x == y) then true else fail "eq: no match" allM :: (a -> MBool) -> [a] -> MBool allM p = foldl (\ r a -> r >> p a) true \end{code} Untyped conversion. \begin{code} class GenSym a where genSym :: a -> (Par, a) conv :: GenSym a => a -> Val -> Val -> Result () conv g v v' = conv' v v' where conv' :: Val -> Val -> Result () conv' (Ne a es) (Ne a' es') = a eq a' >> allM convE (zip es es') conv' v@(Lam _ _ _) v'@(Lam _ _ _) = conv g' (app v a) (app v' a) conv' v@(Lam _ _ _) v'@(Ne _ _ ) = conv g' (app v a) (app v' a) conv' v@(Ne _ _) v'@(Lam _ _ _) = conv g' (app v a) (app v' a) conv' v@(Comma _ _ _) v'@(Comma _ _ _) = conv' (fst v) (fst v') >> conv' (snd v) (snd v') conv' v@(Ne _ _) v'@(Comma _ _ _) = conv' (fst v) (fst v') >> conv' (snd v) (snd v') conv' v@(Comma _ _ _) v'@(Ne _ _) = conv' (fst v) (fst v') >> conv' (snd v) (snd v') (p,g') = genSym g a = Atom p convE :: (Elim, Elim) -> Result () convE (FunE w, FunE w') = conv' (evalClos w) (evalClos w') convE (PairE p, PairE p') = p eq p' \end{code} Contexts. \begin{code} newtype Counter = Counter Int instance GenSym Counter where genSym (Counter k) = (k, Counter (k+1)) data Cxt = Cxt (FiniteMap Par Val) Counter instance GenSym Cxt where genSym (Cxt cxt k) = (p, Cxt cxt k') where (p, k') = genSym k empty :: Cxt empty = Cxt emptyFM (Counter 0) push :: Cxt -> Val -> (Cxt, Par) push (Cxt cxt g) v = (Cxt cxt' g', p) where (p, g') = genSym g cxt' = addToFM cxt p v get :: Cxt -> Par -> Val get (Cxt cxt g) p = lookupWithDefaultFM cxt (error "parameter not bound") p \end{code} Type checking. \begin{code} isType :: Cxt -> Exp -> Env -> MBool -- Env is just a renaming isType cxt (Const Set) rho = true isType cxt ((Const El) App t) rho = check cxt t rho (const Set) isType cxt (((Const Fun) App r) App (Abs x s)) rho = isType cxt r rho >> isType cxt' s rho' where (cxt', p) = push cxt (eval r rho) rho' = addToFM rho x (Atom p) isType cxt (((Const Sig) App r) App (Abs x s)) rho = isType cxt r rho >> isType cxt' s rho' where (cxt', p) = push cxt (eval r rho) rho' = addToFM rho x (Atom p) isType _ _ _ = fail ("isType: not a valid type") check :: Cxt -> Exp -> Env -> Val -> Result () check cxt (Abs x t) rho (Ne (Cst Fun) [FunE f, FunE w]) = check cxt' t rho' fa where (cxt', p) = push cxt (evalClos w) a = Atom p rho' = addToFM rho x a fa = evalClos f app a check cxt (Pair r s) rho (Ne (Cst Sig) [FunE f, FunE w]) = check cxt r rho (evalClos w) >> check cxt s rho (evalClos f app Clos r rho) check cxt t rho v = do v' <- infer cxt t rho conv cxt v v' infer :: Cxt -> Exp -> Env -> Result Val infer cxt (Var x) rho = case (lookupFM rho x) of Just (Atom p) -> return (get cxt p) _ -> fail ("infer: Variable " ++ x ++ " not bound") infer cxt (App r s) rho = do v <- infer cxt r rho case v of (Ne (Cst Fun) [FunE f, FunE w]) -> check cxt s rho (evalClos w) >> return (evalClos f app Clos s rho) _ -> fail ("infer: Not a function type") infer cxt (Fst r) rho = do v <- infer cxt r rho case v of (Ne (Cst Sig) [FunE f, FunE w]) -> return (evalClos w) _ -> fail ("infer: Not a pair type") infer cxt (Snd r) rho = do v <- infer cxt r rho case v of (Ne (Cst Sig) [FunE f, FunE w]) -> return (evalClos f app Clos (Fst r) rho) _ -> fail ("infer: Not a pair type") infer _ _ _ = fail ("infer: Not a neutral expression") \end{code} Top level. \begin{code} doit :: Exp -> Exp -> Result () doit e t = isType empty t emptyFM >> check empty e emptyFM (eval t emptyFM) \end{code} Successful tests. \begin{code} t1 = doit (Abs "A" (Abs "x" (Var "x"))) (fun "B" set (fun "y" (el (Var "B")) (el (Var "B")))) t2 = doit (Abs "x" (Abs "x" (Var "x"))) (fun "x" set (el (Var "x") ==> el (Var "x"))) t3 = doit (Abs "A" (Abs "B" (Abs "p" (Pair (Fst (Var "p")) (Snd (Var "p")))))) $fun "A" set$ fun "B" set $fun "p" (prod (el (Var "A")) (el (Var "B")))$ prod (el (Var "A")) (el (Var "B")) t4 = doit (Abs "A" (Abs "B" (Abs "p" (Pair (Fst (Var "p")) (Snd (Var "p")))))) $fun "A" set$ fun "B" (el (Var "A") ==> set) $fun "p" (sig "x" (el (Var "A")) (el (Var "B" App Var "x")))$ sig "x" (el (Var "A")) (el (Var "B" App Var "x")) t5 = doit (Abs "A" (Abs "B" (Abs "p" (Pair (Fst (Var "p")) (Snd (Var "p")))))) $fun "A" set$ fun "B" (el (Var "A") ==> set) $fun "p" (sig "x" (el (Var "A")) (el (Var "B" App Var "x")))$ sig "y" (el (Var "A")) (el (Var "B" App Var "y")) \end{code} Failing tests. \begin{code} f1 = doit (Abs "x" (Var "x")) (fun "A" set (el (Var "A") ==> el (Var "A"))) f2 = doit set set f3 = doit (Abs "A" (Abs "x" (Var "x"))) (fun "B" set (fun "y" (el (Var "B")) (el (Var "C")))) f4 = doit (Abs "A" (Abs "B" (Abs "p" (Pair (Fst (Var "p")) (Snd (Var "p")))))) $fun "A" set$ fun "B" set $fun "p" (prod (el (Var "A")) (el (Var "B")))$ prod (el (Var "B")) (el (Var "A")) f5 = doit (Abs "A" (Abs "B" (Abs "p" (Pair (Fst (Var "p")) (Snd (Var "p")))))) $fun "A" set$ fun "B" (el (Var "A") ==> set) $fun "p" (sig "x" (el (Var "A")) (el (Var "B" App Var "x")))$ prod (el (Var "B")) (el (Var "A")) f6 = doit (Abs "A" (Abs "B" (Abs "p" (Pair (Fst (Var "p")) (Snd (Var "p")))))) $fun "A" set$ fun "B" (el (Var "A") ==> set) $fun "p" (sig "x" (el (Var "A")) (el (Var "B" App Var "x")))$ sig "x" (el (Var "A")) (el (Var "B" App Var "y")) \end{code}