Come implementare il calcolo del combinatore SKI con i tipi di corrispondenza?

Aug 22 2020

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, e Isono termini
  • (xy)è un termine se xe ysono termini ed è come l'applicazione di una funzione
  • (((Sx)y)z)(uguale a Sxyz) restituisce xz(yz)(uguale a (xz)(yz))
  • ((Kx)y)(uguale a Kxy) restituiscex
  • (Ix)ritornax

Di seguito è quello che ho usato ( Rriduce il termine il più possibile). Un termine (xy)è scritto come una tupla (x,y)e S, Ke Isono 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 Kconsente 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

4 HTNW Aug 25 2020 at 02:32

S, K, e Inon sono disgiunti. Gli incroci K with Iecc. 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 Iche 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 classes, che li rende disgiunti, dato che non puoi ereditare da due classes 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