Site du prof cours – gio(at)irif.fr
Site du prof TD – geoffroy(at)irif.fr
Dépôt
TP : https://pfav.ddns.net/ (token : pfa)

Application partielle ew

Si v est une valeur avec un type fonctionnel (n arguments) polymorphe, l’application partielle (i.e. avec k arguments, 0<k<n) de f donne une valeur avec un type polymorphe faible.

Exemple

let id x = x (* identité *)
let f1 g = fun x -> g x
;;

f1 id (* application partielle *)
(* Dans un mode avec OCaml est naïf *)
f1 : 'a -> 'a

(* Dans notre mode *)
f1 : ('a -> 'b) -> 'a -> 'b

Autre exemple

let id x = x (* identité *)
let f2 g = let r = ref [] in
           fun x -> r := x :: (!r);
                    g x

f2 id
(* OCaml pourrait typé la fonction comme suit *)
f2 : ('a -> 'b) -> 'a -> 'b (* Comme f1! *)

(* Dans le monde OCaml-naïf *)
let h = f2 id
h : 'a -> 'a (* avec *) !r = []

let z1 = h true
=> true : bool (* avec *) !r = [ true ]

let z2 = h "abc"
=> "abc" : string (* avec *) !r = [ "abc" ; true ] (* deux types différents ??? *)

Le seul moyen de s’en sortir c’est avec un type faible

f1 : '_weak1 -> '_weak1
f2 : '_weak1 -> '_weak1

On peut se sortir de ce genre de problème via un état expansion :

let phrase8 = (fun x y -> (x, y)) 0
val phrase8 : '_weak1 -> int * '_weak1 = <fun>

let f = fun z -> (fun x y -> (x, y)) 0 z
val f : 'a -> int * 'a = <fun>