Browse Source

Initial commit

hydraz 1 year ago
commit
24900ea148
21 changed files with 921 additions and 0 deletions
  1. 1 0
      .gitignore
  2. 5 0
      ChangeLog.md
  3. 30 0
      LICENSE
  4. 15 0
      README.md
  5. 2 0
      Setup.hs
  6. 32 0
      default.nix
  7. 25 0
      dtt.cabal
  8. 8 0
      example.dtt
  9. 55 0
      src/Main.hs
  10. 58 0
      src/Parser.hs
  11. 42 0
      src/Parser/Lexer.hs
  12. 236 0
      src/Pretty.hs
  13. 26 0
      src/Syntax.hs
  14. 25 0
      src/Syntax/Pretty.hs
  15. 11 0
      src/Syntax/Refresh.hs
  16. 40 0
      src/Syntax/Subst.hs
  17. 72 0
      src/Types/Context.hs
  18. 37 0
      src/Types/Equality.hs
  19. 87 0
      src/Types/Infer.hs
  20. 38 0
      src/Types/Normalise.hs
  21. 76 0
      src/Types/Unify.hs

+ 1 - 0
.gitignore

@@ -0,0 +1 @@
+dist/

+ 5 - 0
ChangeLog.md

@@ -0,0 +1,5 @@
+# Revision history for dtt
+
+## 0.1.0.0  -- YYYY-mm-dd
+
+* First version. Released on an unsuspecting world.

+ 30 - 0
LICENSE

@@ -0,0 +1,30 @@
+Copyright (c) 2017, hydraz
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of hydraz nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

+ 15 - 0
README.md

@@ -0,0 +1,15 @@
+# dtt
+
+A simple dependent type theory which can be used to verify very simple
+theorems.
+
+`dtt` does not have:
+  - inductive data types (use postulations if possible)
+  - recursive definitions (TODO: a totality checker so we can allow this)
+  - pattern matching
+  - Σ types
+  - a standard library
+
+`dtt` does have:
+  - Π types
+  - unification-based type equality

+ 2 - 0
Setup.hs

@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain

+ 32 - 0
default.nix

@@ -0,0 +1,32 @@
+{ nixpkgs ? import <nixpkgs> {}, compiler ? "default" }:
+
+let
+
+  inherit (nixpkgs) pkgs;
+
+  f = { mkDerivation, base, containers, freer, mtl, parsec, stdenv
+      , these, transformers
+      }:
+      mkDerivation {
+        pname = "dtt";
+        version = "0.1.0.0";
+        src = ./.;
+        isLibrary = false;
+        isExecutable = true;
+        executableHaskellDepends = [
+          base containers freer mtl parsec these transformers
+        ];
+        homepage = "https://amulet.ml/dtt/";
+        description = "A dependent type theory for use in proof checking and the implementation of the Amulet programming language";
+        license = stdenv.lib.licenses.bsd3;
+      };
+
+  haskellPackages = if compiler == "default"
+                       then pkgs.haskellPackages
+                       else pkgs.haskell.packages.${compiler};
+
+  drv = haskellPackages.callPackage f {};
+
+in
+
+  if pkgs.lib.inNixShell then drv.env else drv

+ 25 - 0
dtt.cabal

@@ -0,0 +1,25 @@
+name:                dtt
+version:             0.1.0.0
+synopsis:            A dependent type theory for use in proof checking and the implementation of the Amulet programming language
+homepage:            https://amulet.ml/dtt/
+license:             BSD3
+license-file:        LICENSE
+author:              hydraz
+maintainer:          urn@semi.works
+category:            Development
+build-type:          Simple
+extra-source-files:  ChangeLog.md
+cabal-version:       >=1.10
+
+executable dtt
+  main-is:             Main.hs
+  build-depends:       transformers
+                     , containers
+                     , haskeline
+                     , parsec
+                     , these
+                     , freer
+                     , base
+                     , mtl
+  hs-source-dirs:      src
+  default-language:    Haskell2010

+ 8 - 0
example.dtt

@@ -0,0 +1,8 @@
+postulate Nat : Set 0.
+postulate S : Π(x:Nat) -> Nat.
+postulate Z : Nat.
+
+postulate Eq : Π(α: Set 0) -> Π(a: α) -> Π(b : α) -> Set 0.
+postulate Refl : Π(a : Set 0) -> Eq (Set 0) a a.
+
+(Refl : Eq (Set 0) Z Z)

