Calculus of Constructions, normalization-by-evaluation, semantic typechecking (WIP)

CC.hs

data Tm = Var Int | Ann Tm Tm | Abs Tm | App Tm Tm | Pi Tm Tm | Uni
  deriving (Show, Eq)
data Clos = Clos Tm Env
  deriving (Show, Eq)
data Dm = DVar Int | DAbs Clos | DApp Dm Dm | DPi Dm Clos | DUni
  deriving (Show, Eq)
type Env = [Dm]

appd :: Clos -> Dm -> Dm
appd (Clos b e) t = eval (t : e) b

app :: Env -> Clos -> Tm -> Dm
app env c t = appd c (eval env t)

eval :: Env -> Tm -> Dm
eval env Uni = DUni
eval env (Var i) = env !! i
eval env (Ann t ty) = eval env ty
eval env (Abs b) = DAbs (Clos b env)
eval env (Pi t b) = DPi (eval env t) (Clos b env)
eval env (App a b) =
  case eval env a of
    DAbs _ c -> app env c b
    tm -> DApp tm (eval env b)

quote :: Int -> Dm -> Tm
quote k DUni = Uni
quote k (DVar i) = Var (k - (i + 1))
quote k (DAbs (Clos b e)) =
  Abs (quote (k + 1) (eval (DVar k : e) b))
quote k (DPi t (Clos b e)) =
  Pi (quote k t) (quote (k + 1) (eval (DVar k : e) b))
quote k (DApp a b) =
  App (quote k a) (quote k b)

nf :: Tm -> Tm
nf t = quote 0 (eval [] t)

eqtype :: Int -> Dm -> Dm -> Bool
eqtype k DUni DUni = True
eqtype k (DVar i) (DVar j) = i == j
eqtype k (DAbs c) (DAbs t' c') =
  let v = DVar k in
  eqtype (k + 1) (appd c v) (appd c' v)
eqtype k (DAbs t c) t' =
  let v = DVar k in
  eqtype (k + 1) (appd c v) (DApp t' v)
eqtype k t' (DAbs t c) =
  let v = DVar k in
  eqtype (k + 1) (DApp t' v) (appd c v)
eqtype k (DApp a b) (DApp a' b') =
  eqtype k a a' && eqtype k b b'
eqtype k (DPi t c) (DPi t' c') =
  let v = DVar k in
  eqtype k t t' && eqtype (k + 1) (appd c v) (appd c' v)
eqtype _ _ _ = False

index :: Int -> [t] -> Maybe t
index _ [] = Nothing
index 0 (h : _) = return h
index i (_ : t) = index (i - 1) t

assert :: Bool -> Maybe ()
assert b = if b then Just () else Nothing

type TEnv = [(Dm, Dm)]

check :: TEnv -> Int -> Tm -> Dm -> Maybe ()
check env k (Abs b) (Pi t b') =
    let v = DVar k in
    check ((v, t) : env) (k + 1) b (appd b' v)
check env k t ty = do
  ty' <- synth env k t
  assert (eqtype k ty' ty)

synth :: TEnv -> Int -> Tm -> Maybe Dm
synth env k Uni = return DUni
synth env k (Var i) = fmap snd (index i env)
synth env k (Ann t ty) = do
    check env k ty DUni
    let ty = eval (map fst env) ty
    check env k t ty
    return ty
synth env k (Abs t b) = Nothing
synth env k (Pi t b) = do
  check env k t DUni
  check ((DVar k, eval (map fst env) t) : env) (k + 1) b DUni
  return DUni
synth env k (App a b) = do
  ta <- synth env k a
  case ta of
    DPi t c -> do
      check env k b t
      return $ app (map fst env) c b
    _ -> Nothing

term :: Tm
term = App (Ann (Abs $ Abs (Var 0) (Var 0)) (Pi Uni Uni)) Uni

main :: IO ()
main = do
  putStrLn $ show term
  putStrLn $ show $ fmap (quote 0) $ synth [] 0 term
  putStrLn $ show $ nf term