究竟是什么让类型系统保持一致？

Question

我采用了 András Kovács 的 DBIndex.hs，一个非常简单的依赖类型内核的实现，并尝试在不“破坏”类型系统的情况下尽可能地进一步简化它。经过几次简化后，我得到了一些小得多的东西：

{-# language LambdaCase, ViewPatterns #-}

data Term
  = V !Int
  | A Term Term
  | L Term Term
  | S
  | E
  deriving (Eq, Show)

data VTerm
  = VV !Int
  | VA VTerm VTerm
  | VL VTerm (VTerm -> VTerm)
  | VS
  | VE

type Ctx = ([VTerm], [VTerm], Int)

eval :: Bool -> Term -> Term
eval typ term = err (quote 0 (eval term typ ([], [], 0))) where

  eval :: Term -> Bool -> Ctx -> VTerm
  eval E _ _ = VE
  eval S _ _ = VS
  eval (V i) typ ctx@(vs, ts, _) = (if typ then ts else vs) !! i
  eval (L a b) typ ctx@(vs,ts,d) = VL a' b' where
    a' = eval a False ctx
    b' = \v -> eval b typ (v:vs, a':ts, d+1)
  eval (A f x) typ ctx = fx where
    f' = eval f typ ctx
    x' = eval x False ctx
    xt = eval x True ctx
    fx = case f' of
      (VL a b) -> if check a xt then b x' else VE -- type mismatch
      VS       -> VE -- non function application
      f        -> VA f x'

  check :: VTerm -> VTerm -> Bool
  check VS _ = True
  check a  b = quote 0 a == quote 0 b

  err :: Term -> Term
  err term = if ok term then term else E where
    ok (A a b) = ok a && ok b
    ok (L a b) = ok a && ok b
    ok E = False
    ok t = True

  quote :: Int -> VTerm -> Term
  quote d = \case
    VV i    -> V (d - i - 1)
    VA f x  -> A (quote d f) (quote d x)
    VL a b  -> L (quote d a) (quote (d + 1) (b (VV d)))
    VS      -> S
    VE      -> E

reduce :: Term -> Term
reduce = eval False

typeof :: Term -> Term
typeof = eval True

问题是我不知道是什么使类型系统保持一致，所以我没有标准（除了直觉）并且可能以多种方式破坏它。不过，它或多或少做了我认为类型系统应该做的事情：