+ 55 - 0
src/Main.hs

@@ -0,0 +1,55 @@
+module Main where
+
+import Syntax.Subst
+import Syntax.Refresh
+import Syntax
+
+import Types.Normalise
+import Types.Context
+import Types.Infer
+
+import Parser.Lexer
+import Parser
+import Text.Parsec
+
+import Data.These
+
+import System.Environment
+import Text.Printf
+
+import Control.Monad
+
+import Pretty (prettyPrint)
+import Syntax.Pretty ()
+
+main :: IO ()
+main = do
+  [x] <- getArgs
+  prg <- readFile x
+  case runParser program () x prg of
+    Left e -> print e
+    Right prog -> do
+      let x = runCheck empty prog
+      case x of
+        Left (NotFound Infer c v) ->
+          printf "Variable %s not found during inference in context %s\n"
+                 (prettyPrint v) (show c)
+        Left (NotFound Normal c v) ->
+          printf "Variable %s not found during normalisation in context %s\n"
+                 (prettyPrint v) (show c)
+        Left (ExpectedType t) -> printf "Expected type, got %s\n" (prettyPrint t)
+        Left (ExpectedPi t) -> printf "Expected Pi-type, got %s\n" (prettyPrint t)
+        Left (NotEqual a b) -> printf "Can not unify %s with %s\n" (prettyPrint a)
+                                      (prettyPrint b)
+        Left (InconsistentSubsts (var, term2) term1) ->
+          printf "Can not unify %s to %s\nIt has already been unifed to %s\n"
+                 (prettyPrint var) (prettyPrint term2) (prettyPrint term1)
+        Left (Occurs a b) -> printf "Circular term: %s appears in %s\n"
+                                    (prettyPrint a) (prettyPrint b)
+        Right (ctx, typ) -> do
+          forM_ (toList ctx) $ \(v, t) ->
+            case t of
+              These a _ -> printf "%s : %s.\n" (prettyPrint v) (prettyPrint a)
+              This a -> printf "%s : %s.\n" (prettyPrint v) (prettyPrint a)
+              _ -> pure ()
+          printf "it : %s.\n" (prettyPrint typ)

+ 58 - 0
src/Parser.hs

