12

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))) 
+1

Ecco un introito su numeri Chiesa in Scala: http: // jim- mcbeath.blogspot.com/2008/11/practical-church-numerals-in-scala.html –

+0

Randall: Quelli sono numeri di chiesa di livello tipo. Quello che sto facendo non è al livello dei tipi. – Apocalisp

+0

Per quello che vale, i metodi Scala ti danno effettivamente tipi di rango n. – Owen

risposta

11

Grazie a Mark Harrah per aver completato questa soluzione. Il trucco è che Function1 nelle librerie standard non è definito in modo abbastanza generale.

Il mio tratto di "chiusura" nella domanda è in realtà una trasformazione naturale tra i funtori. Questa è una generalizzazione del concetto di "funzione".

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

Una funzione a -> b quindi dovrebbe essere una specializzazione di questa caratteristica, una trasformazione naturale tra due endofunctors sulla categoria di tipi di Scala.

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

Const[A] è un funtore che associa ogni tipo di A.

Ed ecco il nostro tipo di elenco:

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

Qui, Endo è solo un alias per il tipo di funzioni che mappano un tipo su se stesso (un endofunction).

type Endo[A] = A ->: A 

E Fold è il tipo di funzioni che possono piegare un elenco:

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

E poi finalmente, ecco i nostri lista costruttori:

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 
} 

Un avvertimento è la necessità di convertire esplicitamente (A ->: B) in (A => B) per aiutare il sistema di tipo Scala. Quindi è ancora terribilmente prolisso e noioso piegare effettivamente una lista una volta creata. Ecco l'equivalente Haskell per il confronto:

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

costruzione List e pieghevole nella versione Haskell è terso e senza disturbi:

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

Questo è così fuori dalla mia zona di comfort! – drozzy