多态编码的递归代数数据类型的值是多少?
Posted
技术标签:
【中文标题】多态编码的递归代数数据类型的值是多少?【英文标题】:What are the values of a polymorphically encoded recursive algebraic data type? 【发布时间】:2014-08-15 17:35:14 【问题描述】:以下问题与Recursive algebraic data types via polymorphism in Haskell有关。
递归代数数据类型可以在任何具有 System F 功能的语言中使用通用参数多态性来实现。例如,自然数的类型可以(在 Haskell 中)引入为
newtype Nat = Nat runNat :: forall t. (t -> (t -> t) -> t)
“通常的”自然数 n
被实现为
\ x0 f -> f(f(...(f x0)...))
使用n
迭代f
。
类似地,布尔值的类型可以被引入
newtype Bool = Bool runBool :: forall t. t -> t -> t
预期值 'true' 和 'false' 被实现为
true = \ t f -> t
false = \ t f -> f
Q: 是否所有类型的项都是Bool
或Nat
或上述形式的任何其他潜在递归代数数据类型(以这种方式编码),直至操作语义的一些简化规则?
示例 1(自然数): forall t. t -> (t -> t) -> t
类型的任何术语在某种意义上是否与 \ x0 f -> f (f ( ... (f x0) ... ))
形式的术语“等效”? p>
示例 2(布尔值):在某种意义上,forall t. t -> t -> t
类型的任何术语是否与 \ t f -> t
或 \ t f -> f
“等效”?
附录(内部版本):如果所考虑的语言甚至能够表达命题相等,这个元数学问题可以内化如下,如果有人愿意,我会很高兴想出一个解决方案:
对于任何函子m
,我们可以在其上定义通用模块和一些解码-编码函数,如下所示:
type ModStr m t = m t -> t
UnivMod m = UnivMod univProp :: forall t. (ModStr m t) -> t
classifyingMap :: forall m. forall t. (ModStr m t) -> (UnivMod m -> t)
classifyingMap f = \ x -> (univProp x) f
univModStr :: (Functor m) => ModStr m (UnivMod m)
univModStr = \ f -> UnivMod $ \ g -> g (fmap (classifyingMap g) f)
dec_enc :: (Functor m) => UnivMod m -> UnivMod m
dec_enc x = (univProp x) univModStr
问:如果语言能够表达这一点:是否存在相等类型dec_enc = id
?
【问题讨论】:
【参考方案1】:在系统 F (AKA λ2) 中,∀α.α→α→α
的所有居民确实 λ 等于 K
或 K*
。
首先,如果M : ∀α.α→α→α
,那么它有范式N
(因为系统F正在归一化)并且通过主题归约定理(参见Barendregt: Lambda calculi with types)还有N : ∀α.α→α→α
。
让我们来看看这些正常形式的外观。 (我们将使用 λ2 的生成引理,有关正式细节,请参阅 Barendregt 的书。)
如果N
是范式,则N
(或其任何子表达式)必须是头范式,即λx1 ... xn. y P1 ... Pk
形式的表达式,其中n
和/或k
也可以是 0。
对于N
的情况,必须至少有一个 λ,因为最初我们在键入上下文中没有任何变量绑定来代替y
。所以N = λx.U
和x:α |- U:α→α
。
现在在U
的情况下必须至少有一个λ,因为如果U
只是y P1 ... Pk
那么y
将有一个函数类型(即使对于k=0,我们也需要@ 987654343@),但上下文中只有x:α
。所以N = λxy.V
和x:α, y:α |- V:α
。
但是V
不能是λ..
,因为那样它就会有函数类型τ→σ
。所以V
必须是z P1 ... Pk
的形式,但是由于我们在上下文中没有任何函数类型的变量,k
必须为0,因此V
只能是x
或@987654355 @。
因此,∀α.α→α→α
类型的正常形式中只有两个术语:λxy.x
和 λxy.y
,并且此类型的所有其他术语都 β 等于其中之一。
使用类似的推理,我们可以证明∀α.α→(α→α)→α
的所有居民都β-等于教堂数字。 (而且我认为对于∀α.(α→α)→α→α
类型,情况稍差;我们还需要η-相等,因为λf.f
和λfx.fx
对应于1
,但不是β-相等,只是βη-相等。 )
【讨论】:
亲爱的彼得 - 谢谢你的回答,很抱歉我花了很长时间才回复!您是否从您的术语中省略了多态抽象和应用程序?在我看来,人们必须考虑范式形式,其主要抽象可能在术语和类型抽象之间交替,以及这些抽象中的(y P1 ... Pk) [T]
等应用术语。但是,这似乎不会在您的论点中引起任何严重的并发症。
@Hanno 我的答案是针对没有任何类型注释或 Λ 的 System-F 的 Curry 风格版本。但我相信同样的论点也可以用于教会风格。我还推荐this answer,它给出了完全不同的证明——它没有表明只有两个正常形式的术语,但它表明布尔类型的所有术语都是extensionally equal到K
和@987654366 @.
好的,谢谢!然而,我偶然发现 CoQ'Art 书中的一句话(前言中的 p.XII)让我感到困惑:关于递归类型的多态编码,它说“......,她 [Christine Mohring] 意识到'她使用的“禁止性”编码不尊重归纳类型的术语仅限于类型构造函数的组合的传统。多态 lambda 演算中的编码引入了寄生术语,使得无法表达适当的归纳原则。你知道这与你的答案有什么关系吗?
即(为什么)如果我们使用更具表现力的构造微积分,事情会崩溃吗?
@Hanno 这超出了我的知识范围。如果您发现了,请添加评论。【参考方案2】:
如果我们忽略底部和unsafe
的东西,那么你唯一可以用函数a -> a
做的事情就是组合它们。然而,这并不能完全阻止我们使用有限的 f (f ( ... (f x0) ... ))
表达式:我们还有无限的组合 infty x f = f $ infty x f
。
同样,唯一的非递归布尔值确实是\t _ -> t
和\_ f -> f
,但你也可以在这里打结,比如
blarg t f = blarg (blarg t f) (blarg f t)
【讨论】:
感谢您的回答!我应该更准确一点,因为我希望这些术语存在于 System F 中,这样就消除了递归的可能性。以上是关于多态编码的递归代数数据类型的值是多少?的主要内容,如果未能解决你的问题,请参考以下文章