main :: IO ()
main = do
  --  id = ∀ (a:*) . (λ (x:a) . a)
  let id = L S (L (V 0) (V 0))

  --  nat = ∀ (a:*) . (a -> a) -> (a -> a)
  let nat = L S (L (L (V 0) (V 1)) (L (V 1) (V 2)))

  --  succ = λ (n:nat) . ∀ (a:*) . λ (s : a -> a) . λ (z:a) . s (n a s z)
  let succ = L nat (L S (L (L (V 0) (V 1)) (L (V 1) (A (V 1) (A (A (A (V 3) (V 2)) (V 1)) (V 0))))))

  --  zero = λ (a:*) . λ (s : a -> a) . λ (z : a) . z
  let zero = L S (L (L (V 0) (V 1)) (L (V 1) (V 0)))

  --  add = λ (x:nat) . λ (y:nat) . λ (a:*) . λ(s: a -> a) . λ (z : a) . (x a s (y a s z))
  let add = L nat (L nat (L S (L (L (V 0) (V 1)) (L (V 1) (A (A (A (V 4) (V 2)) (V 1)) (A (A (A (V 3) (V 2)) (V 1)) (V 0)))))))

  --  bool = ∀ (a:*) . a -> a -> a
  let bool = L S (L (V 0) (L (V 1) (V 2)))

  --  false = ∀ (a:*) . λ (x : a) . λ(y : a) . x
  let false = L S (L (V 0) (L (V 1) (V 0)))

  --  true = ∀ (a:*) . λ (x : a) . λ(y : a) . y
  let true = L S (L (V 0) (L (V 1) (V 1)))

  --  loop = ((λ (x:*) . (x x)) (λ (x:*) . (x x)))
  let loop = A (L S (A (V 0) (V 0))) (L S (A (V 0) (V 0)))

  --  natOrBoolId = λ (a:bool) . λ (t:(if a S then nat else bool)) . λ (x:t) . t
  let natOrBoolId = L bool (L (A (A (A (V 0) S) nat) bool) (V 0))

  -- nat
  let c0 = zero
  let c1 = A succ zero
  let c2 = A succ c1
  let c3 = A succ c2
  let c4 = A succ c3
  let c5 = A succ c4

  -- Tests
  let test name pass = putStrLn $ "- " ++ (if pass then "OK." else "ERR") ++ " " ++ name

  putStrLn "True and false are bools"
  test "typeof true  == bool " $ typeof true  == bool
  test "typeof false == bool " $ typeof false == bool

  putStrLn "Calling 'true nat' on two nats selects the first one"
  test "reduce (true nat c1 c2) == c1"  $ reduce (A (A (A true nat) c1) c2) == reduce c1
  test "typeof (true nat c1 c2) == nat" $ typeof (A (A (A true nat) c1) c2) == nat

  putStrLn "Calling 'true nat' on a bool is a type error"
  test "reduce (true nat true c2) == E" $ reduce (A (A (A true nat) true) c2) == E
  test "reduce (true nat c2 true) == E" $ reduce (A (A (A true nat) c2) true) == E

  putStrLn "More type errors"
  test "reduce (succ true) == E" $ reduce (A succ true) == E

  putStrLn "Addition works"
  test "reduce (add c2 c3) == c5"  $ reduce (A (A add c2) c3) == reduce c5
  test "typeof (add c2 c2) == nat" $ typeof (A (A add c2) c3) == nat

  putStrLn "Loop isn't typeable"
  test "typeof loop == E" $ typeof loop == E

  putStrLn "Function with type that depends on value"
  test "typeof (natOrBoolId true c2) == nat" $ typeof (A (A natOrBoolId true) c2) == nat
  test "typeof (natOrBoolId true true) == E" $ typeof (A (A natOrBoolId true) true) == E
  test "typeof (natOrBoolId false c2) == E" $ typeof (A (A natOrBoolId false) c2) == E
  test "typeof (natOrBoolId false true) == bool"  $ typeof (A (A natOrBoolId false) true) == bool

我的问题是，究竟是什么让系统保持一致？具体来说：

• 我从我所做的事情中遇到了什么问题（删除 Pi、合并推断/评估等）？这些可以以某种方式“合理”（生成不同的系统但仍然“正确”）吗？

• 基本上：是否有可能修复这个系统（即，使其“适合作为像 CoC 一样的依赖类型语言的核心”）同时保持它的小？

Runnable code.

Answer 1

首先，一致性是数理逻辑中的一个东西，意思是一个逻辑不包含矛盾。我见过有人谈论类型理论的“一致性”，但不幸的是，它不是一个定义明确的术语。

在 lambda 演算的上下文中，许多人使用术语“一致性”来表示截然不同的事物。有人说无类型的 lambda 演算是一致的，他们的意思是 lambda 项的不同推导导致相同的结果（即 Church-Rosser 属性）。在这方面，大多数演算都是一致的。

然而，一致也可以表示微积分的Curry-Howard同构逻辑是一致的。简单类型的 lambda-calculus 对应于一阶直觉逻辑（没有相等性），当人们说 STLC 是一致的时，他们实际上是指一阶直觉逻辑是一致的。在这种一致性的意义上，一致性意味着底部（空）类型没有居民（因此，没有派生）。也就是说，每个表达式都必须生成一个具有有效类型的值。底部对应于虚假，因此这意味着无法衍生虚假（因为您可以从虚假中衍生出任何东西）。

现在，从这个意义上说，为了保持一致，您不能有非终止 (fix)、非返回函数或控制运算符（call/cc 和朋友们）。 Haskell 在这个意义上是不一致的，因为您可以编写产生任意类型的函数（函数f x = f x 具有类型a -> b；显然，这不一致）。同样，您可以从任何东西返回undefined，使其产生底部类型的东西。因此，为了确保类型理论在这个意义上是一致的，您必须确保您不能从任何表达式返回空类型。

但是，在“一致性”的第一个意义上，我相信 Haskell 是一致的（除了一些古怪的功能）。方程等价应该是好的。