关闭和普遍量化

Apo*_*isp 12 closures functional-programming scala quantifiers church-encoding

我一直在努力研究如何在Scala中实现Church编码的数据类型.它似乎需要rank-n类型,因为你需要一个类型的第一类const函数forAll a. a -> (forAll b. b -> b).

但是,我能够如此编码对:

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)
  }
Run Code Online (Sandbox Code Playgroud)

对于列表,我能够编码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))
  }
}
Run Code Online (Sandbox Code Playgroud)

但是,空列表更有问题,我无法让Scala编译器统一类型.

你可以定义nil,所以,鉴于上面的定义,以下编译?

cons(1)(cons(2)(cons(3)(nil)))
Run Code Online (Sandbox Code Playgroud)

Apo*_*isp 11

感谢Mark Harrah完成此解决方案.诀窍在于Function1标准库中没有以足够的方式定义.

问题中我的"封闭"特征实际上是仿函数之间的自然转换.这是"功能"概念的概括.

trait ~>[F[_],G[_]] { def apply[B](f: F[B]): G[B] }
Run Code Online (Sandbox Code Playgroud)

a -> b然后一个函数应该是这个特性的特化,这是Scala类型的两个endofunctors之间的自然转换.

trait Const[A] { type Apply[B] = A }
type ->:[A,B] = Const[A]#Apply ~>: Const[B]#Apply
Run Code Online (Sandbox Code Playgroud)

Const[A]是一个将每种类型映射到的仿函数A.

这是我们的列表类型:

type CList[A] = ({type f[x] = Fold[A,x]})#f ~> Endo
Run Code Online (Sandbox Code Playgroud)

这里,Endo它只是将类型映射到自身的函数类型的别名(endofunction).

type Endo[A] = A ->: A
Run Code Online (Sandbox Code Playgroud)

并且Fold是可以折叠列表的函数类型:

type Fold[A,B] = A ->: Endo[B]
Run Code Online (Sandbox Code Playgroud)

最后,这是我们的列表构造函数:

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
}
Run Code Online (Sandbox Code Playgroud)

需要注意的是需要将(A - >:B)显式转换为(A => B)以帮助Scala的类型系统.因此,创建后实际折叠列表仍然非常冗长和乏味.这是用于比较的等效Haskell:

nil p z = z
cons x xs p z = p x (xs p z)
Run Code Online (Sandbox Code Playgroud)

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

let xs = cons 1 (cons 2 (cons 3 nil)) in xs (+) 0
Run Code Online (Sandbox Code Playgroud)