关闭和普遍量化 [英] Closures and universal quantification

问题描述

我一直在尝试如何在Scala中实现Church编码的数据类型。看起来它需要rank-n类型，因为你需要一个 const 类型的函数forAll。 a - >然而，我能够这样编码对：

$ b $（对于所有b。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） 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））
} 
} 
  

你可以定义nil，这样，给定上面的定义，以下编译？

  cons（1） ））
  

解决方案

感谢Mark Harrah完成这个解决方案。窍门是， Function1 在标准库中没有定义一个一般的足够的方式。

我的Closure问题中的特质实际上是一个自然的变换。这是功能概念的泛化。

  trait〜> [F [_]，G [_] ] {def apply [B]（f：F [B]）：G [B]} 
  

函数 a - > b

 
 
 code> trait Const [A] {type Apply [B] = A} 
 type  - >：[A，B] = Const [A] #Apply〜 
  

Const [A] 将每个类型映射到 A 。

这里是我们的列表类型：

 类型CList [A] =（{type f [x] = Fold [A，x]}）＃f〜 Endo 
  

这里， Endo 用于将类型映射到自身上的函数类型（ endofunction ）。

  type Endo [A] = A  - > ;: A 
  

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

  type Fold [A，B] = A  - >：Endo [B] 
   
 
然后最后，我们的列表构造函数：
  def cons [A] （x：A）= {
 new（CList [A]  - > CList [A]）{
 def apply [C] {
 def apply [B]（f：Fold [A，B]）=（b：B）=> f（x）（xs（f）（b））
} 
} 
} 
 
 def nil [A] = new CList [ $ b def apply [B]（f：Fold [A，B]）=（b：B）=>一个警告是需要显式转换（A  - >：B）b 
} 
  
 
 
到（A => B）来帮助Scala的类型系统。所以实际上折叠一个列表一旦创建仍然是非常冗长和乏味。这里是等效的Haskell比较：
  nil pz = z 
 cons x xs pz = px（xs pz）
  
 Haskell版本中的列表构造和折叠是简洁且无噪音的：
  let xs = cons 1（cons 2（cons 3 nil））in xs（+）0 
  pre> 
I've been trying to work out how to implement Church-encoded data types in Scala. It seems that it requires rank-n types since you would need a first-class const function of type forAll a. a -> (forAll b. b -> b).

However, I was able to encode pairs thusly:
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)
  }
For lists, I was able to encode 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))
  }
}
However, the empty list is more problematic and I've not been able to get the Scala compiler to unify the types.

Can you define nil, so that, given the definition above, the following compiles?
cons(1)(cons(2)(cons(3)(nil)))

解决方案
Thanks to Mark Harrah for completing this solution. The trick is that Function1 in the standard libraries is not defined in a general enough way.

My "Closure" trait in the question is actually a natural transformation between functors. This is a generalization of the concept of "function".
trait ~>[F[_],G[_]] { def apply[B](f: F[B]): G[B] }
A function a -> b then ought to be a specialization of this trait, a natural transformation between two endofunctors on the category of Scala types.
trait Const[A] { type Apply[B] = A }
type ->:[A,B] = Const[A]#Apply ~>: Const[B]#Apply
Const[A] is a functor that maps every type to A.

And here's our list type:
type CList[A] = ({type f[x] = Fold[A,x]})#f ~> Endo
Here, Endo is just an alias for the type of functions that map a type onto itself (an endofunction). 
type Endo[A] = A ->: A
And Fold is the type of functions that can fold a list:
type Fold[A,B] = A ->: Endo[B]
And then finally, here are our list constructors:
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
}
One caveat is the need to explicitly convert (A ->: B) to (A => B) to help Scala's type system along. So it's still terribly verbose and tedious to actually fold a list once created. Here's the equivalent Haskell for comparison:
nil p z = z
cons x xs p z = p x (xs p z)
List construction and folding in the Haskell version is terse and noise-free:
let xs = cons 1 (cons 2 (cons 3 nil)) in xs (+) 0


                        
这篇关于关闭和普遍量化的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！