What exactly makes a type system consistent?

Question

I've taken András Kovács's DBIndex.hs, a very simple implementation of a dependently typed core, and tried simplifying it even further, as much as I possibly could, without "breaking" the type system. After several simplifications, I was left with something much smaller:

{-# 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

The problem is that I have no idea what makes a type system consistent, so I had no criteria (other than intuition) and probably broke it in several ways. It, more or less, does what I think a type system should do, though:

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

My question is, what exactly makes a system consistent? Specifically:

• What problems do I get from the things I did (removing Pi, merging infer/eval, etc.)? Can those be somehow "justified" (generating a different system but still "correct")?

• Basically: is it possible to fix this system (i.e., make it "suitable as the core of a dependently typed language just like CoC") while keeping it small?

Runnable code.

Answer 1

First of all, consistency is a thing in mathematical logic, meaning that a logic doesn't contain a contradiction. I've seen people speaking about the "consistency" of type theories, but unfortunately it is not a well-defined term.

In the context of lambda calculus, many people use the term "consistency" to mean vastly different things. Some people say the untyped lambda-calculus is consistent, by which they mean that different derivations of a lambda-term lead to the same result (i.e. the Church-Rosser property). In that respect, most calculi are consistent.

However, consistent can also mean that the Curry-Howard isomorphic logic of the calculus is consistent. Simply-typed lambda-calculus corresponds to first-order intuitionistic logic (without equality), and when people say STLC is consistent they really mean that first-order intuitionistic logic is consistent. In this sense of consistency, consistency means that the bottom (void) type doesn't have an inhabitant (and, thus, a derivation). That is, every expression must produce a value with a valid type. Bottom corresponds to falsehood, so this means that falsehood can't be derived (because you can derive anything from falsehood).

Now, in this sense, to be consistent you can't have nontermination (fix), non-returning functions, or control operators (call/cc and friends). Haskell is not consistent in this sense, because you can write functions that produce arbitrary types (the function f x = f x has type a -> b; obviously, this isn't consistent). Similarly, you can return undefined from anything, making it producing something of the bottom type. So, to make sure that a type theory is consistent in this sense, you'd have to make sure that you can't return the empty type from any expression.

But then, in the first sense of "consistency", Haskell is consistent I believe (barring some wacky features). Equational equivalence should be good.