Haskell的类型系统是否与不一致的逻辑系统同构？如果是这样,后果是什么？

Question

在Haskell中有一个术语undefined :: a,据说是一个坏计算或无限循环的术语表示.由于undefined具有类型a,因此可以通过应用类型替换来创建任何语法正确类型.所以undefined有任何类型,o反过来也是如此:任何类型都有undefined,这是生活在任何类型内部的底值(包括Void类型,对吧？).

库里 - 霍华德同构提供的不仅仅是命题作为类型,它还给出了习惯类型作为定理.

具有所有命题作为定理的逻辑系统被认为是不一致的.

那么,Haskell的类型系统是否与不一致的逻辑系统同构？

如果是这样,后果是什么？

如果Haskell的类型系统是一个不一致的证明系统,我们不能相信它吗？

有可能代表无限循环undefined吗？

Answer 1

是的,逻辑是不一致的.

但是,这并不意味着类型系统是无用的.例如,类型系统确保我们永远不会尝试添加整数和字符串,或者从布尔值中调出第一个组件.这些通常是某些非类型语言中的运行时类型错误.

我们仍然有一些运行时错误,如非详尽的模式匹配(其中我个人从语言:-P禁止), ,error,undefined异常,等等.但至少我们没有类型相关的.我们还有非终止(通过无限递归),这是图灵完整语言中的必要之恶,并且无论如何都会导致不一致.

最后,我认为Curry-Howard即使在这种不一致的环境中也很有用.例如,如果我想写f :: Either a b -> a,我可以立即发现这不是一个直觉主义定理,因此f只能使用上面的运行时错误来实现,所以开始时可能是一个坏主意,如果我需要这样f,我应该重新考虑我的设计.

拥有一个定义良好的Haskell"完整"片段,具有相同的类型,但没有上面提到的不好的东西也是有用的吗？绝对!例如,它允许将任何类型的表达式优化()为值()- 毕竟它必须对其进行求值.此外,e :: a :~: b同样可以优化到类似的东西unsafeCoerce Refl,使得编写"类型之间相等的证明"成为可能,这只需要O(1)运行时成本.现在,不幸的是,这些证据必须在运行时进行评估,导致愚蠢的开销只是为了确保证明是"真实的",而不是例如伪装undefined.

Answer 2

如果Haskell的类型系统是一个不一致的证明系统,那么我们不能相信它？

正如@chi所提到的,类型安全是一种比逻辑一致性要弱得多的条件.引用类型和编程语言(如果您对此类内容感兴趣,请阅读以下内容!),

安全=进步+保存

[...]然后,我们想知道的是,良好类型的术语不会被卡住.我们分两步来说明这一点,俗称进步和保存定理.

• 进度:一个好的术语不会被卡住(无论是一个值还是根据评估规则可以采取一个步骤).
• 保存:如果一个好的术语需要一个评估步骤,那么得到的术语也是很好的类型.

这些属性一起告诉我们,在评估期间,良好类型的术语永远不会达到卡住状态.

请注意,这种类型安全的定义并不排除良好类型的术语永远循环或抛出异常的可能性.但是这两条规则确实可以保证,如果你已经成功获得了Int它,那么它确实是一个Int而不是一个Bool或一个Spoon或一个Ennui.(在Haskell中,这有点复杂,因为懒惰,但基本的想法仍然是正确的.)这是一个非常有用的属性,程序员学会在他们的日常工作流程中至关重要地依赖它!

让我一个题外话.就像逻辑上不一致但仍然是类型安全的系统在实践中是有用且值得信赖的那样,类型不安全但仍然静态检查的系统在实践中也是有用的(尽管有些人可能不愿称它们"值得信赖") .查看JavaScript生态系统,其中"逐渐类型化"的系统(如TypeScript和Flow)旨在为工作程序员提供额外的支持 - 因为VanillaJS甚至是中型代码库中的噩梦 - 没有像进步和保存这样做出大胆的承诺.(我听说Python和PHP社区也逐渐(哈哈)采用类型.)TypeScript仍然成功地捕获了我在编程时产生的大部分人为错误,并且支持在小型和大型中更改代码,尽管不是"在正式意义上"安全".

我想我的观点是,PL社区倾向于非常重视证明系统的属性(例如类型安全),但这通常不是软件工程师完成工作的方式!我所知道的工程师关心的是一个工具是否可以帮助他们减少错误,而不是关于它是否被证明是安全的或一致的.我只是觉得每个小组都可以从另一个小组中学到很多东西!当超类型社区中聪明的人与无类型社区中的聪明人聚在一起构建工程工具时,有趣的事情就会发生.

有可能代表无限循环undefined吗？

当然.很多方法.

loop = loop
fib = 1 : 1 : zipWith (+) fib (tail fib)
repeat x = unfoldr (const (Just x))
main = forever $ print "cheese"

从正式的角度来看,所有这些术语都是?,但在实践中,它非常重要,?你正在运行.

如果您的问题确实存在,那么编写循环术语的能力意味着不一致吗？那么简短的回答是肯定的,即let x = x in x :: forall a. a.这就是为什么像Agda这样的证明助手通常会使用终止检查器来检查程序的语法并拒绝一般递归的可疑外观.更长的答案是否定的,不完全是 - 你可以将程序的通用递归部分嵌入monad中,然后用一些外部求值程序实现该偏好monad的语义.(这正是Haskell纯粹采用的方法:将不纯的部分放在IOmonad中,并将执行委托给运行时系统.)

总而言之,是的,Haskell作为一种逻辑是不一致的 - 每种类型都由具有?各种运行时行为的无限s 族居住,因此您可以轻松地"证明"任何命题.那(以及依赖类型的总体笨拙)是人们不使用Haskell作为定理证明者的原因.但是对于工程而言,类型安全的较少保证通常是足够的,其中一些?是有趣的!