## Friday, 27 March 2009

### Type Checker

prototype

import Control.Monadimport Control.Monad.Errorimport Control.Monad.Identityimport Data.Maybeimport Data.Charimport Text.ParserCombinators.ReadP-- Proof irrelevance is implemented by:----   erase(Gamma) |- phi : P--   ----------------------- Prf--   Gamma |- []phi : Prf(P)----   []phi =def []psi : Prf(_)---- Allow eliminations like P(x) -> Prf(x = y) -> P(y)-- along the same schema as Coqs Prop sort, this gives us Axiom K.-- * I am not a number: I am a free variable-- * Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory-- * Intensionality, extensionality, and proof irrelevance in modal type theory-- Syntaxtype Ref = Intnewtype Scope a = Scope a deriving Showdata Name = Local Ref | Global String   deriving (Eq, Show)data T = Type | Pi T (Scope T) | Prf T | Lam T (Scope T) | Square T | App T T | Def String | Bound Ref | Free Name   deriving Showabstract x expr = Scope (rip 0 expr) where rip i Type = Type rip i (Pi tau (Scope sigma)) = Pi (rip i tau) (Scope (rip (i+1) sigma)) rip i (Prf p) = Prf (rip i p) rip i (Lam tau (Scope sigma)) = Lam (rip i tau) (Scope (rip (i+1) sigma)) rip i (Square s) = Square (rip i s) rip i (App m n) = App (rip i m) (rip i n) rip i (Def d) = Def d rip i (Bound j) = Bound j rip i (Free j)  | x == j = Bound i  | otherwise = Free jinstantiate y (Scope expr) = shove 0 expr where shove i Type = Type shove i (Pi tau (Scope sigma)) = Pi (shove i tau) (Scope (shove (i+1) sigma)) shove i (Prf p) = Prf (shove i p) shove i (Lam tau (Scope sigma)) = Lam (shove i tau) (Scope (shove (i+1) sigma)) shove i (Square s) = Square (shove i s) shove i (App m n) = App (shove i m) (shove i n) shove i (Def d) = Def d shove i (Bound j)  | i == j = y  | otherwise = Bound j shove i (Free j) = Free j-- Parsing-- *-- /\(x:T),x-- Prf(P)-- \(x:T),x-- []P-- T T-- xparseTerm = readP_to_S pTermpTerm = pPi +++ pLam +++ do a <- skipSpaces >> pSimpleUnit ; as <- many (skipSpaces >> pUnit) ; skipSpaces ; return (foldl1 App (a:as))pUnit = pType +++ pPi +++ pPrf +++ pLam +++ pSquare +++ pFree +++ parens pTermpSimpleUnit = pType +++ pPrf +++ pSquare +++ pFree +++ parens pTermpType = do string "*" ; return TypepPi = do string "/\\" ; (x, t) <- binder ; string "," ; b <- pTerm ; return (Pi t (abstract x b))pPrf = do string "Prf" ; m <- parens pTerm ; return (Prf m)pLam = do string "\\" ; (x, t) <- binder ; string "," ; b <- pTerm ; return (Lam t (abstract x b))pSquare = do string "[]" ; m <- pTerm ; return (Square m)pFree = do a <- name ; guard (a /= "Prf") ; return (Free (Global a))name = munch1 isAlphabinder = b +++ parens b where b = do a <- name ; string ":" ; x <- pTerm ; return (Global a,x)parens p = do string "(" ; r <- p ; string ")" ; return r-- bug 1:       (\x:*,\y:*,x y)--   parses as: (\x:*,(\y:*,(x y)))--          or: (\x:*,(\y:*,x) y)--          or: ((\x:*,\y:*,x) y)-- fix: introduced 'simple' units and changed pTerm--      from being applications of [unit unit ...] to [simpleUnit unit ...]-- Typingdata V = VType | VPi V (V -> V) | VPrf V | VLam (V -> V) | VSquare V | VNeutral Ndata N = NApp N V | NFree NameVLam f % x = f xVNeutral n % x = VNeutral (NApp n x)_ % _ = error "Malformed application"eval delta xi Type = VTypeeval delta xi (Pi tau (Scope sigma)) = VPi (eval delta xi tau) (\x -> eval (x:delta) xi sigma)eval delta xi (Prf p) = VPrf (eval delta xi p)eval delta xi (Lam _ (Scope f)) = VLam (\x -> eval (x:delta) xi f)eval delta xi (Square s) = VSquare (eval delta xi s)eval delta xi (App m n) = eval delta xi m % eval delta xi neval delta xi (Def d) = fromJust (lookup d xi)eval delta xi (Bound i) = delta !! ieval delta xi (Free j) = VNeutral (NFree j)quote q VType = Typequote q (VPi tau sigmaF) = Pi (quote q tau) (abstract (Local q) (quote (q+1) (sigmaF (VNeutral (NFree (Local q))))))quote q (VPrf p) = Prf (quote q p)quote q (VLam f) = Lam Type (abstract (Local q) (quote (q+1) (f (VNeutral (NFree (Local q))))))quote q (VSquare s) = Square (quote q s)quote q (VNeutral n) = nquote q nnquote q (NApp n v) = App (nquote q n) (quote q v)nquote q (NFree j) = Free jabstractV i VType _ = VTypeabstractV i (VPi tau sigmaF) o = VPi (abstractV i tau o) (\e -> abstractV i (sigmaF e) o)abstractV i (VPrf p) x = VPrf (abstractV i p x)abstractV i (VLam sigmaF) o = VLam (\e -> abstractV i (sigmaF e) o)abstractV i (VSquare s) x = VSquare (abstractV i s x)abstractV i (VNeutral n) x = abstractN i n xabstractN i (NApp n m) x = abstractN i n x % abstractV i m xabstractN i (NFree j) x | i == j = x | otherwise = VNeutral (NFree j)type Infer = ErrorT String IdentityrunInfer :: Infer o -> Either String orunInfer m = runIdentity (runErrorT m)conv q gamma VType VType = Trueconv q gamma (VPi tau sigmaF) (VPi tau' sigmaF') = conv q gamma tau tau' && conv (q+1) ((Local q, tau):gamma) (sigmaF x) (sigmaF' x) where  x = VNeutral (NFree (Local q))conv q gamma (VPrf p) (VPrf p') = conv q gamma p p'conv q gamma (VNeutral n) (VNeutral m) = maybe False (const True) (convN q gamma n m)conv q gamma _ _ = FalseconvV q gamma f g (VPi tau sigmaF) = convV (q+1) ((Local q, tau):gamma) (f % x) (g % x) (sigmaF x) where x = VNeutral (NFree (Local q))convV q gamma _ _ (VPrf _) = TrueconvV q gamma (VNeutral n) (VNeutral m) _ = maybe False (const True) (convN q gamma n m)convV q gamma t s VType = conv q gamma t sconvN q gamma (NFree i) (NFree j) | i == j = lookup i gammaconvN q gamma (NApp f x) (NApp g y) = do VPi tau sigmaF <- convN q gamma f g case convV q gamma x y tau of  True -> Just (sigmaF x)  False -> NothingconvN q gamma n m = do case (convN q gamma n n, convN q gamma m m) of  (Just (VPrf p), Just (VPrf p')) | conv q gamma (VPrf p) (VPrf p') -> Just (VPrf p)  _ -> Nothingerase = map (\(q,tau) -> (q,eraseV tau))eraseV (VPrf p) = eraseV peraseV sigma = sigmainfer :: Ref -> [(Name, V)] -> [(String, V)] -> T -> Infer Vinfer q gamma xi Type = return VTypeinfer q gamma xi (Pi tau scopeSigma) = do VType <- infer q gamma xi tau VType <- infer (q+1) ((Local q, VType):gamma) xi (instantiate (Free (Local q)) scopeSigma) return VTypeinfer q gamma xi (Prf p) = do VType <- infer q gamma xi p return VTypeinfer q gamma xi (Lam tau scopeM) = do VType <- infer q gamma xi tau tau' <- return $eval [] xi tau sigmaF <- infer (q+1) ((Local q, tau'):gamma) xi (instantiate (Free (Local q)) scopeM) pi <- return$ VPi tau' (abstractV (Local q) sigmaF) return piinfer q gamma xi (Square s) = do p <- infer q (erase gamma) xi s -- How do local definitions relate to erasure? return (VPrf p)infer q gamma xi (App m n) = do pi <- infer q gamma xi m case pi of  VPi sigma tauF -> do   sigma' <- infer q gamma xi n   case conv q gamma sigma sigma' of    True -> return (tauF (eval [] xi n))    False -> throwError (unlines [ "Type error in application: "                                 , " expected: " ++ show (quote q sigma)                                 , " received: " ++ show (quote q sigma')                                 ])  _ -> throwError "Nonfunctional application"infer q gamma xi (Def d) = do infer q gamma xi (Free (Global d))infer q gamma xi (Bound _) = do throwError "Encountered a bound variable"infer q gamma xi (Free j) = do case lookup j gamma of  Just tau -> return tau  Nothing -> case j of   Local _ -> throwError "Free local variable"   Global j -> throwError ("Free global variable: " ++ j)inferType gamma xi t = case runInfer (infer q gamma xi t) of  Left err -> Left err  Right tau -> Right (quote q tau) where q = length gamma + 1checkType gamma xi t tau = case runInfer (infer q gamma xi t) of  Left err -> Left err  Right tau' -> Right (conv q gamma tau tau') where q = length gamma + 1unstickDefinitions xi Type = TypeunstickDefinitions xi (Pi t (Scope b)) = Pi (unstickDefinitions xi t) (Scope (unstickDefinitions xi b))unstickDefinitions xi (Prf p) = Prf (unstickDefinitions xi p)unstickDefinitions xi (Lam t (Scope b)) = Lam (unstickDefinitions xi t) (Scope (unstickDefinitions xi b))unstickDefinitions xi (Square p) = Square (unstickDefinitions xi p)unstickDefinitions xi (App m n) = App (unstickDefinitions xi m) (unstickDefinitions xi n)unstickDefinitions xi (Def d) = Def dunstickDefinitions xi (Bound j) = Bound junstickDefinitions xi (Free (Local j)) = Free (Local j)unstickDefinitions xi (Free (Global g)) = case lookup g xi of   Nothing -> Free (Global g)  Just _ -> Def g-- TODO: that was silly, find a sensible fold for T-- User interfacingrepl gamma xi = do putStr "> " line <- getLine case parseTerm line of  [] -> putStrLn "No parse"  [(t,"")] -> case inferType gamma xi (unstickDefinitions xi t) of                Left err -> putStrLn err                Right ty -> print ty  [(_,stuff)] -> putStrLn ("extra stuff at end of line: " ++ stuff)  ambiguous -> putStrLn ("ambiguous parse: " ++ show (length ambiguous) ++ " alternatives") repl gamma xi-- Examples/Toys-- nat : *; Z : nat; S : nat -> natnat = [ (Global "nat", VType) , (Global "Z", zType) , (Global "S", sType) , (Global "natElim", natElimType) ]natDefs = [ ("natElim", natElimV) ]zType = VNeutral (NFree (Global "nat"))sType = VPi (VNeutral (NFree (Global "nat"))) (\_ -> VNeutral (NFree (Global "nat")))natElimType = VPi (VPi (VNeutral (nfree "nat")) (\_ -> VType)) (\p ->               -- forall P : nat -> Type,               VPi (p % (VNeutral (nfree "Z"))) (\_ ->                               -- P 0 ->                VPi (VPi (VNeutral (nfree "nat")) (\n ->                              -- (forall n : nat,                         VPi (p % n) (\_ -> (p % (VNeutral (nfree "S") % n))))) (\_ -> -- P n -> P (S n)) ->                 VPi (VNeutral (nfree "nat")) (\n -> p % n))))                          -- forall n : nat, P n where nfree = NFree . GlobalnatElimV = VLam (\motive -> VLam (\zero -> VLam (\succ -> VLam (\n -> natElim motive zero succ n))))natElim motive zero succ (VNeutral (NFree (Global "Z"))) = zeronatElim motive zero succ (VNeutral (NApp (NFree (Global "S")) m)) = succ % m % natElim motive zero succ mnatElim motive zero succ stuck = VNeutral (NFree (Global "natElim")) % motive % zero % succ % stuck-- add : Pi (Free (Global "nat")) (Scope (Pi (Free (Global "nat")) (Scope (Free (Global "nat")))))--  := (\(x:nat),\(y:nat),natElim (\(n:nat),nat) x (\(T:nat),S) y)add = [ (Global "add", addType) ]addDefs = [ ("add", addValue) ]addType = VPi (VNeutral (NFree (Global "nat"))) (\_ ->            VPi (VNeutral (NFree (Global "nat"))) (\_ ->             VNeutral (NFree (Global "nat"))))addValue = VLam (\x -> VLam (\y ->  natElimV % (VLam (\_ -> VNeutral (NFree (Global "nat")))) % y % (VLam (\_ -> VNeutral (NFree (Global "S")))) % x))-- eq : /\T:*, T -> T -> *; refl : /\T:*,/\t:T, eq T t teq = [ (Global "eq", VPi VType (\t -> VPi t (\_ -> VPi t (\_ -> VType)))) , (Global "refl", reflType) , (Global "eqElim", eqElimType) , (Global "eqPrfElim", eqPrfElimType) -- eq has only one constructor so allow Proof eliminations ]eqDefs = [ ("eqElim", eqElimV) , ("eqPrfElim", eqElimV) ]reflType = VPi VType (\t -> VPi t (\t' -> VNeutral (NFree (Global "eq")) % t % t' % t'))eqElimType = VPi VType (\a -> VPi a (\x -> VPi (VPi a (\_ -> VType)) (\p -> -- forall (A : Type) (x : A) (P : A -> Type),              VPi (p % x) (\_ -> VPi a (\y -> -- P x -> forall y : A,               VPi (VNeutral (NFree (Global "eq")) % a % x % y) (\_ -> p % y)))))) -- x = y -> P yeqPrfElimType = VPi VType (\a -> VPi a (\x -> VPi (VPi a (\_ -> VType)) (\p -> -- forall (A : Type) (x : A) (P : A -> Type),                 VPi (p % x) (\_ -> VPi a (\y -> -- P x -> forall y : A,                  VPi (VPrf (VNeutral (NFree (Global "eq")) % a % x % y)) (\_ -> p % y)))))) -- Prf(x = y) -> P yeqElimV = VLam (\a -> VLam (\x -> VLam (\motive -> VLam (\pX -> VLam (\y -> VLam (\eqPrf -> eqElim pX eqPrf))))))eqElim pX (VNeutral (NApp (NFree (Global "refl")) _)) = pXeqElim _ _ = error "not implemented"-- Example session:---- Main> repl (nat ++ add ++ eq) (natDefs ++ addDefs ++ eqDefs)---- -- join for the Prf monad:---- > \P:*,\phi:Prf(Prf(P)),[]phi-- Pi Type (Scope (Pi (Prf (Prf (Bound 0))) (Scope (Prf (Bound 1)))))---- -- proof of eq symmetry:---- > (\T:*,\a:T,\b:T,\e:eq T a b,eqElim T a (\x:T,eq T x a) (refl T a) b e)-- Pi Type (Scope (Pi (Bound 0) (Scope (Pi (Bound 1) (Scope (Pi (App (App (App (Free (Global "eq")) (Bound 2)) (Bound 1)) (Bound 0)) (Scope (App (App (App (Free (Global "eq")) (Bound 3)) (Bound 1)) (Bound 2)))))))))---- -- that is: /\T:*,/\a:T,/\b:T,/\(a = b),b = a---- proof of f_equal, x = y -> f x = f y---- > (\x:nat,\y:nat,\f:(/\n:nat,nat),\e:eq nat x y,eqElim nat x (\y:nat,eq nat (f x) (f y)) (refl nat (f x)) y e)-- Pi (Free (Global "nat")) (Scope (--  Pi (Free (Global "nat")) (Scope (--   Pi (Pi (Free (Global "nat")) (Scope (Free (Global "nat")))) (Scope (--    Pi (App (App (App (Free (Global "eq")) (Free (Global "nat"))) (Bound 2)) (Bound 1)) (Scope (--     App (App (App (Free (Global "eq")) (Free (Global "nat"))) (App (Bound 1) (Bound 3))) (App (Bound 1) (Bound 2))))))))))---- Induction proof that: n + 0 = n---- > (natElim (\n:nat,eq nat (add n Z) n) (refl nat Z) (\n:nat,\e:eq nat (add n Z) n,(\x:nat,\y:nat,\f:(/\n:nat,nat),\e:eq nat x y,eqElim nat x (\y:nat,eq nat (f x) (f y)) (refl nat (f x)) y e) (add n Z) n S e))-- Pi (Free (Global "nat")) (Scope (--  App (App (App (Free (Global "eq")) (Free (Global "nat")))--      (App (App (App (App (Free (Global "natElim"))--        (Lam Type (Scope (Free (Global "nat")))))--        (Free (Global "Z")))--        (Lam Type (Scope (Free (Global "S")))))--        (Bound 0)))--      (Bound 0)))