型検査は足りてないけど、型検査が通った場合に返ってくる型は返せるようになった！

HoTT.hs

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

import Control.Monad.Reader hiding (join)

data TermP v where
  TmFamily   :: TermP v -> (v -> TermP v) -> TermP v
  TmSubst    :: TermP v -> TermP v -> TermP v
  TmVar      :: v -> TermP v
  TmU        :: Int -> TermP v
  TmProd     :: TermP v -> TermP v
  TmAbs      :: TermP v -> TermP v
  TmApp      :: TermP v -> TermP v -> TermP v
  TmSigma    :: TermP v -> TermP v
  TmPair     :: TermP v -> TermP v -> TermP v -> TermP v
  TmSigmaInd :: TermP v -> TermP v -> TermP v -> TermP v
  TmEq       :: TermP v -> TermP v -> TermP v -> TermP v
  TmRefl     :: TermP v -> TermP v -> TermP v
  TmEqInd    :: TermP v -> TermP v -> TermP v -> TermP v -> TermP v -> TermP v
  {-
  TmCoprod   :: Term -> Term -> TermP v
  TmInLeft   :: Term -> TermP v
  TmInRight  :: Term -> TermP v
  TmCoprodInd :: Family -> Family -> Family -> Term -> TermP v
  TmZero :: TermP v
  TmZeroInd :: Family -> Term -> TermP v
  TmOne  :: TermP v
  TmPt   :: TermP v
  TmOneInd :: Family -> Family -> Term -> TermP v
-}

type Term = forall a. TermP a

data Binding v where
  BindDecl :: TermP v -> TermP v -> Binding v
  BindDef  :: TermP v -> TermP v -> Binding v

valueOfBinding :: Binding v -> TermP v
valueOfBinding (BindDecl v _) = v
valueOfBinding (BindDef v _) = v

typeOfBinding :: Binding v -> TermP v
typeOfBinding (BindDecl _ t) = t
typeOfBinding (BindDef _ t) = t

hasSubst :: TermP a -> Bool
hasSubst (TmSubst _ _) = True
hasSubst (TmFamily a f) = hasSubst a || hasSubst (f undefined)
hasSubst (TmProd f) = hasSubst f
hasSubst (TmAbs f) = hasSubst f
hasSubst (TmApp a b) = hasSubst a || hasSubst b
hasSubst (TmEq a x y) = hasSubst a || hasSubst x || hasSubst y
hasSubst (TmRefl a x) = hasSubst a || hasSubst x
hasSubst (TmEqInd ct c x y p) = hasSubst ct || hasSubst c || hasSubst x || hasSubst y || hasSubst p
hasSubst _ = False

reduceValue :: TermP (Binding a) -> TermP a
reduceValue = rd
  where
    rd :: TermP (Binding a) -> TermP a
    rd (TmFamily a f) = TmFamily (rd a) $ \x ->
      rd (f (BindDecl (TmVar x) (rd a)))
    rd (TmSubst (TmFamily a f) b) =
      rd (f (BindDef (rd b) (rd a)))
    rd (TmSubst f b) = TmSubst (rd f) (rd b)
    rd (TmVar b) = valueOfBinding b
    rd (TmU i) = TmU i
    rd (TmProd f) = TmProd (rd f)
    rd (TmAbs f) = TmAbs (rd f)
    rd (TmApp (TmAbs (TmFamily t f)) b) =
      rd (f (BindDef (rd b) (rd t)))
    rd (TmApp a b) = TmApp (rd a) (rd b)
    rd (TmEq a x y) = TmEq (rd a) (rd x) (rd y)
    rd (TmRefl a x) = TmRefl (rd a) (rd x)
    rd (TmEqInd ct (TmFamily t c) x y (TmRefl a z)) =
      rd (c (BindDef (rd x) (rd a)))
    rd (TmEqInd ct c x y p) = TmEqInd (rd ct) (rd c) (rd x) (rd y) (rd p)
    rd _ = undefined

univ :: TermP a -> Int
univ (TmU u) = u
univ (TmFamily _ f) = univ (f (error "not universe"))
univ _ = error "not universe"

reduceType :: TermP (Binding a) -> TermP a
reduceType = rd
  where
    err = error "type check error"
    rd :: TermP (Binding a) -> TermP a
    rd (TmFamily a f) = TmFamily (reduceValue a) $ \x -> -- TODO: a : U
      rd (f (BindDecl (TmVar x) (reduceValue a)))
    rd (TmSubst (TmFamily a f) b) =
      rd (f (BindDef (reduceValue b) (reduceValue a)))
    rd (TmVar b) = typeOfBinding b
    rd (TmU i) = TmU (i + 1)
    rd (TmProd f@(TmFamily a _)) =
      TmU (max ua ufa)
      where ua  = univ (rd a)
            ufa = univ (rd f)
    rd (TmAbs f) = case rd f of
      TmFamily a f -> TmProd (TmFamily a f)
      _ -> err
    rd (TmApp a b) = case rd a of -- TODO: typeof b
      TmProd (TmFamily at rtf) -> TmSubst (TmFamily at rtf) (reduceValue b)
      _ -> err
    rd (TmEq a x y) = -- TODO: x y : A
      TmU ua
      where ua = univ (rd a)
    rd (TmRefl a x) = TmEq (reduceValue a) (reduceValue x) (reduceValue x) -- TODO: a : U, x : a
    rd (TmEqInd ct c x y p) =
      TmSubst (TmSubst (TmSubst (reduceValue ct) (reduceValue x)) (reduceValue y)) (reduceValue p)
    rd _ = undefined

