L'inférence de type pour un modèle de données de calcul combinateur scala

Question

Je suis en train un encodage très léger du calcul Combinator dans scala. Dans un premier temps, je suis tout simplement mettre en œuvre les S et K combinateurs, l'application et des valeurs constantes. Plus tard, j'espère lever les fonctions et permettre à scala évaluation d'une expression en fonction de scala. Cependant, ce sera pour plus tard. Voici ce que j'ai à ce jour.

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

Maintenant, je voudrais faire une inférence de type à ce sujet. Pour simplifier la mise en œuvre de petites et de réduction à grande étape, le modèle de données est typées, donc je voudrais types être externe à cette structure. Introduisons quelque chose à retenir les informations de type.

trait TypeOf { type typeOf }

Le type de valeur est facile.

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

L'application est un peu plus difficile, mais se résume essentiellement à l'application de la fonction. Introduisons un type ? pour l'application de combinateur, pour éviter toute confusion avec l'application scala normale.

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

est où je suis bloqué. Je dois représenter le type des combinateurs S et K. Cependant, ils sont universellement types quantifiés. Vous ne savez pas leur type réel jusqu'à ce que vous commencez à les appliquer. Prenons K comme un exemple.

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

Les deux premières fois j'ai essayé de travailler avec cela, je fais K paramétrées comme K [X, Y], mais est (catastrophiquement) insuffisamment polymorphes. Le type de K doit être en attente pour le type du premier argument, puis de la suivante. Si vous appliquez K à une seule valeur, le type de l'argument suivant ne doit pas encore être fixé. Vous devriez être en mesure de prendre (K x: X). Et l'appliquer à une chaîne ou à un int ou tout ce que vous tapez comme

Donc mon problème est de savoir comment écrire l'implicite qui génère le typeof S et K, et comment gérer les types de ?-quantifiés correctement. Peut-être que je veux quelque chose comme ça?

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

Cependant, je ne sais pas comment je devrais écrire le type de ? faire la plomberie. J'ai le sentiment que, en plus d'obtenir ? droit, il y aura une deuxième implicite pour typeOfAp gérer A # typeof =: = ? [...] cas en plus de la sortie A # typeof =: = ? [ ...] un.

Merci,

Matthieu

Answer 1

Est-ce que cette aide?

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]