Como implementar o cálculo do combinador SKI com tipos de correspondência?

Question

Eu estava tentando implementar o cálculo do combinador SKI em Dotty usando tipos de correspondência.

Uma descrição rápida do cálculo combinador SKI:

• S, K, e Isão termos
• (xy)é um termo se xe ysão termos e é como aplicação de função
• (((Sx)y)z)(o mesmo que Sxyz) retorna xz(yz)(o mesmo que (xz)(yz))
• ((Kx)y)(o mesmo que Kxy) retornax
• (Ix)retornax

Abaixo está o que usei ( Rreduz o termo o máximo possível). Um termo (xy)é escrito como uma tupla (x,y), e S, Ke Isão traços.

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
}

No entanto, as 2 linhas a seguir não compilam (ambas pelo mesmo motivo) ( Scastie ):

val check: (K, K) = ??? : R[(((S,I),I),K)]
val check2: (K, K) = ??? : R[((I,K),(I,K))]

O erro diz que é necessário, (K,K)mas encontrado R[((I, K), (I, K))]. Eu esperava que ele primeiro visse o S e o transformasse em (IK)(IK), ou R[((I,K),(I,K))], após o que deveria corresponder à avaliação do primeiro (I, K)e ver que é K, o que não é o mesmo que (I, K), fazendo-o retornar R[(R[(I,K)], R[(I,K)])], o que se torna R[(K,K)], o que se torna justo (K,K).

No entanto, não vai além R[((I,K),(I,K))]. Aparentemente, não reduz o termo se estiver aninhado. Isso é estranho, porque tentei a mesma abordagem, mas com uma função de tempo de execução real e parece funcionar corretamente ( 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
}

A saída de println(r((((S, I), I), K)))é (K,K), como esperado.

Curiosamente, remover a regra for Kpermite compilar, mas não reconhece (K, K)e R[(K, K)]como do mesmo tipo. Talvez seja isso que está causando o problema? ( Scastie )

def check2: (K, K) = ??? : R[(K, K)]
//Found:    R[(K, K)]
//Required: (K, K)

Answer 1

S, K, e Inão são disjuntos. Os cruzamentos K with Ietc. são habitados:

println(new K with I)

Em um tipo de correspondência, um caso só é ignorado quando os tipos são separados . Então, por exemplo, isso falha:

type IsK[T] = T match {
  case K => true 
  case _ => false
}
@main def main() = println(valueOf[IsK[I]])

porque a case K => _ramificação não pode ser pulada, pois existem valores de Ique são K s. Portanto, por exemplo, no seu caso , R[(K, K)]fica preso em case (I, x) => _, pois existem alguns s (K, K)que também são (I, x)s (por exemplo (new K with I, new K {}), ). Você nunca chega ao case (a,b) => _, o que nos levaria a (K, K).

Você pode fazer S, Ke I classes, o que os torna disjuntos, já que você não pode herdar de dois classes ao mesmo tempo.

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

Outra solução é torná-los todos tipos 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