使用 CPS 将谓词类型减少到 RankNTypes

Question

这四个陈述中哪一个是假的？

• newtype和data定义可以用(->)和forall的type结构来代替。
• RankNTypes已正确实现。
• 即使不存在GADTs，也很难正确实施ImpredicativeTypes。
• 前两个陈述反驳了第三个陈述。

---

编辑：我很惊讶不清楚。data Maybe = Nothing | Just a可以写成type Maybe a = forall b. b -> (a -> b) -> b.data [] a = [] | a : [a]可以写成type [] a = forall b. b -> (a -> b -> b) -> b.(与maybe和foldr相比。对于所有newtype和data定义，应该可以做同样的事情，并且称为延续传递样式(CPS)。

据我所知，对于具有深度嵌套的forall和(->)的类型推断是通过使用RankNTypes扩展ghc正确实现的，但是ImpredicativeTypes，即使在参数中也允许foralls键入(->)以外的构造函数，被无可救药地破坏了。

但是，您不能通过将所有data和newtype类型转换为其 CPS 形式，使用RankNTypes机制进行推理，然后重新转换为data/newtype形式来实现ImpredicativeTypes吗？

Answer 1

都不是。使用ImpredicativeTypes的困难在于没有类型推断，需要用户提供显式的类型签名。您假设由于RankNTypes被广泛使用，因此类型推断通常适用于RankNTypes，但事实并非如此：

一般来说，不可能

推断出更高等级的类型;在许多情况下，类型注释必须由程序员提供。