闭包和通用量化

Posted 2023-02-22

【中文标题】闭包和通用量化

【英文标题】：Closures and universal quantification

【发布时间】：2011-02-05 20:00:15

【问题描述】：

我一直在尝试研究如何在 Scala 中实现 Church 编码的数据类型。似乎它需要 rank-n 类型，因为您需要 forAll a. a -> (forAll b. b -> b) 类型的一流 const 函数。

但是，我可以这样对对进行编码：

import scalaz._

trait Compose[F[_],G[_]]  type Apply = F[G[A]] 

trait Closure[F[_],G[_]]  def apply[B](f: F[B]): G[B] 

def pair[A,B](a: A, b: B) =
  new Closure[Compose[(type f[x] = A => x)#f,
                      (type f[x] = B => x)#f]#Apply, Id] 
    def apply[C](f: A => B => C) = f(a)(b)
  

对于列表，我能够编码cons：

def cons[A](x: A) = 
  type T[B] = B => (A => B => B) => B
  new Closure[T,T] 
    def apply[B](xs: T[B]) = (b: B) => (f: A => B => B) => f(x)(xs(b)(f))
  

但是，空列表的问题更大，我无法让 Scala 编译器统一类型。

你能定义 nil，这样，给定上面的定义，下面的编译吗？

cons(1)(cons(2)(cons(3)(nil)))

【问题讨论】：

这是 Scala 中关于教堂数字的一个例子：jim-mcbeath.blogspot.com/2008/11/…

Randall：这些是类型级别的教堂数字。我所做的不是类型级别的。

不管怎样，Scala 方法有效地为您提供了 n 个类型的排名。

Scala 方法不能有效地为您提供 rank-n 类型，但您可以通过这种方式编码大量 rank-n 类型。

【参考方案1】：

感谢 Mark Harrah 完成此解决方案。诀窍是标准库中的Function1 没有以足够通用的方式定义。

我在问题中的“闭包”特征实际上是函子之间的自然转换。这是对“功能”概念的概括。

trait ~>[F[_],G[_]]  def apply[B](f: F[B]): G[B] 

函数a -> b 应该是这个特征的特化，是Scala 类型类别上的两个内函子之间的自然转换。

trait Const[A]  type Apply[B] = A 
type ->:[A,B] = Const[A]#Apply ~>: Const[B]#Apply

Const[A] 是一个函子，将每种类型映射到A。

这是我们的列表类型：

type CList[A] = (type f[x] = Fold[A,x])#f ~> Endo

这里，Endo 只是将类型映射到自身的函数类型的别名（endofunction）。

type Endo[A] = A ->: A

而Fold是可以折叠列表的函数类型：

type Fold[A,B] = A ->: Endo[B]

最后，这是我们的列表构造函数：

def cons[A](x: A) = 
  new (CList[A] ->: CList[A]) 
    def apply[C](xs: CList[A]) = new CList[A] 
      def apply[B](f: Fold[A,B]) = (b: B) => f(x)(xs(f)(b))
    
  


def nil[A] = new CList[A] 
  def apply[B](f: Fold[A,B]) = (b: B) => b

一个警告是需要将 (A ->: B) 显式转换为 (A => B) 以帮助 Scala 的类型系统。因此，一旦创建了列表，实际上折叠列表仍然非常冗长和乏味。这是用于比较的等效 Haskell：

nil p z = z
cons x xs p z = p x (xs p z)

Haskell 版本中的列表构造和折叠简洁且无噪音：

let xs = cons 1 (cons 2 (cons 3 nil)) in xs (+) 0

【讨论】：

这太超出我的舒适区了！