マッチタイプでSKIコンビネータ微積分を実装するにはどうすればよいですか?

Aug 22 2020

マッチタイプを使用して、DottyにSKIコンビネータ計算を実装しようとしていました。

SKIコンビネータ計算の簡単な説明:

  • SK、およびI用語であります
  • (xy)は用語でxあり、yは用語であり、関数適用のようなものです
  • (((Sx)y)z)(同じSxyz戻り)xz(yz)(同じ(xz)(yz)
  • ((Kx)y)(と同じKxy)が返されますx
  • (Ix) 戻り値 x

以下は私が使用したものです(R可能な限り用語を減らします)。用語は(xy)タプルとして書かれている(x,y)、とSKと、I形質です。

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
}

ただし、次の2行はコンパイルされません(両方とも同じ理由で)(Scastie):

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

エラーは、それが必要である(K,K)が見つかったことを示していますR[((I, K), (I, K))]。最初にSを見て(IK)(IK)、またはに変換し、R[((I,K),(I,K))]その後、最初の評価と一致し、(I, K)それがK、と同じではないことを確認して(I, K)、それを返すことを期待しました。これはR[(R[(I,K)], R[(I,K)])]、になりR[(K,K)]、はちょうどになります(K,K)

ただし、それを超えることはありませんR[((I,K),(I,K))]。どうやら、それがネストされている場合、それは用語を減らしません。同じアプローチを試しましたが、実際のランタイム関数を使用していて、正しく機能しているように見えるため、これは奇妙です(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
}

からの出力println(r((((S, I), I), K)))(K,K)、予想どおりです。

興味深いことに、のためのルールを削除しK、それはコンパイルできますが、それは認識していない(K, K)R[(K, K)]同じタイプとして。おそらくこれが問題の原因ですか?(スカスティ)

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

回答

4 HTNW Aug 25 2020 at 02:32

SKI互いに素ではありません。交差点K with Iなどに人が住んでいます:

println(new K with I)

マッチタイプでは、タイプが互いに素である場合にのみケースがスキップされます。したがって、たとえばこれは失敗します:

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

case K => _sでIあるため、ブランチをスキップできないためです。したがって、たとえば、s(eg )でもあるいくつかのsあるため、たとえば、あなたの場合はスタックします。あなたはに取得することはありませんに私たちを取ることになります、。 KR[(K, K)]case (I, x) => _(K, K)(I, x)(new K with I, new K {})case (a,b) => _(K, K)

あなたは作ることができるSKI classあなたは2から継承することができないので、彼らはばらばらになり、ES、class一度にES。

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)])
}

スカスティ

別の解決策は、それらをすべてシングルトンタイプにすることです。

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