12

He estado tratando de encontrar la manera de implementar los tipos de datos codificados por Church en Scala. Parece que requiere tipos rango-n ya que necesitaría una función de primera clase const del tipo forAll a. a -> (forAll b. b -> b).Cierres y cuantificación universal

Sin embargo, yo era capaz de codificar pares de esta manera:

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) 
    } 

Para listas, yo era capaz de codificar 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)) 
    } 
} 

Sin embargo, la lista vacía es más problemática y he No se ha podido obtener el compilador de Scala para unificar los tipos.

¿Se puede definir nil, para que, dada la definición anterior, las siguientes compilaciones?

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

Aquí hay una sola toma en números Iglesia en Scala: http: // jim- mcbeath.blogspot.com/2008/11/practical-church-numerals-in-scala.html –

+0

Randall: Esos son números de iglesia de nivel de tipo. Lo que estoy haciendo no está en el nivel de tipos. – Apocalisp

+0

Por lo que vale, los métodos de Scala le otorgan efectivamente rango n tipos. – Owen

Respuesta

11

Gracias a Mark Harrah por completar esta solución. El truco es que Function1 en las bibliotecas estándar no está definido de una manera lo suficientemente general.

Mi rasgo "Closure" en la pregunta es en realidad una transformación natural entre los funtores. Esta es una generalización del concepto de "función".

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

Una función a -> b entonces debe ser una especialización de este rasgo, una transformación natural entre dos endofunctors en la categoría de tipos de Scala.

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

Const[A] es un funtor que asigna a cada tipo A.

Y aquí es nuestro tipo de lista:

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

Aquí, Endo es sólo un alias para el tipo de funciones que se asignan un tipo en sí mismo (un endofunction).

type Endo[A] = A ->: A 

Y Fold es el tipo de funciones que se pueden plegar una lista:

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

Y, por último, he aquí nuestra lista de constructores:

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 
} 

Una advertencia es la necesidad de convertir explícitamente (A ->: B) en (A => B) para ayudar al sistema de tipos de Scala. Por lo tanto, es terriblemente prolijo y tedioso plegar una lista una vez creada. Aquí está la Haskell equivalente para la comparación:

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

construcción de lista y plegado en la versión Haskell es terso y libre de ruidos:

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

¡Esto está fuera de mi zona de confort! – drozzy