我选择了 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 一样的依赖类型语言的核心”),同时保持较小的规模?
最佳答案
首先,一致性是数理逻辑中的一个东西,意味着逻辑不包含矛盾。我见过有人谈论类型理论的“一致性”,但不幸的是这不是一个明确定义的术语。
在 lambda 演算的背景下,许多人使用术语“一致性”来表示截然不同的事物。有些人说无类型 lambda 演算是一致的,他们的意思是 lambda 项的不同推导会导致相同的结果(即 Church-Rosser 性质)。在这方面,大多数演算都是一致的。
但是,一致也可以意味着微积分的 Curry-Howard 同构逻辑是一致的。简单类型的 lambda 演算对应于一阶直觉逻辑(不相等),当人们说 STLC 是一致的时,他们实际上意味着一阶直觉逻辑是一致的。在这种一致性意义上,一致性意味着底部(空)类型没有居民(因此也没有派生)。也就是说,每个表达式都必须生成具有有效类型的值。底部对应于虚假,因此这意味着无法导出虚假(因为你可以从虚假中衍生出任何东西)。
现在,从这个意义上说,为了保持一致,你不能有非终止(fix
)、非返回函数或控制运算符(call/cc
等) )。 Haskell 在这个意义上并不一致,因为你可以编写产生任意类型的函数(函数 f x = f x
的类型为 a -> b
;显然,这不是持续的)。同样,您可以从任何内容返回undefined
,使其生成底部类型的内容。因此,为了确保类型理论在这个意义上是一致的,您必须确保不能从任何表达式返回空类型。
但是,从第一个意义上的“一致性”来看,我相信 Haskell 是一致的(除了一些古怪的功能)。方程等价性应该很好。
关于haskell - 究竟是什么使类型系统保持一致?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/40143070/