PML

PML : Proved ML or Programmable Mathematical Logic

La page web

User's manual

Sujets de discussions en cours

• Compilo? Cible probable LLVM.
• Généralisation.
• Spécifications et preuves.
• Exemples (notamment en utilisant "untyped").
• Mise à jour de la doc.
• Révisions: PML le langage.

Syntaxe de PML

Termes

 fun x->u 

ou

 \x.u
 
 u v

Variants polymorphes

 A[…]

Rien, c'est

 {}

Pattern matching:

 A[x] -> …

Héritage ouvert pour les sommes

 match … with
 | A[x] -> …
 | B[x] -> …
 …
 | _    -> …   <= attrape vraiment tout

Cas problématique

 match f x with 
 | A[] ,  _  -> …
 |  _  , A[] -> …
 | B[] , B[] -> …

Râle pour cause de pattern matching incomplet, parce qu'on ne connaît pas le produit $E\times F$ qui étend $E'\times F'\cup E''\times F''$.

Il suffit de donner le type de x.

Héritage multiple (fermé)

 | A[?x] … -> …  

matche tous les variants du membre droit (doit être fini)

Cas d'utilisation

 type a_expr (expr) =  Add[expr] | …
 type p_expr (expr) = Pair[expr] | …
 
 val eval_a_expr ev = function
     Add[x] -> 
   | …
 
 val eval_p_expr ev = function
     Pair[x] -> 
   | …
 
 val rec eval_tout x = match x with 
   | ?x -> eval_a_expr eval_tout x
   | ?x -> eval_p_expr eval_tout x

À venir dans les patterns

Digression sur les entiers:

 nat16, nat32, nat64  <= Z/(2^k)Z
 int                  <= big_nat / GMP

Et on pourra écrire:

| %fun as f ->
| %nat32 as n ->       <= force à boxer 

Les records

 { val x  = …  <= normal
 { val x == …  <= champs utilisables uniquement dans les
                  preuves et les autres champs « == »
                  i.e. on teste que c'est jetable à la compil
 { val x =: …  <= champs toujours inlinés
                  champs dont la valeur fait partie des contraintes de types
                  restriction: ne peut parler que des champs précédents 
                  du même record
                  statut à clarifier dans les « val rec » 
                  à l'intérieur des preuves
 

Le lieur n'est pas forcément le label:

 { val x as toto  <= x est le nom du champ, mais on l'appelle toto 
                     dans la suite du record

Exemple:

 { 
   val x as y = … ,
   val f = … y … 
 }.x

Les tableaux (à venir)

 type toto = { 
         val size : int,
         val a[0...size]: …
         val b[1...size]: …
       

même contrainte que pour « =: »

Héritage ouvert pour les records

 { x with val l = … }

x n'est pas forcément un record.

Exemple:

 { \x.x with val l = … }

Si x est un record, le champ par défaut de

 { x with … } 

est le champ par défaut de x.

Héritage multiple

 { x with
         val …
         include r       <= recopie r 
                            (sauf le champ par défaut, et les champs qui sont
                            écrasés après [note: en général, on ne peut pas écrire:
                                  { val l = … , val l = … }
                            ])
                            il est nécessaire de connaître tous les champs de r
                            en particulier le champ par défaut de r ne doit pas
                            être un record indéterminé (cette restriction ne
                            s'applique pas à x, qu'on est en train d'étendre)

Note:

• le champ par défaut: analogue du _ dans le pattern matching
• le ?x du pattern matching: dual du include

Erreurs et exceptions

 raise u    //     try x = … in … with e -> … 
 error u    //     rien: on ne rattrape pas les erreurs

On a le droit à

 let try x = …

À voir:

 open try r in …       <= gnih ? 

Preuves

Une preuve c'est un terme qui a le type vide.

 [ t proof p ]  <= p prouve que t ne lève ni exception ni erreur
                   p est typé sous l'hypothèse que t diverge

Exemples

 [ A[] proof 8< ]

 if b then [ f b proof 8< ] else …

Sucre

Dans les records:

 val f x |- p proof q …

c'est:

 val f =: \x.[if p then {} else error {} 
              proof if p then 8< else q ]

La suite

• types
• polymorphisme
• subtilités sur except et without dans l'héritage (patterns et records)