Agn*_*yay 10 type-theory lambda-calculus existential-type system-f
在系统F中,类型exists a. P可以被编码为forall b. (forall a. P -> b) -> b使用存在性的任何系统F术语可以根据关于打字和缩减规则的该编码来表达.
在"类型和编程语言"中,将显示以下练习:
我们可以根据存在类型编码通用类型吗？
我的直觉说这是不可能的,因为在某种程度上,"存在包装"机制并不像"类型抽象"机制那样强大.我如何正式展示这个？
我甚至不确定我需要证明什么才能正式显示这个结果.