Le typage de CAML VI

Le typage de CAML VI

Fonctions récursives

une fonction récursive est une expression fonctionnelle déclarée par let rec.

let rec f = function x -> corps

#let rec fact1 = function n ->
     if n <= 0 then 1 
     else n * fact1 (n-1);;
fact1 : int -> int = <fun>

Typage dans Env

Choisir deux nouvelles variables de type t₁ et t₂ pour désigner le type de f puis étendre Env Env' = ë (f:t₁ ® t₂), (x:t₁)<| Env û
typer corps (Env' |- corps : ty₂)
Faire le bilan des contraintes (t₁ = t₁ et t₂ = t₂)

(Rec)

ë (f:t₁ ® t₂), (x:t₁)<| Env û |- corps : t₂

Env |- rec f = function x -> corps : t₁ ® t₂