Scala Combinator Calculusデータモデルの推論を入力します
-
13-10-2019 - |
質問
Scalaのコンビネーター計算の非常に軽量のエンコードを試しています。当初、私は単にSとKの組み合わせ、アプリケーション、および一定の値を実装しています。その後、SCALA機能を持ち上げ、Scala関数としての式の評価を許可したいと考えています。しかし、それは後でです。これが私がこれまでに持っているものです。
/** 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 [x、y]としてkをパラメーターにしますが、これは(壊滅的に)不十分な多型です。 Kのタイプは、最初の引数のタイプを待っている必要があります。 Kを1つだけの値に適用する場合、次の引数のタイプはまだ修正されてはなりません。 (k x:x)を取得し、文字列、またはintまたは好きなタイプに適用できるはずです。
したがって、私の問題は、sとkのタイプを生成する暗黙をどのように記述するか、そして∀Quantified型を正しく処理する方法です。多分私はこのようなものが欲しいですか?
implicit def typeOfK(k: K.type): TypeOf = { type typeOf = ∀[X, X ⊃ (∀[Y, Y⊃X])] }
ただし、配管を行うために∀タイプをどのように書くべきかわかりません。正しく取得することに加えて、a#typeof =:=∀[...]の場合、#typeof =:=⊃[= =⊃[]に加えて、typeofapが処理するための2番目の暗黙があると感じています。 ...] 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]