La inferencia de tipos para un modelo de datos de cálculo Scala combinador

Question

Estoy intentando a cabo una codificación muy ligero del cálculo combinador en Scala. Inicialmente, estoy simplemente la aplicación de los combinadores S y K, aplicación y valores constantes. Más tarde espero para levantar Scala de funciones y permitir la evaluación de una expresión como una función Scala. Sin embargo, eso es para más adelante. Aquí es lo que tengo hasta ahora.

/** 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

Ahora me gustaría hacer algún tipo de inferencia sobre esto. Para simplificar la implementación de la reducción de pequeña y gran paso, el modelo de datos no tiene tipo, así que me gustaría tipos para ser externos a esta estructura. Vamos a introducir algo para mantener la información de tipo.

trait TypeOf { type typeOf }

El tipo de valor es fácil.

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

La aplicación es un poco más complicado, pero básicamente se reduce a la aplicación de funciones. Vamos a introducir un tipo ? para aplicación combinador, para evitar confusiones con aplicación normal 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 }

Aquí es donde se queda bloqueado. Necesito para representar el tipo de los combinadores S y K. Sin embargo, son universalmente tipos cuantificados. Usted no sabe su tipo real hasta que empiece a aplicarlas. Tomemos como ejemplo K.

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

El primer par de veces que trató de trabajo con este, hago K parametriza como K [X, Y], pero esto es (catastróficamente) insuficientemente polimórfico. El tipo de K debe estar esperando para el tipo del primer argumento, y después de la siguiente. Si se aplica K a sólo un valor, entonces el tipo del siguiente argumento no debe sin embargo ser fijo. Usted debe ser capaz de tomar (K X: X). Y aplicarlo a una cadena, o para un int o lo que escribir como

Así que mi problema es cómo escribir el implícito que genera el TypeOf para S y K, y cómo manejar los tipos ?-cuantificado correctamente. Tal vez quiero algo como esto?

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

Sin embargo, no estoy seguro de cómo debería estar escribiendo el tipo ? hacer la instalación de cañerías. Tengo la sensación de que, además de conseguir ? derecha, habrá un segundo implícito para manejar la typeOfAp A # = TypeOf: = ? [...] caso, además de la salida de A # = TypeOf: = ? [ ...] uno.

Gracias,

Matthew

Answer 1

¿Esto ayuda?

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]