Implementation of the calculus of constructions

gistfile1.hs

import Control.Monad.State
import Control.Monad.Error
import Control.Applicative

type Sym = Int
data Term = Box Int
          | Star
          | Abs Term (Term -> Term)
          | App Term Term
          | Forall Term (Term -> Term)
          | Temp Term Sym
(#) = App
infixl 9 #
t --> s = Forall t (const s)
infixr 7 -->

-- | Pretty print a term
pretty :: Int -> Term -> String
pretty _ (Box i) = "Box " ++ show i
pretty _ Star    = "Star"
pretty c (Abs ty body) = "\\" ++ show c ++ " : " ++ pretty (c + 1) ty ++ ". " ++ pretty (c + 1) (body $ Temp ty c)
pretty c (App f a) = "(" ++ pretty c f ++ ") (" ++ pretty c a ++ ")"
pretty c (Forall ty body) = "forall " ++ show c ++ " : " ++ pretty (c + 1) ty ++ ". " ++ pretty (c + 1) (body $ Temp ty c)
pretty _ (Temp _ i) = show i

instance Show Term where
  show = pretty 0

data TypeError = Mismatch Term Term
               | NoSuchName Sym
               | IllegalQuant Term Term
               deriving Show

instance Error TypeError
type TypeCheck = ErrorT TypeError (State Int)

relations :: [(Term, Term)]  -- A pair (s1, s2) means that (forall x : s1. p x : s2) : s2
relations = [ (Star, Star) , (Star, Box 0) , (Box 0, Star) , (Box 0, Box 0) , (Box 0, Box 1)]

-- | Inductive equivalence relation across terms
equiv :: Term -> Term -> TypeCheck Bool
equiv (Box i) (Box j) = return $ i == j
equiv Star Star = return True
equiv (Abs ty f) (Abs _ f') = fresh ty >>= \a -> f a `equiv` f' a
equiv a1@(App f a) a2@(App g b) = simple a1 `equiv` simple a2 -- Beta conversion
equiv (Forall ty f) (Forall _ g) = fresh ty >>= \a -> f a `equiv` g a
equiv (Temp _ i) (Temp _ j) = return $ i == j
equiv _ _ = return False

-- | Generate a fresh temp
fresh :: Term -> TypeCheck Term
fresh ty = modify (+1) >> fmap (Temp ty) get 

-- | Substitue a Temp `i`, the first int is a generator for new temps.
subst :: Int {- Count -} -> Int {- Target for substitution -} -> Term {- Replacement term -} -> Term -> Term
subst c i e (Temp _ j) | i == j = e
subst c i e (Abs ty body) = Abs (subst c i e ty) $ \a ->
  subst (c - 1) c a -- substitue the temp
  $ subst (c - 1) i e (body $ Temp ty c) -- substitute the original exp
subst c i e (App f a) = subst c i e f `App` subst c i e a
subst c i e (Forall ty body) = Forall (subst c i e ty) $ \a ->
  subst (c - 1) c a -- substitue the temp
  $ subst (c - 1) i e (body $ Temp ty c) -- substitute the original exp, we unHOAS it
subst _ _ _ a = a

-- | Check that a quantification is sane
quantCheck :: Term -> TypeCheck ()
quantCheck (Forall arg body) = do
  resT <- fresh arg >>= typeCheck . body
  argT <- typeCheck arg
  sane <- fmap or . forM relations $ \ (a, r) ->
    liftM2 (&&) (equiv argT a) (equiv resT r)
  when (not sane) $ throwError (IllegalQuant argT resT)

-- | Beta convert in the most trivial way possible
simple (App f a) = let (Abs _ f') = simple f in f' a
simple a = a

-- | Typecheck a given term
typeCheck :: Term -> TypeCheck Term
typeCheck (Temp ty _) = return ty
typeCheck (Box i) = return $ Box (i + 1)
typeCheck Star    = return $ Box 0
typeCheck (Abs ty body) = do
  _ <- typeCheck ty --Assert the sanity of the type annotation
  temp@(Temp _ i) <- fresh ty
  resT <- typeCheck (body temp)
  let f =  Forall ty (\a -> subst (-1) i a resT)
  quantCheck f
  return f
typeCheck (App f a) = do
  fTy <- typeCheck f
  aTy <- typeCheck a
  case simple fTy of
    Forall argTy resT -> do
        match <- argTy `equiv` aTy
        if match
          then return (resT a)
          else throwError $ Mismatch argTy aTy
    _        -> throwError $ Mismatch fTy (Forall aTy id)
typeCheck (Forall argT body) = do
  typeCheck argT >> quantCheck (Forall argT body)
  fresh argT >>= typeCheck . body

typeOf :: Term -> Either TypeError Term
typeOf = flip evalState 0 . runErrorT . typeCheck