L'inférence de type pour un modèle de données de calcul combinateur scala
-
13-10-2019 - |
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
La solution
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]