showsTerm :: TermP Char -> ShowS
showsTerm tm = runReader (showR tm) 'a'
  where
    showR :: TermP Char -> Reader Char ShowS
    showR (TmFamily a f) =
      do i <- ask
         s <- local succ $ showR (f i)
         as <- showR a
         return $ ("(\\"++) . (i:) . (" : "++) . as . (" -> "++) . s . (")"++)
    showR (TmSubst f a) = do
      s1 <- showR f
      s2 <- showR a
      return $ ("SUBST ("++) . s1 . (") ["++) . s2 . ("]"++)
    showR (TmVar i) = return $ (i:)
    showR (TmU i) = return $ ("U"++) . shows i
    showR (TmProd f) = do
      s1 <- showR f
      return $ ("(PROD "++) . s1 . (")"++)
    showR (TmAbs f) = do
      s1 <- showR f
      return $ ("(ABS "++) . s1 . (")"++)
    showR (TmApp a b) = do
      s1 <- showR a
      s2 <- showR b
      return $ s1 . (" "++) . s2
    showR (TmSigma f) = do
      s1 <- showR f
      return $ ("(SIGMA "++) . s1 . (")"++)
    showR (TmPair _ a b) = do
      s1 <- showR a
      s2 <- showR b
      return $ ("(PAIR "++) . s1 . (" "++) . s2 . (")"++)
    showR (TmSigmaInd c g p) = do
      s1 <- showR c
      s2 <- showR g
      s3 <- showR p
      return $ ("(IND_SIGMA "++) . s1 . (" "++) . s2 . (" "++) . s3 . (")"++)
    showR (TmEq a x y) = do
      s1 <- showR a
      s2 <- showR x
      s3 <- showR y
      return $ ("("++) . s2 . (" ="++) . s1 . ("= "++) . s3 . (")"++)    
    showR (TmRefl a x) = do
      s1 <- showR a
      s2 <- showR x
      return $ ("(REFL "++) . s1 . (" "++) . s2 . (")"++)
    showR (TmEqInd ct c a b p) = do
      s1 <- showR ct
      s2 <- showR c
      s3 <- showR a
      s4 <- showR b
      s5 <- showR p
      return $ ("(IND_EQ "++) . s1 . (" "++) . s2 . (" "++) . s3 . (" "++) . s4 . (" "++) . s5 . (")"++)

instance (a ~ Char) => Show (TermP a) where
  show t = showsTerm t ""

r :: IO ()
r = do
  go u0
  go u1
  go $ prod u0 $ \_ -> u0
  go $ abs u0 $ \_ -> u0
  go $ abs u0 $ \x -> v x
  go $ TmEq u1 u0 u0
  go $ TmRefl u1 u0

  go
    $ prod u0
    $ \a -> prod (v a)
            $ \x -> prod (v a)
                    $ \y -> arr (eq (v a) (v x) (v y)) (eq (v a) (v y) (v x))
  go
    $ abs u0
    $ \a -> abs (v a)
            $ \x -> abs (v a)
                    $ \y -> abs (eq (v a) (v x) (v y))
                            $ \p -> (v p)

  go
    $ abs u0 $ \a -> abs (v a) $ \x -> abs (v a) $ \y ->
    abs (eq (v a) (v x) (v y))
    $ \p -> TmEqInd (fam (v a) $ \x' -> fam (v a) $ \y' -> fam (eq (v a) (v x') (v y')) $ \_ -> (eq (v a) (v y') (v x')))
            (fam (v a) $ \z -> TmRefl (v a) (v z)) (v x) (v y) (v p)
    
  where
    go :: Term -> IO ()
    go t = do
      putStrLn "-----"
      putStrLn (show t)
      putStr "  : "
      putStr $ show $ typeof t
      putStrLn ""

    typeof :: Term -> Term
    typeof t = red (reduceType t)

    red :: Term -> Term
    red t = if hasSubst t then red (reduceValue t) else t

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

    v = TmVar

    prod a f = TmProd (TmFamily a f)
    arr a b = TmProd (TmFamily a $ \_ -> b)
    abs a f = TmAbs (TmFamily a f)
    eq = TmEq
    fam = TmFamily
    

result.txt

-----
U0
  : U1
-----
U1
  : U2
-----
(PROD (\a : U0 -> U0))
  : U1
-----
(ABS (\a : U0 -> U0))
  : (PROD (\a : U0 -> U1))
-----
(ABS (\a : U0 -> a))
  : (PROD (\a : U0 -> U0))
-----
(U0 =U1= U0)
  : U2
-----
(REFL U1 U0)
  : (U0 =U1= U0)
-----
(PROD (\a : U0 -> (PROD (\b : a -> (PROD (\c : a -> (PROD (\d : (b =a= c) -> (c =a= b)))))))))
  : U1
-----
(ABS (\a : U0 -> (ABS (\b : a -> (ABS (\c : a -> (ABS (\d : (b =a= c) -> d))))))))
  : (PROD (\a : U0 -> (PROD (\b : a -> (PROD (\c : a -> (PROD (\d : (b =a= c) -> (b =a= c)))))))))
-----
(ABS (\a : U0 -> (ABS (\b : a -> (ABS (\c : a -> (ABS (\d : (b =a= c) -> (IND_EQ (\e : a -> (\f : a -> (\g : (e =a= f) -> (f =a= e)))) (\e : a -> (REFL a e)) b c d)))))))))
  : (PROD (\a : U0 -> (PROD (\b : a -> (PROD (\c : a -> (PROD (\d : (b =a= c) -> (c =a= b)))))))))