Come implementare il calcolo del combinatore SKI con i tipi di corrispondenza?
Stavo cercando di implementare il calcolo del combinatore SKI in Dotty utilizzando i tipi di corrispondenza.
Una breve descrizione del calcolo del combinatore SKI:
S
,K
, eI
sono termini(xy)
è un termine sex
ey
sono termini ed è come l'applicazione di una funzione(((Sx)y)z)
(uguale aSxyz
) restituiscexz(yz)
(uguale a(xz)(yz)
)((Kx)y)
(uguale aKxy
) restituiscex
(Ix)
ritornax
Di seguito è quello che ho usato ( R
riduce il termine il più possibile). Un termine (xy)
è scritto come una tupla (x,y)
e S
, K
e I
sono tratti.
trait S
trait K
trait I
type R[T] = T match {
case (((S,x),y),z) => R[((x,z),(y,z))]
case ((K,x),y) => R[x]
case (I,x) => R[x]
case (a,b) => R[a] match {
case `a` => (a, R[b])
case _ => R[(R[a], R[b])]
}
case T => T
}
Tuttavia, le seguenti 2 righe non vengono compilate (entrambe per lo stesso motivo) ( Scastie ):
val check: (K, K) = ??? : R[(((S,I),I),K)]
val check2: (K, K) = ??? : R[((I,K),(I,K))]
L'errore dice che è richiesto (K,K)
ma trovato R[((I, K), (I, K))]
. Mi aspettavo che prima vedesse la S e la trasformasse in (IK)(IK)
, o R[((I,K),(I,K))]
, dopo di che dovrebbe corrispondere alla valutazione della prima (I, K)
e vedere che è K
, che non è la stessa cosa di (I, K)
, facendola ritornare R[(R[(I,K)], R[(I,K)])]
, che diventa R[(K,K)]
, che diventa giusto (K,K)
.
Tuttavia, non va oltre R[((I,K),(I,K))]
. Apparentemente, non riduce il termine se è nidificato. Questo è strano, perché ho provato lo stesso approccio ma con una vera funzione di runtime, e sembra funzionare correttamente ( Scastie ).
case object S
case object K
case object I
def r(t: Any): Any = t match {
case (((S,x),y),z) => r(((x,z),(y,z)))
case ((K,x),y) => r(x)
case (I,x) => r(x)
case (a,b) => r(a) match {
case `a` => (a, r(b))
case c => (c, r(b))
}
case _ => t
}
L'output di println(r((((S, I), I), K)))
è (K,K)
, come previsto.
Abbastanza interessante, la rimozione della regola per K
consente la compilazione, ma non riconosce (K, K)
e R[(K, K)]
come dello stesso tipo. Forse è questo che sta causando il problema? ( Scastia )
def check2: (K, K) = ??? : R[(K, K)]
//Found: R[(K, K)]
//Required: (K, K)
Risposte
S
, K
, e I
non sono disgiunti. Gli incroci K with I
ecc. sono abitati:
println(new K with I)
In un tipo di corrispondenza, un caso viene saltato solo quando i tipi sono disgiunti . Quindi, ad esempio, questo fallisce:
type IsK[T] = T match {
case K => true
case _ => false
}
@main def main() = println(valueOf[IsK[I]])
perché il case K => _
ramo non può essere saltato, poiché ci sono valori I
che sono K
s. Quindi, ad esempio, nel tuo caso R[(K, K)]
si blocca su case (I, x) => _
, poiché ci sono alcune (K, K)
s che sono anche (I, x)
s (ad esempio (new K with I, new K {})
). Non arrivi mai al case (a,b) => _
, che ci porterebbe a (K, K)
.
Puoi creare S
, K
, ed I
class
es, che li rende disgiunti, dato che non puoi ereditare da due class
es contemporaneamente.
class S
class K
class I
type R[T] = T match {
case (((S,x),y),z) => R[((x,z),(y,z))]
case ((K,x),y) => R[x]
case (I,x) => R[x]
case (a,b) => R[a] match {
case `a` => (a, R[b])
case _ => R[(R[a], R[b])]
}
case T => T
}
@main def main(): Unit = {
println(implicitly[R[(K, K)] =:= (K, K)])
println(implicitly[R[(((S,I),I),K)] =:= (K, K)])
}
Scastie
Un'altra soluzione è renderli tutti tipi singleton:
object S; type S = S.type
object K; type K = K.type
object I; type I = I.type
// or, heck
type S = 0
type K = 1
type I = 2