什么因素会使一个类型系统一致？

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、合并infer/eval等）会遇到哪些问题？这些问题是否可以“证明”（生成不同的系统但仍然“正确”）？

• 基本上：是否有可能在保持小型的同时修复此系统（即使其“适用于像CoC这样的依赖类型语言的核心”）？

可运行代码。

- MaiaVictor

---

这里有一个关于一致性的小诀窍：是否有任何类型是没有人使用的？如果每个类型都有人使用，那么这很可能意味着它不一致。 - Daniel Wagner

请参考Simply Easy或Weirich的这个系列讲座(以及代码)，了解一些小型依赖类型系统的示例。不过我不认为你已经实现了一个类型检查器（例如，我期望typeof (VL x y)返回一个pi类型，而不是另一个lambda）。我推荐Types and Programming Languages作为入门读物，我目前已经看到一半了。 - Benjamin Hodgson

@Viclib 你可以通过提供一个接受类型并生成该类型术语的函数来知道每种类型是否被占用。通常这很容易；例如，通常可以给无限循环任何类型。我不确定是否有一致的定义。当然，如果有人做了以下事情，我会眯起眼睛：1.从Haskell的类型系统开始，很容易证明不一致。2.添加一个新类型“UNINHABITED”，并使其无法通过任何类型判断到达。3.声称这个新系统是一致的。 - Daniel Wagner

请注意，在这个系统中，“VL”实际上同时代表“λ”或“Pi”（因为它们的工作方式相同...）——Thorsten Altenkirch：“函数和它的类型是非常不同的概念，即使它们有一些表面上的语法相似性。特别是对于新手来说，这种等同是非常令人困惑和完全误导的。我认为应该从它们的含义而不是它们的外观来理解类型理论概念”。 - effectfully

而Thorsten的话也立即证明了这一点：你写了∀(a:*) . (λ(x:a) . a)，但是λ(x:a) . a不是一个类型，因此它不能作为∀的参数。 - effectfully

Answer 1

首先，在数理逻辑中，“一致性”是指逻辑不包含矛盾。我见过人们谈论类型理论的“一致性”，但不幸的是，这并不是一个明确定义的术语。

在 lambda 演算的背景下，许多人使用“一致性”这个术语来表示非常不同的事情。有些人说无类型 lambda 演算是一致的，这意味着 lambda 项的不同推导导致相同的结果（即 Church-Rosser 性质）。在这方面，大多数演算都是一致的。

然而，“一致”的含义也可以是与演算的 Curry-Howard 同构逻辑一致。简单类型 lambda 演算对应于一阶直觉主义逻辑（没有相等性），当人们说 STLC 是一致的时，他们真正意思是一阶直觉主义逻辑是一致的。在这种一致性意义上，一致性意味着底部（void）类型没有实例（因此也没有推导）。也就是说，每个表达式必须产生一个具有有效类型的值。Bottom 对应于 falsehood，这意味着不能推导出 falsehood（因为你可以从 falsehood 推导出任何东西）。

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

但是，从“一致性”的第一个意义上讲，我认为Haskell是一致的（除了一些古怪的功能）。等式等价应该很好。

- xuq01