9

私はスカラでコンビネータ計算の非常に軽量なエンコーディングを試しています。最初は、S コンビネータと K コンビネータ、アプリケーション、および定数値を実装しているだけです。後で、スカラ関数を持ち上げて、式をスカラ関数として評価できるようにしたいと考えています。ただし、それは後ほど。これが私がこれまでに持っているものです。

/** Combinator expression */
sealed abstract class CE

/** Application: CE| (x y) <=> LC| (x:(A=>B) y:A) : B */
case class Ap[A <: CE, B <: CE, X](e1: A, e2: B) extends CE

/** A raw value with type */
case class Value[T](v: T) extends CE

/** Some combinator */
sealed abstract class Comb extends CE

/** The S combinator: CE| S x y z
 *                    LC| λx:(A=>B=>C).λy:(A=>B).λz:A.(x z (y z)) : C
 *  S : ∀A.∀B.∀C. (A => B => C) => (A => B) => A => C
 */
case object S extends Comb
/** The K combinator: CE| K x y
 *                    LC| λx:A.λy:B.x:A : A
 *  K : ∀A => ∀B => A
 */
case object K extends Comb

ここで、これについていくつかの型推論を行いたいと思います。スモール ステップ リダクションとラージ ステップ リダクションの実装を簡単にするために、データ モデルは型指定されていないため、型をこの構造の外部に配置したいと考えています。型情報を保持するものを導入しましょう。

trait TypeOf { type typeOf }

値型は簡単です。

implicit def typeOfValue[T](vt: Value[T]) : TypeOf =
    new TypeOf { type typeOf = T }

アプリケーションはもう少しトリッキーですが、基本的には関数アプリケーションに要約されます。通常の scala アプリケーションとの混同を避けるために、コンビネータ アプリケーションに型 ⊃ を導入しましょう。

/** Combinator application */
class ⊃[+S, -T]

implicit def typeOfAp[Ap[A, B], A <: CE, B <: CE], X, Y](Ap(A, B)
  (implicit aIsFXY: A#typeOf =:= (X⊃Y), bIsX: B#typeOf =:= X) : TypeOf =
      { type typeOf = Y }

これは私が立ち往生するところです。S コンビネータと K コンビネータの型を表す必要があります。ただし、それらは普遍的に量化された型です。それらを適用し始めるまで、実際のタイプはわかりません。Kさんを例に挙げてみましょう。

(K x:X y:Y) : X
(K x:X) : ∀Y.Y => X
(K) : ∀X.x => ∀Y.Y => X

これを使用しようとした最初の数回は、K を K[X, Y] としてパラメーター化しましたが、これは (壊滅的に) ポリモーフィック性が不十分です。K の型は、最初の引数の型を待ってから、次の引数の型を待つ必要があります。K を 1 つの値だけに適用する場合、次の引数の型はまだ固定されていません。(K x:X) を取得して、文字列、int、または好きな型に適用できるはずです。

したがって、私の問題は、S と K の typeOf を生成する暗黙の記述方法と、∀ 量化された型を正しく処理する方法です。ひょっとして、こんなものが欲しいのかな？

implicit def typeOfK(k: K.type): TypeOf = { type typeOf = ∀[X, X ⊃ (∀[Y, Y⊃X])] }

しかし、配管を行うために∀型をどのように記述すればよいかわかりません。∀ を正しく取得することに加えて、既存の A#typeOf =:= ⊃[ に加えて、 typeOfAp が A#typeOf =:= ∀[...] ケースを処理するための 2 番目の暗黙的なものがあると感じています。 ...] 1。

ありがとう、

マシュー

4

1 に答える 1

1

これは役に立ちますか？

trait λ {
    type ap[X] <: λ
}

type K = λ {
    type ap[X<:λ] = λ {
        type ap[Y<:λ] = X
    }
}

type S = λ {
    type ap[X<:λ] = λ {
        type ap[Y<:λ] = λ {
            type ap[Z<:λ] = X#ap[Z]#ap[Y#ap[Z]]
        }
    }
}

type I = S#ap[K]#ap[K]

def ap[X<:λ,Y<:λ](x:X,y:Y): X#ap[Y]
于 2011-03-07T23:54:46.833 に答える