Inférence de type en Prolog

Pour ce TP vous pouvez travailler avec n'importe quel interpréteur Prolog, par exemple:

  • SWISH-Prolog (recommandé)
    • allez dans le notebook pré-rempli
    • dans le menu File/Save demandez un fork du notebook
    • faites des sauvegardes régulièrement
    • si vous voulez bien passer un compte Google à Swish-Prolog pour vous identifier, vous aurez quelques fonctionalités supplémentaires
  • Tau-Prolog
  • sur les machines du département, avec la commande swipl ou prolog
  • sur vos machines perso, vous pouvez aussi installer gnu-prolog
  • il y a plein d'extensions Visual Code pour faire du Prolog

Le but de ce TP est d'écrire un programme Prolog permettant de vérifier et d'inférer le type d'expressions Caml. On ne regardera qu'un petit fragment de Caml (que l'on appelera "micro Caml"), donné par la grammaire ci-dessous:

<expr> ::= 
    <var>
|   fun <var> -> <expr>
|   <expr> <expr>
|   (<expr>, <expr>)
|   fst
|   snd
|   true
|   false
|   <int>
|   <expr> + <expr>
|   <expr> = <expr>
|   if <expr> then <expr> else <expr>
|   ()
|   if <expr> then <expr>
|   <expr> ; <expr>

avec des types définis par la grammaire

<type> ::=
    <vartype>
|   <type> -> <type>
|   <type> * <type>
|   bool
|   int
|   unit

Étape 1 - le fragment fonctionnel

On se concentre d'abord sur le fragment vu en cours

<expr> ::= 
    <var>
|   fun <var> -> <expr>
|   <expr> <expr>


<type> ::=
    <vartype>
|   <type> -> <type>

On a vu comment on pouvait représenter une expression par un terme Prolog à l'aide des symboles de fonction fun/2 et app/2. On a vu la relation "l'expression $e$ est de type $\tau$ sous l'hypothèse de typage $\Gamma$ pour les variables libres de $e$", que l'on a notée $\Gamma\vdash e:\tau$, et on a vu comment axiomatiser cette relation en Prolog pour certaines expressions $e$ :

% Axiome
type([X, Alpha | _], X, Alpha).

% Affaiblissement
type([X, Alpha | Gamma], E, Tau) :- type(Gamma, E, Tau).

% Intro ->
type(Gamma, fun(X,E), arrow(Tau1,Tau2)) :-
	type([X, Tau1 | Gamma], E, Tau2).

% Elim ->
type(Gamma, app(E1, E2), Tau) :-
    type(Gamma, E1, arrow(Tau2, Tau)),
    type(Gamma, E2, Tau2).

Question 1.1 - vérifier le type d'une expression

Le terme Prolog fun(x,fun(y,app(y, x))) représente l'expression Caml fun x -> fun y -> y x. Trouvez son type avec Caml. Ce type se modélise par le terme Prolog arrow(Alpha,arrow(arrow(Alpha,Beta),Beta). Vérifiez que la requête

?- type([], fun(x,fun(y,app(y, x))), arrow(Alpha,arrow(arrow(Alpha,Beta),Beta))).

termine avec succès (on utilise le programme Prolog pour vérifier un type).

Question 1.2 - inférer le type d'une expression

Quel terme représente l'expression ci-dessous?

(fun x -> x (fun y -> y)) (fun z -> z) (fun t -> t)

À l'aide d'une requête appropriée, calculez son type avec Prolog, et vérifiez le résultat avec Caml (on utilise le programme pour inférer un type).

Dans la suite on fera toujours des tests d'inférence de types, mais n'hésitez pas à faire vos propres tests en vérification de type, en spécifiant le type attendu, comme à la question 1.

Étape 2 - le fragment fonctionnel, en mieux

Si vous ne parvenez pas à faire cette étape, vous pouvez quand même faire les étapes suivantes.

Question 2.1 - unification avec occurs check

Corrigez l'axiomatisation à l'aide du prédicat unify_with_occurs_check/2.

Indication: lisez rapidement ceci, en particulier la partie sur occurs check

Vérifiez qu'après avoir corrigé Prolog ne sait pas typer le terme qui représente l'expression Caml fun x-> x x.

Question 2.2 - analyse du problème avec les variables introduites plusieurs fois

Inférez le type de l'expression

fun x -> fun x -> x x

et observez que, comme mentioné dans le cours, Prolog parvient à typer cette expression, mais pas Caml.

Question 2.3 - correction du problème

Corrigez la règle d'affaiblissement pour ne pas avoir besoin de supposer que l'expression à typer n'introduit jamais deux fois la même variable avec fun. Idée: on n'applique pas la règle d'affaiblissement lorsque la règle d'axiome a échoué parce que les types n'étaient pas unifiables: si on a $\Gamma,x:\tau_1\vdash x:\tau_2$ et qu'on ne parvient pas à unifier $\tau_1$ et $\tau_2$, alors l'expression n'est pas typable, il ne faut pas aller chercher plus loin dans $\Gamma$, puisque s'il y a d'autres déclarations de types pour $x$ dans $\Gamma$, ce sont des $x$ qui sont "masqués" par le $x$ actuel.

Étape 3 - les couples

On s'intéresse maintenant aux expression Caml définies par la grammaire ci-dessous

<expr> ::= 
    <var>
|   fun <var> -> <expr>
|   <expr> <expr>
|   (<expr>, <expr>)
|   fst
|   snd

<type> ::=
    <vartype>
|   <type> -> <type>
|   <type> * <type>

On va modéliser les fonctions prédéfinies Caml fst et snd par des constantes Prolog fst/0 et snd/0, et on utilisera un symbole de fonction couple/2 pour représenter un couple Caml (e1,e2) par le terme Prolog couple(E1, E2). On utilisera enfin le symbole de fonction Prolog product/2 pour représenter le type produit tau1 * tau2 par le terme Prolog product(Tau1, Tau2).

Question 3.1 - axiomatisation des couples

Ajoutez trois règles (ou axiomes) Prolog à la définition de la relation type.

type(Gamma, fst, ...) :- ...
type(Gamma, snd, ...) :- ...
type(Gamma, couple(E1, E2), ...) :- ...

Question 3.2 - test

Testez votre code avec les requêtes suivantes

?- type([],fst, Tau)
% renvoie [Tau <- arrow(product(Alpha1, Alpha2), Alpha1)]

?- type([],snd, Tau)
% renvoie [Tau <- arrow(product(Alpha1, Alpha2), Alpha2)]

?- type([],fun(x,couple(x,x)), Tau)
% renvoie [Tau <- arrow(Alpha,product(Alpha, Alpha)]

?- type([],fun(x,couple(app(snd, x),app(fst, x)), Tau)
% renvoie [Tau <- arrow(product(Alpha1,Alpha2),product(Alpha2, Alpha1)]

Question 3.3 - test avancé

Cherchez plusieurs (au moins deux) expressions Caml (dans la grammaire ci-dessus) qui ne sont pas typables. Vérifiez avec les requêtes Prolog correspondantes que l'expression n'est effectivement pas typable. Vous laisserez les requêtes en commentaire.

Étape 4 - micro Caml

On s'intéresse au fragment de Caml mentionné en début de sujet. On fixe les symboles de fonction suivants en Prolog: true/0, false/0, entier/1, plus/2, egal/2, if/3, if/2, unit/0, seq/2 pour représenter les expressions Caml. Par exemple, l'expression Caml

if x=(1+y) then ( (); true ) else false

sera représentée le terme Prolog

if(egal(x,plus(entier(1),y)),seq(unit,true),false)

De plus, on introduit les symboles de fonction et de constantes Prolog suivants: bool/0, int/0, unit/0 pour représenter les types "de base" de micro Caml.

Question 4.1 - axiomatisation de micro Caml

Étendez l'axiomatisation de la relation type pour prendre en compte ces nouveaux éléments.

Question 4.2 - test

Testez votre code sur les expressions Caml suivantes; vérifiez votre résultat avec Caml, toutes les expression ci-dessous ne sont pas typables, votre code doit inférer le type quand il est inférable, et déclarer l'expression non typable lorsqu'elle n'est pas typable.

fun x -> x=1

fun x -> fun y -> x=y

fun x -> x=x+x

fun x -> fun y -> fun z -> if x then y else z

fun x -> if x then x else true

fun x -> if x then x else 1

fun x -> x ()

fun x -> fun y -> ( x; y )

fun x -> fun y -> if x then ( y (); 1 ) else 2

fun x -> fun y -> if x then y ()

fun x -> if x then x ()