Type Checker

prototype

import Control.Monad
import Control.Monad.Error
import Control.Monad.Identity
import Data.Maybe
import Data.Char
import 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

-- Syntax

type Ref = Int
newtype Scope a = Scope a
 deriving Show

data 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 Show

abstract 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 j

instantiate 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
-- x

parseTerm = readP_to_S pTerm

pTerm = pPi +++ pLam +++
 do a <- skipSpaces >> pSimpleUnit ; as <- many (skipSpaces >> pUnit) ; skipSpaces ; return (foldl1 App (a:as))
pUnit = pType +++ pPi +++ pPrf +++ pLam +++ pSquare +++ pFree +++ parens pTerm
pSimpleUnit = pType +++ pPrf +++ pSquare +++ pFree +++ parens pTerm

pType = do string "*" ; return Type
pPi = 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 isAlpha
binder = 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 ...]

-- Typing

data V
 = VType
 | VPi V (V -> V)
 | VPrf V
 | VLam (V -> V)
 | VSquare V
 | VNeutral N
data N
 = NApp N V
 | NFree Name

VLam f % x = f x
VNeutral n % x = VNeutral (NApp n x)
_ % _ = error "Malformed application"

eval delta xi Type = VType
eval 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 n
eval delta xi (Def d) = fromJust (lookup d xi)
eval delta xi (Bound i) = delta !! i
eval delta xi (Free j) = VNeutral (NFree j)

quote q VType = Type
quote 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 n
nquote q (NApp n v) = App (nquote q n) (quote q v)
nquote q (NFree j) = Free j

abstractV i VType _ = VType
abstractV 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 x
abstractN i (NApp n m) x = abstractN i n x % abstractV i m x
abstractN i (NFree j) x
 | i == j = x
 | otherwise = VNeutral (NFree j)

type Infer = ErrorT String Identity
runInfer :: Infer o -> Either String o
runInfer m = runIdentity (runErrorT m)

conv q gamma VType VType = True
conv 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 _ _ = False
convV 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 _) = True
convV 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 s
convN q gamma (NFree i) (NFree j)
 | i == j = lookup i gamma
convN 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 -> Nothing
convN 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)
  _ -> Nothing

erase = map (\(q,tau) -> (q,eraseV tau))
eraseV (VPrf p) = eraseV p
eraseV sigma = sigma

infer :: Ref -> [(Name, V)] -> [(String, V)] -> T -> Infer V
infer q gamma xi Type = return VType
infer 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 VType
infer q gamma xi (Prf p) = do
 VType <- infer q gamma xi p
 return VType
infer 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 pi
infer 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 + 1

checkType 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 + 1

unstickDefinitions xi Type = Type
unstickDefinitions 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 d
unstickDefinitions xi (Bound j) = Bound j
unstickDefinitions 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 interfacing

repl 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 -> nat
nat =
 [ (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 . Global
natElimV = VLam (\motive -> VLam (\zero -> VLam (\succ -> VLam (\n -> natElim motive zero succ n))))
natElim motive zero succ (VNeutral (NFree (Global "Z"))) = zero
natElim motive zero succ (VNeutral (NApp (NFree (Global "S")) m)) = succ % m % natElim motive zero succ m
natElim 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 t
eq =
 [ (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 y
eqPrfElimType = 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 y
eqElimV = VLam (\a -> VLam (\x -> VLam (\motive -> VLam (\pX -> VLam (\y -> VLam (\eqPrf -> eqElim pX eqPrf))))))
eqElim pX (VNeutral (NApp (NFree (Global "refl")) _)) = pX
eqElim _ _ = 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)))