Chiusure e quantificazione universale
-
25-09-2019 - |
Domanda
ho cercato di capire come implementare i tipi di dati Chiesa-codificati in Scala. Sembra che richiede tipi di rango n poiché si avrebbe bisogno di una funzione di prima classe const
di tipo forAll a. a -> (forAll b. b -> b)
.
Tuttavia, ero 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 io non sono stato in grado di ottenere il compilatore Scala di unificare i tipi.
Si può definire pari a zero, in modo che, data la definizione di cui sopra, i seguenti compilazioni?
cons(1)(cons(2)(cons(3)(nil)))
Soluzione
Grazie a Mark Harrah per il completamento di questa soluzione. Il trucco è che Function1
nelle librerie standard non è definito in modo abbastanza generale.
Il mio tratto "chiusura" in questione è in realtà una trasformazione naturale tra 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
.
E qui è 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 in modo esplicito (A ->: B) (A => B) al sistema di tipi di aiuto di Scala lungo. Quindi è ancora terribilmente prolisso e noioso per piegare in realtà una lista una volta creato. Ecco l'equivalente Haskell per il confronto:
nil p z = z
cons x xs p z = p x (xs p z)
Lista costruzione e pieghevole nella versione Haskell è terso e privo di rumore:
let xs = cons 1 (cons 2 (cons 3 nil)) in xs (+) 0