@@ -0,0 +1,58 @@
+{-# LANGUAGE TupleSections #-}
+module Parser where
+
+import Text.Parsec.String
+import Text.Parsec
+import Parser.Lexer
+
+import Syntax
+
+term' :: Parser Term
+term' = set <|> try (parens typeHint) <|> parens term <|> pi <|> lam <|> lett <|> var where
+  set = reserved "Set" *> (Set . fromInteger <$> integer)
+  var = Variable . Name <$> identifier
+  typeHint = do
+    nm <- term
+    colon
+    TypeHint nm <$> term
+  pi = do
+    reserved "Π" <|> reserved "forall"
+    (nm, ty) <- parens $ do
+      nm <- Name <$> identifier
+      colon
+      (nm,) <$> term
+    reservedOp "->"
+    Pi nm ty <$> term
+  lam = do
+    reservedOp "\\"
+    (nm, ty) <- parens $ do
+      nm <- Name <$> identifier
+      colon
+      (nm,) <$> term
+    reservedOp "."
+    Lam nm ty <$> term
+  lett = do
+    reserved "let"
+    nm <- Name <$> identifier
+    reservedOp "="
+    val <- term
+    reservedOp ";"
+    Let nm val <$> term
+
+term = foldl1 App <$> many1 term'
+
+toplevel :: Parser Toplevel
+toplevel = postulate <|> define <|> Eval <$> term where
+  postulate = do
+    reserved "postulate"
+    x <- Name <$> identifier
+    reservedOp ":"
+    Postulate x <$> term
+  define = do
+    reserved "define"
+    x <- Name <$> identifier
+    reservedOp ":="
+    Define x <$> term
+
+program :: Parser Program
+program = sepBy1 toplevel dot

+ 42 - 0
src/Parser/Lexer.hs

@@ -0,0 +1,42 @@
+module Parser.Lexer where
+
+import Text.Parsec.String (Parser)
+import Text.Parsec.Language (haskellDef)
+
+import qualified Text.Parsec.Token as Tok
+
+lexer :: Tok.TokenParser ()
+lexer = Tok.makeTokenParser style where
+  ops = ["->", ".", ";", "\\", "=", ":", ":="]
+  names = ["postulate", "define", "Set", "Π", "let", "forall"]
+  style = haskellDef
+            { Tok.reservedOpNames = ops
+            , Tok.reservedNames = names
+            }
+
+integer :: Parser Integer
+integer = Tok.integer lexer
+
+parens :: Parser a -> Parser a
+parens = Tok.parens lexer
+
+colon :: Parser ()
+colon = pure () <* (Tok.colon lexer)
+
+commaSep :: Parser a -> Parser [a]
+commaSep = Tok.commaSep lexer
+
+semiSep :: Parser a -> Parser [a]
+semiSep = Tok.semiSep lexer
+
+identifier :: Parser String
+identifier = Tok.identifier lexer
+
+reserved :: String -> Parser ()
+reserved = Tok.reserved lexer
+
+reservedOp :: String -> Parser ()
+reservedOp = Tok.reservedOp lexer
+
+dot :: Parser String
+dot = Tok.dot lexer

+ 236 - 0
src/Pretty.hs

@@ -0,0 +1,236 @@
+{-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-}
+{-# LANGUAGE DefaultSignatures #-}
+module Pretty 
+  ( module M
+  , PrettyM, PrettyP, PParam(..), PState(..)
+  , Pretty(..)
+  , runPrinter, runPrinter', runPrettyM
+  , defaults, colourless
+  , prettyPrint, uglyPrint
+  , ppshow
+  , colour
+  , block
+  , step
+  , newline
+  , indented
+  , body
+  , typeClr
+  , kwClr
+  , tvClr
+  , litClr
+  , strClr
+  , opClr
+  , patClr
+  , spcClr
+  , greyOut
+  , delim
+  , width
+  , between
+  , padRight
+  , padRight'
+  , Pretty.local
+  , parens, braces, squares, angles
+  , quotes, dquotes
+  , interleave
+  , (<+>)
+  , str
+  , ppr
+  ) where
+
+import qualified Data.Map as Map
+
+import Control.Monad.RWS.Strict as M hiding (local)
+import Control.Applicative as M
+import Data.List as M
+import Data.Char as M
+
+type PrettyM = RWS PParam String PState
+type PrettyP = PrettyM ()
+
+data PParam
+  = PParam { colours        :: Bool
+           , typeColour     :: String
+           , operatorColour :: String
+           , keywordColour  :: String
+           , patternColour  :: String
+           , stringColour   :: String
+           , typevarColour  :: String
+           , greyoutColour  :: String
+           , literalColour  :: String
+           , specialColour  :: String }
+    deriving (Eq, Show)
+
+newtype PState
+  = PState { indent :: Int }
+  deriving (Eq, Show, Ord)
+
+class Pretty a where
+  pprint :: a -> PrettyP
+  default pprint :: Show a => a -> PrettyP
+  pprint = tell . show
+
+runPrinter :: PParam -> PrettyP -> String
+runPrinter ctx act = let (_, _, ret) = runRWS act ctx (PState 0) in ret
+
+runPrinter' :: PParam -> PState -> PrettyM a -> String
+runPrinter' ct st ac = let (_, _, ret) = runRWS ac ct st in ret
+
+runPrettyM :: PParam -> PState -> PrettyM a -> (a, PState, String)
+runPrettyM ct st ac = runRWS ac ct st
+
+defaults :: PParam
+defaults = PParam { colours = True
+                  , keywordColour  = "\x1b[35m"
+                  , operatorColour = "\x1b[35m"
+                  , literalColour  = "\x1b[1;33m"
+                  , stringColour   = "\x1b[32m"
+                  , typeColour     = "\x1b[34m"
+                  , typevarColour  = "\x1b[0m"
+                  , greyoutColour  = "\x1b[1;30m"
+                  , patternColour  = "\x1b[35m"
+                  , specialColour  = "\x1b[33m" }
+
+colourless :: PParam
+colourless = defaults { colours = False }
+
+prettyPrint :: Pretty a => a -> String
+prettyPrint = runPrinter defaults . pprint
+
+uglyPrint :: Pretty a => a -> String
+uglyPrint = runPrinter colourless . pprint
+
+ppshow :: Pretty a => PParam -> a -> String
+ppshow = (. pprint) . runPrinter
+
+colour :: Pretty a => String -> a -> PrettyP
+colour clr cmb
+  = do x <- asks colours
+       when x (tell clr)
+       y <- pprint cmb
+       when x $ tell "\x1b[0m"
+       return y
+
+block :: Pretty a => Int -> a -> PrettyP
+block st ac
+  = do x <- gets indent
+       put $ PState (x + st)
+       pprint ac
+       put $ PState x
+
+step :: Int -> PrettyP
+step x = modify $ \s -> s { indent = indent s + x }
+
+newline :: PrettyP
+newline
+  = do x <- gets indent
+       tell "\n"
+       tell $ replicate x ' '
+
+indented :: Pretty a => a -> PrettyP
+indented x = newline *> pprint x
+
+body :: Pretty a => [a] -> PrettyP
+body b = block 1 $ mapM_ indented b
+
+typeClr :: Pretty a => a -> PrettyP
+typeClr x = flip colour x =<< asks typeColour
+
+kwClr :: Pretty a => a -> PrettyP
+kwClr x = flip colour x =<< asks keywordColour
+
+tvClr :: Pretty a => a -> PrettyP
+tvClr x = flip colour x =<< asks typevarColour
+
+litClr :: Pretty a => a -> PrettyP
+litClr x = flip colour x =<< asks literalColour
+
+strClr :: Pretty a => a -> PrettyP
+strClr x = flip colour x =<< asks stringColour
+
+opClr :: Pretty a => a -> PrettyP
+opClr x = flip colour x =<< asks operatorColour
+
+patClr :: Pretty a => a -> PrettyP
+patClr x = flip colour x =<< asks patternColour
+
+spcClr :: Pretty a => a -> PrettyP
+spcClr x = flip colour x =<< asks specialColour
+
+greyOut :: Pretty a => a -> PrettyP
+greyOut x = flip colour x =<< asks greyoutColour
+
+delim :: (Pretty a, Pretty b, Pretty c) => a -> b -> c -> PrettyP
+delim s e y = pprint s *> pprint y <* pprint e
+
+width :: Pretty a => a -> PrettyM Int
+width ac = do st  <- get
+              let xs = runPrinter' colourless st $ pprint ac
+               in return $ length xs
+
+between :: (Pretty a, Pretty b, Pretty c) => a -> b -> c -> PrettyP
+between a b c = pprint a >> pprint c >> pprint b
+
+padRight :: Pretty a => a -> Int -> PrettyM String
+padRight ac fl
+  = do st <- get
+       ct <- ask
+       let xs = runPrinter' ct st $ pprint ac
+        in return $ xs ++ replicate (fl - length xs) ' '
+
+padRight' :: Pretty a => a -> Int -> PrettyP
+padRight' ac fl = padRight ac fl >>= pprint
+
+local :: Pretty a => a -> PrettyM String
+local ac
+  = do st <- get
+       ct <- ask
+       let xs = runPrinter' ct st $ pprint ac
+        in return xs
+
+parens, braces, squares, angles :: Pretty a => a -> PrettyP
+parens  = delim "(" ")"
+braces  = delim "{" "}"
+squares = delim "[" "]"
+angles  = delim "<" ">"
+
+quotes, dquotes :: Pretty a => a -> PrettyP
+quotes  = delim "'" "'"
+dquotes = delim "\"" "\""
+
+interleave :: (Pretty a, Pretty b) => b -> [a] -> PrettyP
+interleave x xs = do
+  env <- ask
+  let x' = env `ppshow` x in
+      tell $ intercalate x' $ map (ppshow env) xs
+
+(<+>) :: (Pretty a, Pretty b) => a -> b -> PrettyP
+a <+> b = pprint a >> pprint b
+infixl 3 <+>
+
+str :: Pretty a => a -> PrettyP
+str = delim (greyOut "\"") (greyOut "\"") . strClr
+
+ppr :: Pretty a => a -> IO ()
+ppr = putStrLn . runPrinter defaults . pprint
+
+instance Pretty PrettyP where pprint = id
+instance Pretty String where pprint = tell
+instance Pretty Char   where pprint = tell . (:[])
+instance Pretty a => Pretty (ZipList a) where
+  pprint (ZipList x) = interleave ", " x
+
+instance (Pretty a, Pretty b) => Pretty (Map.Map a b) where
+  pprint mp = do
+    x <- ask
+    braces $ intercalate "," $ map (\(k, v) -> x `ppshow` k ++ " => " ++ x `ppshow` v) $ Map.assocs mp
+
+instance (Pretty a, Pretty b, Pretty c) => Pretty (a, b, c) where
+  pprint (a, b, s) = a <+> s <+> b
+
+instance Pretty a => Pretty (a -> PrettyP, a) where
+  pprint (x, y) = x y
+
+instance Pretty Int
+instance Pretty Double
+instance Pretty Float
+instance Pretty Integer

+ 26 - 0
src/Syntax.hs

@@ -0,0 +1,26 @@
+module Syntax where
+
+-- Used only for clarity. Types and terms are _the same thing_ in dtt
+type Type = Term
+data Term
+  = Variable Var
+  | Set Int -- We have Set k : Set (k + 1)
+  | TypeHint Term Type -- x : t
+  | Pi Var Type Type -- (x : t) -> x
+  | Lam Var Type Term -- \(x : t). x
+  | Let Var Term Term
+  | App Term Term -- a b
+  deriving (Eq, Show, Ord)
+
+data Var
+  = Name String
+  | Refresh String Int
+  deriving (Eq, Show, Ord)
+
+data Toplevel
+  = Postulate Var Type
+  | Define Var Term
+  | Eval Term
+  deriving (Eq, Show, Ord)
+
+type Program = [Toplevel]

+ 25 - 0
src/Syntax/Pretty.hs

@@ -0,0 +1,25 @@
+module Syntax.Pretty where
+
+import Syntax
+import Pretty
+
+instance Pretty Term where
+  pprint (Variable v) = pprint v
+  pprint (Set k) = kwClr "Set " <+> litClr k
+  pprint (App x y) = x <+> " " <+> y
+  pprint (TypeHint x t) = parens $ x <+> opClr " : " <+> t
+  pprint (Pi v t s) = do
+    opClr "Π"
+    parens (v <+> opClr " : " <+> t)
+    opClr " -> " <+> s
+  pprint (Lam v t s) = do
+    opClr "\\" 
+    parens (v <+> opClr " : " <+> t)
+    opClr ". " <+> s
+  pprint (Let v t b) = do
+    kwClr "let " <+> v <+> opClr " = " <+> t
+    opClr "; " <+> b
+
+instance Pretty Var where
+  pprint (Name k) = pprint k
+  pprint (Refresh x _) = pprint x

+ 11 - 0
src/Syntax/Refresh.hs

@@ -0,0 +1,11 @@
+{-# LANGUAGE FlexibleContexts #-}
+module Syntax.Refresh where
+
+import Control.Monad.Freer.Fresh
+import Control.Monad.Freer
+
+import Syntax
+
+refresh :: Member Fresh r => Var -> Eff r Var
+refresh (Name x) = Refresh x <$> fresh
+refresh (Refresh x k) = Refresh x <$> fresh

+ 40 - 0
src/Syntax/Subst.hs

@@ -0,0 +1,40 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE LambdaCase #-}
+module Syntax.Subst where
+
+import Control.Monad.Freer.Fresh
+import Control.Monad.Freer
+
+import qualified Data.Set as S
+import Syntax.Refresh
+import Syntax
+
+freeIn :: Term -> S.Set Var
+freeIn (Variable k) = S.singleton k
+freeIn (Set k) = S.empty
+freeIn (TypeHint x t) = freeIn x `S.union` freeIn t
+freeIn (Pi v t s) = freeIn t `S.union` (freeIn s S.\\ S.singleton v)
+freeIn (Lam v t s) = freeIn t `S.union` (freeIn s S.\\ S.singleton v)
+freeIn (Let v t s) = freeIn t `S.union` (freeIn s S.\\ S.singleton v)
+freeIn (App x y) = freeIn x `S.union` freeIn y
+
+subst :: Member Fresh r => [(Var, Term)] -> Term -> Eff r Term
+subst ss = \case
+  Variable k ->
+    pure $ case lookup k ss of
+             Just v -> v
+             Nothing -> Variable k
+  Set k -> pure (Set k)
+  Pi v t s -> do
+    v' <- refresh v
+    Pi v' <$> subst ss t <*> subst ((v, Variable v'):ss) s
+  Lam v t s -> do
+    v' <- refresh v
+    Lam v' <$> subst ss t <*> subst ((v, Variable v'):ss) s
+  Let v t s -> do
+    v' <- refresh v
+    Let v' <$> subst ss t <*> subst ((v, Variable v'):ss) s
+  App x y -> App <$> subst ss x <*> subst ss y
+
+runSubst :: [(Var, Term)] -> Term -> Term
+runSubst ss t = run $ runFresh' (subst ss t) 0

