Scala 组合器微积分数据模型的类型推断

Question

我正在 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 参数化为 K[X, Y]，但这（灾难性地）不够多态。 K 的类型应该等待第一个参数的类型，然后等待下一个参数的类型。如果您仅将 K 应用于一个值，则下一个参数的类型应该尚未确定。您应该能够获取 (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 =:= ∀[...] 情况...] 一。

谢谢，

马修

Answer 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]