initial commit

Algo.hs

@@ -0,0 +1,201 @@
+{-# LANGUAGE LambdaCase #-}
+module Algo where
+
+import Data.Maybe (fromMaybe)
+import Data.Map (Map)
+import qualified Data.Map as M
+
+import Control.Monad.RWS
+import Control.Monad.Except
+
+import Data.List
+
+type Id = String 
+
+data Exp
+  = Var Id
+  | App Exp Exp
+  | Abs Id Exp
+  | Let Id Exp Exp Exp
+  | Pi Id Exp Exp
+  | Type 
+  deriving Show
+
+data Val
+  = VGen Int 
+  | VApp Val Val
+  | VType
+  | VClos Env Exp 
+  deriving Show
+
+type Env = Map Id Val
+
+data Err
+  = Lookup
+  | ExpectedPi
+  | ExpectedType
+  | NoInfer
+  | AppError
+  deriving Show
+
+data Result = Result (Either Err Bool) [String]
+
+instance Show Result where
+  show (Result r s) = header <> "\n" <> intercalate "\n" s
+    where header = case r of
+                     Left e -> show e
+                     Right True  -> "Checked successfully!"
+                     Right False -> "Types do not match!"
+
+type Conv  = ExceptT Err (RWS Env [String] Int)
+type Check = ExceptT Err (RWS (Env, Env) [String] Int)
+
+li :: Conv a -> Check a
+li conv = do
+  state   <- get
+  (env,_) <- ask
+  let (a, s, w) = runRWS (runExceptT conv) env state
+  put s
+  tell w
+  case a of
+    Left e  -> throwError e
+    Right v -> pure v
+
+maybeConv :: MonadError e m => e -> Maybe a -> m a
+maybeConv _ (Just a) = pure a
+maybeConv e Nothing  = throwError e
+
+lookupEnv :: Id -> Conv Val
+lookupEnv x = ask >>= maybeConv Lookup . M.lookup x
+
+insertEnv :: Id -> Val -> Conv a -> Conv a
+insertEnv x v = local (M.insert x v)
+
+withEnv :: Env -> Conv a -> Conv a
+withEnv = local . const
+
+localCh :: (Env -> Env, Env -> Env) -> Check a -> Check a
+localCh (f,g) = local h
+  where h (a,b) = (f a, g b)
+
+fresh :: (Num i, MonadState i m) => m i
+fresh = do
+  i <- get
+  put (i+1)
+  pure i
+
+app :: Val -> Val -> Conv Val
+app u v = case u of
+            VClos env (Abs x e) -> insertEnv x v (eval e)
+            _                   -> pure (VApp u v)
+
+eval :: Exp -> Conv Val
+eval = \case
+          Var x         -> lookupEnv x
+
+          App e1 e2     -> do
+            e1' <- eval e1
+            e2' <- eval e2
+            app e1' e2'
+
+          Let x e1 _ e3 -> do
+            e1' <- eval e1
+            insertEnv x e1' (eval e3)
+
+          Type          -> pure (VType)
+          e             -> ask >>= pure . (flip VClos) e
+
+whnf :: Val -> Conv Val
+whnf = \case
+          VApp u w    -> do
+            u' <- whnf u
+            w' <- whnf w
+            app u' w'
+          VClos env e -> withEnv env (eval e)
+          v           -> pure v
+
+eqVal :: Val -> Val -> Conv Bool
+eqVal u1 u2 = do
+  u1' <- whnf u1
+  u2' <- whnf u2
+  tell ["checking equality of terms '" <> show u1 <> "' and '" <> show u2 <> "'."]
+  tell ["with value representations '" <> show u1' <> "' and '" <> show u2' <> "'."]
+  case (u1', u2') of
+    (VType, VType) -> pure True
+    (VApp t1 w1, VApp t2 w2) -> (&&) <$> eqVal t1 t2 <*> eqVal w1 w2
+    (VGen k1, VGen k2) -> pure (k1 == k2)
+
+    (VClos env1 (Abs x1 e1), VClos env2 (Abs x2 e2)) -> do
+      v <- VGen <$> fresh
+      eqVal (VClos (M.insert x1 v env1) e1)
+            (VClos (M.insert x2 v env2) e2)
+
+    (VClos env1 (Pi x1 a1 b1), VClos env2 (Pi x2 a2 b2)) -> do
+      v <- VGen <$> fresh
+      (&&) <$> eqVal (VClos env1 a1)
+                     (VClos env2 a2)
+           <*> eqVal (VClos (M.insert x1 v env1) b1)
+                     (VClos (M.insert x1 v env2) b2)
+    _ -> pure False
+
+checkType :: Exp -> Check Bool
+checkType = (flip checkExp) VType
+
+checkExp :: Exp -> Val -> Check Bool
+checkExp e v' = do
+  v <- li (whnf v')
+  case e of
+    Abs x n ->
+      case v of
+        VClos env (Pi y a b) -> do
+          v <- VGen <$> fresh
+          localCh (M.insert x v, M.insert x (VClos env a))
+            (checkExp n (VClos (M.insert y v env) b))
+
+        _ -> throwError ExpectedPi
+
+    Pi x a b ->
+      case v of
+        VType -> do
+          v <- VGen <$> fresh
+          rho <- fst <$> ask
+          (&&) <$> checkType a <*> localCh (M.insert x v, M.insert x (VClos rho a)) (checkType b)
+
+        _ -> throwError ExpectedType
+
+    Let x e1 e2 e3 -> do
+      etr <- li (eval e1)
+      ety <- li (eval e2)
+      (&&) <$> checkType e2 <*> localCh (M.insert x etr, M.insert x ety) (checkExp e3 v)
+
+    _ -> do 
+      e' <- inferExp e
+      li (eqVal v e')
+
+inferExp :: Exp -> Check Val
+inferExp = \case
+  Var id -> maybeConv Lookup . M.lookup id =<< snd <$> ask
+  App e1 e2 -> 
+    inferExp e1 >>= li . whnf >>= \case
+      VClos env (Pi x a b) -> do
+        rho <- fst <$> ask
+        bool <- checkExp e2 (VClos env a)
+        if bool
+           then pure (VClos (M.insert x (VClos rho e2) env) b)
+           else throwError AppError
+      _ -> throwError ExpectedPi
+  Type -> pure VType
+  _    -> throwError NoInfer
+
+typecheck :: Exp -> Exp -> Result
+typecheck m a = resolve ((&&) <$> checkType a <*> checkExp m (VClos M.empty a))
+  where resolve action = let (r,_,w) = (runRWS (runExceptT action) (M.empty, M.empty) 0)
+                         in Result r w
+
+test1 :: Result
+test1 = typecheck (Abs "A" (Abs "x" (Var "x")))
+                  (Pi "A" Type (Pi "x" (Var "A") (Var "A")))
+
+test2 :: Result
+test2 = typecheck (Abs "A" (Abs "f" (Abs "x" (App (Var "f") (Var "x")))))
+                  (Pi "A" Type (Pi "f" (Pi "_" (Var "A") (Var "A")) (Pi "x" (Var "A") (Var "A"))))

README.md

@@ -0,0 +1,5 @@
+# An algorithm for type-checking dependent types 
+
+A "modern" implementation of algorithm described in Thierry Coquand's paper. This employs some monad nicities compared to the haskell implementation in the paper (and isn't a pdf).
+
+This isn't meant to be "better", it might even be more confusing to you. I wrote this to get more of a feel for checking dependent types.