+ 72 - 0
src/Types/Context.hs

@@ -0,0 +1,72 @@
+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
+module Types.Context
+  ( Context
+  , TypeError(..), Phase(..)
+  , insertType, insertValue, insertBoth
+  , lookupType, lookupValue, lookupBoth
+
+  , fromList, toList
+  , empty )
+  where
+
+import qualified Data.Map.Strict as Map
+import Data.These
+import Syntax
+
+newtype Context
+  = Context { getContext :: Map.Map Var (These Type Term) }
+  deriving Show
+
+insertType :: Context -> (Var, Type) -> Context
+insertType (Context c) (v, t)
+  = Context (Map.alter upd v c) where
+    upd (Just (These _ v)) = Just (These t v)
+    upd (Just (This _)) = Just (This t)
+    upd (Just (That v)) = Just (These t v)
+    upd Nothing = Just (This t)
+
+insertValue :: Context -> (Var, Type) -> Context
+insertValue (Context c) (k, v)
+  = Context (Map.alter upd k c) where
+    upd (Just (These t _)) = Just (These t v)
+    upd (Just (This t)) = Just (These t v)
+    upd (Just (That _)) = Just (That v)
+    upd Nothing = Just (That v)
+
+insertBoth :: Context -> (Var, Type, Term) -> Context
+insertBoth (Context c) (v, t, s)
+  = Context (Map.alter (const . Just $ These t s) v c)
+
+lookupType :: Context -> Var -> Maybe Type
+lookupType = (fst .) . lookupBoth
+
+lookupValue :: Context -> Var -> Maybe Term
+lookupValue = (snd .) . lookupBoth
+
+lookupBoth :: Context -> Var -> (Maybe Type, Maybe Term)
+lookupBoth (Context c) v
+  = case Map.lookup v c of
+      Just (These t v) -> (Just t, Just v)
+      Just (This t) -> (Just t, Nothing)
+      Just (That v) -> (Nothing, Just v)
+      Nothing -> (Nothing, Nothing)
+
+fromList :: [(Var, These Type Term)] -> Context
+fromList = Context . Map.fromList
+
+toList :: Context -> [(Var, These Type Term)]
+toList (Context c) = Map.toList c
+
+empty :: Context
+empty = Context Map.empty
+
+data TypeError
+  = NotFound Phase Context Var
+  | ExpectedType Term
+  | ExpectedPi Type
+  | NotEqual Type Type
+  | InconsistentSubsts (Var, Term) Term
+  | Occurs Var Term
+  deriving (Show)
+
+data Phase = Infer | Normal deriving (Show)

