Attempt to create simple dependently typed type inferrer / evaluator.

Context.hs

module Context
    ( T()
    , empty
    , add
    , extend, singleton
    , assign, assignment
    , apply, accumulate
    )
    where

import Data.Foldable

import qualified Data.List as List

import Types

newtype T = Ctx [(Var, Expr, Maybe Expr)]

instance Show T where
    show (Ctx list) = foldr (\a b -> a ++ " |- " ++ b) "[]" (map assignment list)
      where
        assignment (name, ty, Nothing) = show name ++ " : " ++ show ty
        assignment (name, ty, Just it) = show name ++ " : " ++ show ty ++ " = " ++ show it

empty :: T
empty = Ctx []

singleton :: Var -> Expr -> T
singleton name ty = Ctx [(name, ty, Nothing)]

assignment :: Var -> Expr -> Expr -> T
assignment name ty val = Ctx [(name, ty, Just val)]

add :: Var -> Expr -> Maybe Expr -> T -> T
add var ty mval (Ctx t) = Ctx $ (var, ty, mval) : t

extend :: Var -> Expr -> T -> T
extend var ty = add var ty Nothing

assign :: Var -> Expr -> Expr -> T -> T
assign var ty = add var ty . Just

apply :: Monad m => ((Var, Expr, Maybe Expr) -> acc -> m acc) -> T -> acc -> m acc
apply a (Ctx c) b = foldrM a b c

accumulate :: Monad m => T -> acc -> ((Var, Expr, Maybe Expr) -> acc -> m acc) -> m acc
accumulate (Ctx c) b a = foldrM a b c

HasCounter.hs

module HasCounter where

class Monad m => C m where
    next :: m Int

Substituton.hs

module Substitution where

import Types
import qualified Context
import qualified HasCounter

refresh :: HasCounter.C m => Var -> m Var
refresh (Name name _) = do
    Name name <$> HasCounter.next

class C it where
    substitute :: HasCounter.C m => Context.T -> it -> m it

instance C Expr where
    substitute =
        Context.apply $ \(name, ty, _) ->
            fix $ \go expr ->
                let
                    substituteAbstr ((name, ty) :=> res) = do
                        name' <- refresh name
                        let renaming = Context.singleton name (Var name')
                        ty'   <- go ty
                        res'  <- go =<< substitute renaming res
                        return ((name', ty') :=> res')

                in case expr of
                    Var name' | name == name' -> return ty
                    Pi  abs                   -> Pi   <$> substituteAbstr abs
                    Lam abs                   -> Lam  <$> substituteAbstr abs
                    f :$ x                    -> (:$) <$> go f <*> go x
                    other                     -> return other

instance C Context.T where
    substitute ctx dest =
        Context.accumulate dest Context.empty $ \(name, ty, mval) acc -> do
            ty'   <- substitute ctx ty
            mval' <- traverse (substitute ctx) mval
            return $ Context.add name ty' mval' acc

fix f = x where x = f x

Ty.hs

{-# language TemplateHaskell #-}

import Control.Monad.RWS
import Control.Monad.Except
import Control.Monad.Identity

import qualified Data.Map as Map

import Lens.Micro.Platform
import Lens.Micro.TH

import Types
import qualified Context

data InferState = IS
    { _nameCounter :: Int
    }
    deriving (Show)

initialState = IS 0

makeLenses ''InferState

data InferError
    = NoError
    | Undefined Var
    | NotAFunction Expr
    | ExpectedButGot Expr Expr
    | NotAType Expr
    deriving (Show)

data Subst = Subst Var Expr
    deriving (Show)

type Substs = Map.Map Var Expr

type InferM = ExceptT InferError (RWST Context Substs InferState Identity)

runInferM :: InferM a -> (Either InferError a, InferState, Substs)
runInferM = runIdentity . (\act -> runRWST act emptyCtx initialState) . runExceptT

refresh :: Var -> InferM Var
refresh (Name s _) = do
    nameCounter += 1
    nc <- use nameCounter
    return (Name s nc)

subst :: Substs -> Expr -> InferM Expr
subst ss = go
  where
    go expr = case expr of
        Var   name -> return $ Map.lookup name ss `orElse` expr
        Universe _ -> return $ expr
        Pi   abstr -> Pi   <$> substAbstr abstr
        Lam  abstr -> Lam  <$> substAbstr abstr
        f :$ x     -> (:$) <$> go f <*> go x

    substAbstr ((name, ty) :=> res) = do
        newName <- refresh name
        ty      <- go ty
        res     <- subst (Map.insert name (Var newName) ss) res
        return $ (newName, ty) :=> res

infoOf :: Var -> InferM (Expr, Maybe Expr)
infoOf name = do
    preview (at name._Just)
        >>= whenNothing (throwError $ Undefined name)

typeOf :: Var -> InferM Expr
typeOf name = (^._1) <$> infoOf name

valueOf :: Var -> InferM (Maybe Expr)
valueOf name = (^._2) <$> infoOf name

infer :: Expr -> InferM Expr
infer expr = case expr of
    Var   name -> typeOf name
    Universe k -> return $ Universe (k + 1)

    Pi ((n, ty) :=> res) -> do
        k1 <- universe ty
        k2 <- local (Map.insert n (ty, Nothing)) $ universe res
        return $ Universe (max k1 k2)

    Lam ((n, ty) :=> res) -> do
        _ <- universe ty
        res <- local (Map.insert n (ty, Nothing)) $ infer res
        return $ Pi $ (n, ty) :=> res

    f :$ x -> do
        tx <- infer x
        tf <- infer f
        case tf of
            Pi ((arg, tx') :=> res) -> do
                unify tx tx'
                subst (Map.singleton arg x) res

            other -> do
                throwError $ NotAFunction other

universe :: Expr -> InferM Int
universe expr = do
    ty <- infer expr
    ty <- norm ty
    case ty of
        Universe k -> return k
        other      -> throwError $ NotAType other


unify :: Expr -> Expr -> InferM ()
unify e1 e2 = do
    when (e1 /= e2) $ do
        throwError $ ExpectedButGot e2 e1

-------------------------------------------------------------------------------

Just  x `orElse` _ = x
Nothing `orElse` x = x

whenNothing :: Monad m => m a -> Maybe a -> m a
whenNothing other = maybe other return

Types.hs

module Types
    ( Expr  (..)
    , Var   (..), var
    , Abstr (..)
    )
    where

data Expr
    = Var Var
    | Universe Int
    | Pi Abstr
    | Lam Abstr
    | Expr :$ Expr

var :: String -> Var
var = flip Name 0

instance Show Expr where
    showsPrec p expr = case expr of
        Var   name -> showsPrec 10 name
        Universe u -> ("Set" ++) . (showsPrec 10 u)
        Pi   abstr -> showsPrecAbstr " => " abstr
        Lam  abstr -> showsPrecAbstr " -> " abstr
        f :$ x     -> showParen (p >= 8) $ showsPrec 7 f . (" " ++ ) . (showsPrec 8 x)
      where
        showsPrecAbstr arrow ((name, ty) :=> res) =
            showParen (p >= 7) $ showsPrec 10 name . (" : " ++ ) . showsPrec 0 ty . (arrow ++ ) . (showsPrec 0 res)

data Var
    = Name String Int
    deriving (Eq, Ord)

data Abstr
    = (Var, Expr) :=> Expr

instance Show Var where
    show var = case var of
        Name s i -> s ++ "'" ++ show i