How to implement the SKI combinator calculus with match types?

I was trying to implement the SKI combinator calculus in Dotty using match types.

A quick description of the SKI combinator calculus:

• S, K, and I are terms
• (xy) is a term if x and y are terms and is like function application
• (((Sx)y)z) (same asSxyz) returns xz(yz) (same as (xz)(yz))
• ((Kx)y) (same as Kxy) returns x
• (Ix) returns x

Below is what I used (R reduces the term as much as possible). A term (xy) is written as a tuple (x,y), and S, K, and I are traits.

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
}

However, the following 2 lines don't compile (both for the same reason) (Scastie):

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

The error says that it required (K,K) but found R[((I, K), (I, K))]. I expected it first see the S and turn it into (IK)(IK), or R[((I,K),(I,K))], after which it should match the evaluation of the first (I, K) and see that it is K, which is not the same as (I, K), making it return R[(R[(I,K)], R[(I,K)])], which becomes R[(K,K)], which becomes just (K,K).

However, it doesn't go beyond R[((I,K),(I,K))]. Apparently, it does not reduce the term if it's nested. This is odd, because I tried the same approach but with an actual runtime function, and it appears to work properly (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
}

The output from println(r((((S, I), I), K))) is (K,K), as expected.

Interestingly enough, removing the rule for K lets it compile, but it doesn't recognize (K, K) and R[(K, K)] as the same type. Perhaps this is what is causing the problem? (Scastie)

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

S, K, and I are not disjoint. The intersections K with I etc. are inhabited:

println(new K with I)

In a match type, a case is only skipped when the types are disjoint. So, e.g. this fails:

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

because the case K => _ branch cannot be skipped, since there are values of I that are Ks. So, e.g. in your case R[(K, K)] gets stuck on case (I, x) => _, since there are some (K, K)s that are also (I, x)s (e.g. (new K with I, new K {})). You never get to the case (a,b) => _, which would take us to (K, K).

You can make S, K, and I classes, which makes them disjoint, since you can't inherit from two classes at once.

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

Another solution is making them all singleton types:

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