+ 37 - 0
src/Types/Equality.hs

@@ -0,0 +1,37 @@
+{-# LANGUAGE FlexibleContexts #-}
+module Types.Equality where
+
+import qualified Types.Normalise as N
+import Types.Context
+
+import Syntax.Refresh
+import Syntax.Subst
+import Syntax
+
+import Control.Monad.Freer.Exception
+import Control.Monad.Freer.Fresh
+import Control.Monad.Freer
+
+equal :: ( Member (Exc TypeError) r
+         , Member Fresh r )
+      => Context
+      -> Term -> Term
+      -> Eff r Bool
+equal ctx a b =
+  let equality a b = case (a, b) of 
+       (Variable av, Variable bv) -> pure (av == bv)
+       (App x1 y1, App x2 y2) -> (&&) <$> x1 `equality` x2
+                                      <*> y1 `equality` y2
+       (Set x, Set y) -> pure (x == y)
+       (Pi v1 t1 s1, Pi v2 t2 s2)
+        -> do s2' <- subst [(v2, Variable v1)] s2
+              (&&) <$> t1 `equality` t2
+                   <*> s1 `equality` s2'
+       (Lam v1 t1 s1, Lam v2 t2 s2)
+         -> do s2' <- subst [(v2, Variable v1)] s2
+               (&&) <$> t1 `equality` t2
+                    <*> s1 `equality` s2'
+       _ -> pure False
+  in do a' <- N.normalise ctx a
+        b' <- N.normalise ctx b
+        equality a' b'

+ 87 - 0
src/Types/Infer.hs

@@ -0,0 +1,87 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE LambdaCase, TupleSections #-}
+module Types.Infer where
+
+import qualified Types.Normalise as N
+import Types.Equality
+import Types.Context
+import Types.Unify
+
+import Syntax.Refresh
+import Syntax.Subst
+import Syntax
+
+import Control.Monad.Freer.Exception
+import Control.Monad.Freer.Fresh
+import Control.Monad.Freer
+
+import Debug.Trace
+
+infer :: ( Member (Exc TypeError) r
+         , Member Fresh r )
+      => Context
+      -> Term
+      -> Eff r Type
+infer ctx = \case
+  Variable x ->
+    case lookupType ctx x of
+      Just t -> pure t
+      Nothing -> throwError (NotFound Infer ctx x)
+  Set k -> pure . Set . succ $ k
+  TypeHint v t -> do
+    t' <- infer ctx v
+    (t `assertEquality` t') ctx
+    pure t
+  Pi x tx ty -> do
+    k1 <- inferSet ctx tx
+    k2 <- inferSet (insertType ctx (x, tx)) ty
+    pure $ Set (k1 `max` k2)
+  Lam x t b -> do
+    inferSet ctx t
+    Pi x t <$> infer (insertType ctx (x, t)) b
+  Let x t b -> do
+    inferSet ctx t
+    infer (insertType ctx (x, t)) b
+  App e1 e2 -> do
+    t1 <- infer ctx e1
+    case t1 of
+      Pi _ i o -> do
+        t2 <- infer ctx e2
+        (t2 `assertEquality` i) ctx
+        pure o
+      e -> throwError (ExpectedPi e)
+
+assertEquality t1 t2 ctx = do
+  x <- equal ctx t1 t2
+  if x then pure () else do
+    constraints <- unify ctx t1 t2
+    checkConsistent constraints
+
+inferSet :: ( Member (Exc TypeError) r
+            , Member Fresh r )
+         => Context -> Type -> Eff r Int
+inferSet ctx t = do
+  x <- infer ctx t
+  x' <- N.normalise ctx x
+  case x of
+    Set k -> pure k
+    x -> throwError (ExpectedType x)
+
+checkProgram :: ( Member (Exc TypeError) r
+                , Member Fresh r )
+             => Context
+             -> Program 
+             -> Eff r (Context, Type)
+checkProgram ctx (Postulate v t:xs)
+  = checkProgram (insertType ctx (v, t)) xs
+checkProgram ctx (Define v vl:xs)
+  = do ty <- infer ctx vl
+       checkProgram (insertBoth ctx (v, ty, vl)) xs
+checkProgram ctx (Eval t:xs)
+  = (ctx,) <$> infer ctx t
+
+runCheck :: Context -> Program -> Either TypeError (Context, Type)
+runCheck = ((run . runError . flip runFresh' 0) .) . checkProgram
+
+runInfer :: Context -> Term -> Either TypeError Term
+runInfer = ((run . runError . flip runFresh' 0) .) . infer

+ 38 - 0
src/Types/Normalise.hs

@@ -0,0 +1,38 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE LambdaCase #-}
+module Types.Normalise where
+
+import Syntax.Subst
+import Syntax
+
+import Control.Monad.Freer.Exception
+import Control.Monad.Freer.Fresh
+import Control.Monad.Freer
+
+import Types.Context
+
+normalise :: ( Member (Exc TypeError) r
+             , Member Fresh r )
+          => Context
+          -> Term
+          -> Eff r Term
+normalise ctx = \case
+  Variable x ->
+    case lookupValue ctx x of
+      Just t -> pure t
+      Nothing -> pure (Variable x)
+  App x y -> do
+    y' <- normalise ctx y
+    x' <- normalise ctx x
+    case x' of
+      Lam v _ b ->
+        do b' <- (subst [(v,y')] b)
+           normalise ctx b'
+      _ -> pure (App x' y')
+  Set k -> pure (Set k)
+  Pi v t s -> do
+    t' <- normalise ctx t
+    Pi v t' <$> normalise (insertType ctx (v, t')) s
+  Lam v t s -> do
+    t' <- normalise ctx t
+    Lam v t' <$> normalise (insertType ctx (v, t')) s

