Cierres y cuantificación universal

Question

He estado tratando de resolver cómo implementar los tipos de datos codificados por la iglesia en Scala. Parece que requiere tipos de rango, ya que necesitarías una primera clase const función del tipo forAll a. a -> (forAll b. b -> b).

Sin embargo, pude 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, pude 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 no he podido hacer que el compilador Scala unifique los tipos.

¿Puedes definir nulo, de modo que, dada la definición anterior, las siguientes compilaciones?

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

Answer 1

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

Mi rasgo de "cierre" en la pregunta es en realidad una transformación natural entre los functores. 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 debería ser una especialización de este rasgo, una transformación natural entre dos endofuntores 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 functor que asigna a cada tipo a A.

Y aquí está nuestro tipo de lista:

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

Aquí, Endo es solo un alias para el tipo de funciones que asignan un tipo en sí mismo (un endofunción).

type Endo[A] = A ->: A

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

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

Y finalmente, aquí están nuestros constructores de lista:

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) a (a => b) para ayudar al sistema de tipo de Scala. Por lo tanto, todavía es terriblemente detallado y tedioso doblar una lista una vez creada. Aquí está el equivalente Haskell para la comparación:

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

La construcción de la lista y el plegamiento en la versión Haskell es Terse y sin ruido:

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