Programmation Avancée

TP10: Typage avancé

Exercices conçu par David Baelde

Variants polymorphes

Question 1

Déclarer un type récursif 'a list avec des variants polymorphes. Ecrire les fonctions map : ('a -> 'b) -> 'a list -> 'b list et equals : 'a list -> 'a list -> bool.

Vérifiez que vous obtenez bien les types attendus. Pour éviter les types illisibles, le mieux est de donner les types attendus dans des annotations ou dans une signature.

Question 2

Dans de nombreux algorithmes (par exemple, manipulation de texte) il est utile de ne pas calculer instantanément la concaténation de listes (ou de chaînes) mais de l'amortir. Pour supporter ceci, on étend notre type de listes avec un constructeur représentant la concaténation.

Indiquer pourquoi la déclaration suivante n'est pas pleinement satisfaisante, et corriger:

type 'a alist = [ 'a list | `Append of 'a list * 'a list ]

Ecrire amap : ('a -> 'b) -> 'a alist -> 'b alist, équivalent de map pour les listes concaténables, ainsi que l'aplatissement flatten : 'a alist -> 'a list qui effectue les concaténations.

Sans variants polymorphes, aplatir ne suffirait pas à obtenir une liste, il faudrait aussi convertir les constructeurs d'un type vers l'autre.

Corriger le code suivant et tester:

let () =
  let make = List.fold_left (fun a b -> `Cons (b,a)) `Nil in
  let a = make ['b';'l';'a'] in
  let b = `Append (a,a) in
    assert (equals b (make ['b';'l';'a';'b';'l';'a']))

Interprète et typeur fortement typés

On considère le mini-langage suivant, et le code permettant de l'interpréter:

(** AST non typé *)

type expr =
  | Int of int
  | String of string
  | Concat of expr*expr
  | Add of expr*expr
  | Substring of expr*expr*expr
  | Pair of expr*expr
  | Fst of expr
  | Snd of expr

(** Valeurs *)

type value =
  | VInt of int
  | VString of string
  | VPair of value*value

(** Evaluateur non typé *)

let rec eval = function
  | Int i -> VInt i
  | String s -> VString s
  | Concat (a,b) ->
      begin match eval a, eval b with
        | VString sa, VString sb -> VString (sa^sb)
        | _ -> failwith "eval error"
      end
  | Add (a,b) ->
      begin match eval a, eval b with
        | VInt sa, VInt sb -> VInt (sa+sb)
        | _ -> failwith "eval error"
      end
  | Substring (a,b,c) ->
      begin match eval a, eval b, eval c with
        | VString a, VInt b, VInt c ->
            VString (String.sub a b c)
        | _ -> failwith "eval error"
      end
  | Pair (a,b) -> VPair (eval a, eval b)
  | Fst e ->
      begin match eval e with
        | VPair (a,b) -> a
        | _ -> failwith "eval error"
      end
  | Snd e ->
      begin match eval e with
        | VPair (a,b) -> b
        | _ -> failwith "eval error"
      end

Question 1

Définir un GADT 'a wtexpr représentant les expressions bien typées, où le paramètre 'a prendra ses valeurs dans int, string, et les produits formés à partir de ceux-ci (par exemple, int*string*string).

Adapter l'interprète précédent pour en obtenir une version où le typage garantit qu'on obtient une valeur du bon type:

let rec wteval : type t. t wtexpr -> t = function ...

Question 2

On définit maintenant un type "singleton" représentant les types de notre mini-langage: le type OCaml t typ ne contient qu'une valeur, représentant le type de notre mini-langage correspondant à t.

type _ typ =
  | TInt : int typ
  | TString : string typ
  | TPair : 'a typ * 'b typ -> ('a*'b) typ

On se donne aussi un type "existentiel": un iswtexpr est un t wtexpr pour un certain t, auquel on attache une représentation de ce type t, qui sera utile si on veut calculer dessus:

type iswtexpr =
  | IsWT : 'a typ * 'a wtexpr -> iswtexpr

Implémenter une fonction de vérification de type qui prend une expression non typée expr, lève une exception si elle n'est pas typable, et sinon renvoie un iswtexpr:

let rec typecheck : expr -> iswtexpr = function ...

On pourra tester à l'aide du code suivant:

let test expr =
  let IsWT (t,e) = typecheck expr in
  let v = wteval e in
    match t with
      | TInt -> Printf.printf "-> %d\n" v
      | TString -> Printf.printf "-> %S\n" v
      | _ -> Printf.printf "<_,_>\n"

let () =
  (* Devrait afficher 15. *)
  test (Add (Int 3, Fst (Snd (Pair (String "", Pair (Int 12, Int 0))))))

Preuves d'inclusions d'automates finis

On se donne un type singleton pour représenter les mots sur un alphabet à deux lettres:

type 'w a = TA of 'w
type 'w b = TB of 'w
type nil = TEmpty

type ab = nil b a
type aab = nil b a a

type _ word =
  | A : 'w word -> 'w a word
  | B : 'w word -> 'w b word
  | Empty : nil word

let aba = A (B (A Empty))
let ab : ab word = A (B Empty)
let aab : aab word = A ab

On considère l'automate fini d'états n, m, f, h, e, o, avec les transitions suivantes:

n -a-> m -a-> m
       m -b-> f
(f acceptant)

h -(epsilon)-> e -b-> f
               e -a-> o
h -(epsilon)-> o -a-> e

Question 1

Définir un type singleton représentant les runs dans notre automate.

Définir un type ('w,'r) acc exprimant qu'un run 'r accepte un mot 'w (les valeurs de ce type sont des preuves d'acceptance).

Définir enfin un type 'w in_n qui exprime que 'w est reconnu par l'état n, c'est à dire qu'il existe un 'r tel que ('w,'r) acc est habité. Faire de même pour les états m et h.

Question 2

Ecrire une fonction qui "prouve" l'inclusion de langages entre n et m (la validité de cette preuve exigera bien sûr que votre fonction soit totale et suffisamment pure):

let n_in_m : type w. w in_n -> w in_m = function ...

Question 3

De même pour montrer que m est inclus dans h: on veut m_in_h : type w. w in_m -> w in_h.