+ 76 - 0
src/Types/Unify.hs

@@ -0,0 +1,76 @@
+{-# LANGUAGE FlexibleContexts #-}
+module Types.Unify where
+
+import qualified Types.Normalise as N
+import Types.Context
+
+import Syntax.Refresh
+import Syntax.Subst
+import Syntax
+
+import Control.Monad.Freer.Exception
+import Control.Monad.Freer.Fresh
+import Control.Monad.Freer
+
+import qualified Data.Map.Strict as Map
+import qualified Data.Set as Set
+
+import Control.Monad
+
+type Subst = [(Var, Term)]
+
+singleton a b = [(a, b)]
+alpha = [1..] >>= flip replicateM ['a'..'z']
+
+unify :: ( Member (Exc TypeError) r
+         , Member Fresh r )
+      => Context
+      -> Term -> Term
+      -> Eff r Subst
+unify ctx t1 t2 = do
+  t1' <- N.normalise ctx t1
+  t2' <- N.normalise ctx t2
+  case (t1', t2') of
+    (Variable a, Variable b) -> pure $ singleton b (Variable a)
+    (a, Variable b) -> pure $ singleton b a
+    (Variable b, a) -> pure $ singleton b a
+    (App x1 y1, App x2 y2) -> (++) <$> unify ctx x1 x2 <*> unify ctx y1 y2
+    (TypeHint v1 t1, TypeHint v2 t2) -> (++) <$> unify ctx v1 v2
+                                             <*> unify ctx t1 t2
+    (Pi v1 t1 b1, Pi v2 t2 b2) -> do
+      (y, z) <- (,) <$> unify ctx t1 t2 <*> unify ctx b1 b2
+      pure $ singleton v2 (Variable v1) ++ y ++ z
+    (Lam v1 t1 b1, Lam v2 t2 b2) -> do
+      (y, z) <- (,) <$> unify ctx t1 t2 <*> unify ctx b1 b2
+      pure $ singleton v2 (Variable v1) ++ y ++ z
+    (Let v1 t1 b1, Let v2 t2 b2) -> do
+      (y, z) <- (,) <$> unify ctx t1 t2 <*> unify ctx b1 b2
+      pure $ singleton v2 (Variable v1) ++ y ++ z
+    (a, Pi v1 t1 b1) -> do
+      id <- fresh
+      let x = Refresh (alpha !! id) id
+      pi' <- subst [(v1, Variable x)] b1
+      unify ctx a pi'
+    (Pi v1 t1 b1, a) -> do
+      id <- fresh
+      let x = Refresh (alpha !! id) id
+      pi' <- subst [(v1, Variable x)] b1
+      unify ctx pi' a
+    (Set k, Set n) | k == n -> pure []
+    (_, _) -> throwError (NotEqual t1' t2')
+
+checkConsistent :: Member (Exc TypeError) r => Subst -> Eff r ()
+checkConsistent = checkConsistent' Map.empty where
+  checkConsistent' map ((a, b):xs)
+    | Map.member a map
+    , b /= map Map.! a
+    = throwError $ InconsistentSubsts (a, b) (map Map.! a)
+    | otherwise =
+      if a `occurs` b
+         then throwError (Occurs a b)
+         else checkConsistent' (Map.insert a b map) xs
+  checkConsistent' map [] = pure ()
+
+occurs :: Var -> Term -> Bool
+occurs v (Variable k) = False
+occurs v x = v `Set.member` freeIn x