Ho cercato di capire come implementare i tipi di dati codificati da Church in Scala. Sembra che richieda tipi di rank-n poiché è necessaria una funzione di prima classe const
di tipo forAll a. a -> (forAll b. b -> b)
.Chiusure e quantificazione universale
Tuttavia, sono stato in grado di codificare le coppie nel seguente modo:
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)
}
Per le liste, sono stato in grado di codificare 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))
}
}
Tuttavia, la lista vuota è più problematico e ho non è stato in grado di ottenere il compilatore Scala per unificare i tipi.
Puoi definire nil, in modo che, data la definizione di cui sopra, le seguenti compilazioni?
cons(1)(cons(2)(cons(3)(nil)))
Ecco un introito su numeri Chiesa in Scala: http: // jim- mcbeath.blogspot.com/2008/11/practical-church-numerals-in-scala.html –
Randall: Quelli sono numeri di chiesa di livello tipo. Quello che sto facendo non è al livello dei tipi. – Apocalisp
Per quello che vale, i metodi Scala ti danno effettivamente tipi di rango n. – Owen