型検査は足りてないけど、PHOASやめてdeBruinインデックスに変えた。PHOASみたいにキチガイじみた難しさはないぽ

HoTT2.hs

-- {-# LANGUAGE RankNTypes #-}
--{-# LANGUAGE GADTs #-}
-- {-# LANGUAGE FlexibleInstances #-}
-- {-# LANGUAGE ImpredicativeTypes #-}

-- import Control.Monad.Reader

data Term = TmU Int
          | TmVar Int
          | TmProd Type Term
          | TmAbs Type Term
          | TmApp Term Term
          | TmEq Type Term Term
          | TmRefl Type Term
          | TmEqInd Type Term Term Term Term
          deriving (Show, Eq)

type Type = Term

data Binding = Decl Type
             | Def  Type Term
             deriving (Show, Eq)
type Env = [Binding]

lookupVar :: Env -> Int -> Binding
lookupVar env i = if null bs then err else head bs
  where
    bs = drop i env
    err = error "unbound variable"

termShift :: Int -> Term -> Term
termShift d = walk 0
  where
    walk :: Int -> Term -> Term
    walk c t = case t of
      TmU _ -> t
      TmVar i | i >= c -> TmVar $ i + d
              | otherwise -> t
      TmProd ty body -> TmProd (w ty) (w' body)
      TmAbs  ty body -> TmAbs  (w ty) (w' body)
      TmApp t1 t2 -> TmApp (w t1) (w t2)
      TmEq t1 t2 t3 -> TmEq (w t1) (w t2) (w t3)
      TmRefl t1 t2 -> TmRefl (w t1) (w t2)
      TmEqInd ct a x y p ->
        TmEqInd (walk (c+3) ct) (w' a) (w x) (w y) (w p)
      where
        w  = walk c
        w' = walk (c+1)

termSubst :: Int -> Term -> Term -> Term
termSubst j s = walk 0
  where
    walk :: Int -> Term -> Term
    walk c t = case t of
      TmU _ -> t
      TmVar i | i == j + c -> termShift c s
              | otherwise -> t
      TmProd ty body -> TmProd (w ty) (w' body)
      TmAbs  ty body -> TmAbs  (w ty) (w' body)      
      TmApp  t1 t2 -> TmApp (w t1) (w t2)
      TmEq t1 t2 t3 -> TmEq (w t1) (w t2) (w t3)
      TmRefl t1 t2 -> TmRefl (w t1) (w t2)
      TmEqInd ct a x y p ->
        TmEqInd (walk (c+3) ct) (w' a) (w x) (w y) (w p)
      where
        w  = walk c
        w' = walk (c+1)

reduceValue :: Env -> Term -> Term
reduceValue e = rd
  where
    rd :: Term -> Term
    rd t = case t of
      TmVar v -> case lookupVar e v of
        Decl _ -> t
        Def _ t' -> termShift (v+1) t'
      TmProd ty body ->
        TmProd (rd ty) (reduceValue (Decl ty : e) body)
      TmAbs ty body ->
        TmAbs (rd ty) (reduceValue (Decl ty : e) body)
      TmApp t1 t2 -> case rd t1 of
        TmAbs ty body -> termShift (-1) $ reduceValue (Def ty (rd t2) : e) body
        t1' -> TmApp t1' (rd t2)
      TmEq a x y -> TmEq (rd a) (rd x) (rd y)
      TmRefl a x -> TmRefl (rd a) (rd x)
      TmEqInd ct c x y p -> case rd p of
        TmRefl a z -> termShift (-1) $ reduceValue (Def a x : e) c
        p' -> TmEqInd ct c x y p'
      _ -> t

typeof :: Env -> Term -> Type
typeof e = to
  where
    to :: Term -> Type
    to (TmU i) = TmU $ i + 1
    to (TmVar v) = case lookupVar e v of
      Decl ty -> ty
      Def ty _ -> ty
    to (TmProd ty body) =
      TmU (max uty ubody)
      where uty = univ (to ty)
            ubody = univ (typeof (Decl ty : e) body)
    to (TmAbs ty body) = -- TODO: type check ty
      TmProd ty tbody
      where tbody = typeof (Decl ty : e) body
    to (TmApp t1 t2) = case to t1 of
      TmProd ty body -> -- TODO: typecheck t2 == ty
        termShift (-1) $ reduceValue (Def ty t2 : e) body
      _ -> error "not applicative"
    to (TmEq a x y) = -- TODO: x y : A
      TmU ua
      where ua = univ (to a)
    to (TmRefl a x) =
      TmEq a x x -- TODO: x : A
    to (TmEqInd ct c x y p) = -- TODO: ippai
      termShift (-3) $ reduceValue (Def pt (termShift 2 p) : Def a (termShift 1 y) : Def a x : e) ct
      where pt = to p
            a = to x
    

univ :: Term -> Int
univ (TmU u) = u
univ _ = error "not universe"

r :: IO ()
r = do
  go u0
  go $ prod u0 u0
  go $ abs u0 u0
  go $ abs u0 (v 0)
  go $ TmEq u1 u0 u0
  go $ TmRefl u1 u0

  go
    $ prod u0    -- a : U 0
    $ prod (v 0) -- x : a
    $ prod (v 1) -- y : a
    $ arr (eq (v 2) (v 1) (v 0)) (eq (v 2) (v 0) (v 1))

  go
    $ abs u0    -- a : U 0
    $ abs (v 0) -- x : a
    $ abs (v 1) -- y : a
    $ abs (eq (v 2) (v 1) (v 0)) -- p : x = y
    $ TmEqInd
    ( -- x' : a
      -- y' : a
      -- p' : x' = y'
      eq    -- y' = x'
      (v 6) -- a
      (v 1) -- y'
      (v 2) -- x'
    )
    ( -- x'' : a
      TmRefl (v 4) (v 0)
    )
    (v 2) -- x
    (v 1) -- y
    (v 0) -- p
  -- match p as p' in x' = y' return y' = x' with refl a x'' => refl a x''

  where
    go :: Term -> IO ()
    go t = do
      putStrLn "-----"
      putStrLn (show t)
      putStr "  : "
      putStr $ show $ typeof [] t
      putStrLn ""

    u0 :: Term
    u0 = TmU 0
    u1 :: Term
    u1 = TmU 1

    v = TmVar

    prod = TmProd
    arr a b = TmProd a (termShift 1 b)
    abs = TmAbs
    eq = TmEq
    

result

*Main> r
-----
TmU 0
  : TmU 1
-----
TmProd (TmU 0) (TmU 0)
  : TmU 1
-----
TmAbs (TmU 0) (TmU 0)
  : TmProd (TmU 0) (TmU 1)
-----
TmAbs (TmU 0) (TmVar 0)
  : TmProd (TmU 0) (TmU 0)
-----
TmEq (TmU 1) (TmU 0) (TmU 0)
  : TmU 2
-----
TmRefl (TmU 1) (TmU 0)
  : TmEq (TmU 1) (TmU 0) (TmU 0)
-----
TmProd (TmU 0) (TmProd (TmVar 0) (TmProd (TmVar 1) (TmProd (TmEq (TmVar 2) (TmVar 1) (TmVar 0)) (TmEq (TmVar 3) (TmVar 1) (TmVar 2)))))
  : TmU 1
-----
TmAbs (TmU 0) (TmAbs (TmVar 0) (TmAbs (TmVar 1) (TmAbs (TmEq (TmVar 2) (TmVar 1) (TmVar 0)) (TmEqInd (TmEq (TmVar 6) (TmVar 1) (TmVar 2)) (TmRefl (TmVar 4) (TmVar 0)) (TmVar 2) (TmVar 1) (TmVar 0)))))
  : TmProd (TmU 0) (TmProd (TmVar 0) (TmProd (TmVar 1) (TmProd (TmEq (TmVar 2) (TmVar 1) (TmVar 0)) (TmEq (TmVar 3) (TmVar 1) (TmVar 2)))))