Minimal Type Theory with Universes and Pi Types.

Minimal.hs

module Minimal where

-- http://math.andrej.com/2012/11/08/how-to-implement-dependent-type-theory-i

import Control.Monad.Except
import Control.Monad.Reader

type Name = String

data Expr
    = Var Name
    | Lam Name Expr Expr
    | Pi Name Expr Expr
    | App Expr Expr
    | Universe Int
    deriving (Eq, Show)

-- Maps variables to types and (optional) definitions.
type Context = [(Name, (Expr, Maybe Expr))]

subst :: Name -> Expr -> Expr -> Expr
subst v e (Var v')
    | v == v' = e
subst v e (Lam v' ta b)
    | v == v'   = Lam v' (subst v e ta) b
    | otherwise = Lam v' (subst v e ta) (subst v e b)
subst v e (Pi v' ta tb)
    | v == v'   = Pi v' (subst v e ta) tb
    | otherwise = Pi v' (subst v e ta) (subst v e tb)
subst v e (App f a) = App (subst v e f) (subst v e a)
subst _ _ e         = e

ext :: Name -> Expr -> Context -> Context
ext v t ctx = (v, (t, Nothing)) : ctx

type Eval = ExceptT String (Reader Context)

eval :: Expr -> Eval Expr
eval e = check e >> normalize e

check :: Expr -> Eval Expr
check e = go e >>= normalize
    where
    go (Var v) = do
        ctx <- ask
        case fst <$> lookup v ctx of
            Just t  -> return t
            Nothing -> throwError $ "Unbound variable: " ++ v

    go (Lam v ta b) = do
        u  <- check ta
        tb <- local (ext v ta) $ go b
        case u of
            Universe _ -> return $ Pi v ta tb
            _          -> throwError $ "The type of `" ++ show ta ++ "` is not an universe."

    go (Pi v ta tb) = do
        ua <- check ta
        ub <- local (ext v ta) $ check tb
        case (ua, ub) of
            (Universe a, Universe b) -> return $ Universe (max a b)
            (Universe a, _)          -> throwError $ "`" ++ show ub ++ "` is not an universe."
            _                        -> throwError $ "`" ++ show ua ++ "` is not an universe."

    go (App f a) = do
        (v, ta, tb) <- do
            e <- check f
            case e of
                Pi v ta tb -> return (v, ta, tb)
                _          -> throwError $ "`" ++ show f ++ "` is not a function."
        ta  <- normalize ta
        ta' <- check a
        if ta `equiv` ta'
            then return $ subst v a tb
            else throwError $ "Cannot match `" ++ show ta ++ "` with `" ++ show ta' ++ "`"

    go (Universe u) = return $ Universe (u + 1)

normalize :: Expr -> Eval Expr
normalize (Var v) = do
    ctx <- ask
    case lookup v ctx of
        Just (t, e) -> case e of
            Just e  -> normalize e
            Nothing -> return $ Var v
        Nothing     -> throwError $ "Unbound variable: " ++ v
normalize (Lam v ta b) = do
    ta <- normalize ta
    b  <- local (ext v ta) $ normalize b
    return $ Lam v ta b
normalize (Pi v ta tb) = do
    ta <- normalize ta
    tb <- local (ext v ta) $ normalize tb
    return $ Pi v ta tb
normalize (App f a) = do
    f <- normalize f
    a <- normalize a
    case f of
        Lam v ta b -> normalize (subst v a b)
        _          -> return $ App f a
normalize (Universe u) = return $ Universe u

equiv :: Expr -> Expr -> Bool
equiv = go 0
    where
    go n (Lam v ta b0) (Lam v' ta' b0') =
        let b  = subst v (Var (show n)) b0
            b' = subst v' (Var (show n)) b0'
        in go n ta ta' && go (n + 1) b b'

    go n (Pi v ta tb0) (Pi v' ta' tb0') =
        let tb  = subst v (Var (show n)) tb0
            tb' = subst v' (Var (show n)) tb0'
        in go n ta ta' && go (n + 1) tb tb'

    go n (App f a) (App f' a') = go n f f' && go n a a'

    -- Variables, universes, and everything else.
    go _ e e' = e == e'

test :: Expr -> Expr
test e = case flip runReader [] $ runExceptT $ eval e of
    Left e  -> error e
    Right e -> e