Table of Contents

1. Using pml(top)

1.1. The toplevel loop(top)

The toplevel loop is not working at the moment... If you have ideas about the semantics and design of this, please contact us.

1.2. The interpreter(top)

If you just type "$ pml file.pml", then PML will type-check and proof-check your file your file and it will run it and display the result. The available options are displayed using the -h or --help flag.

``examples/simple/first.pml``
open int

val square n = n * n

val big = square 100

Example: if you have the (simple) program above in a file named first.pml and type "$ pml first.pml" in your favorite terminal, you should get:

Correct pml code
$ pml first.pml
{val big = int%10000 val square = fun ...}

Note that the value of the function square is not displayed.

1.3. The compiler(top)

No compiler is available at the moment. An optimized llvm based compiler is planed for the near future.

You can "compile" a file using $ pml -c file.pml. This will only type-check and proof-check the file without running it.

2. Arithmetic(top)

By opening the int module, you can access the usual arithmetic operations on integers:

``examples/simple/second.pml``
open int
val x = 2 + 3 * 5
val y = x * x - x
val z = y % 2

There is some magic that needs to be explained here. If you read the file $PML_ROOT/lib/int.pml from the distribution, you will see lines such as:

Correct pml code
val add = int%add

This defines add as an internal function (internal means not defined in PML) performing addition on the predefined data-type int%. Then, the symbol + will have access to all functions named add and will disambiguate this using typing.

The same happens for constants. A constant of type int should be written int%123. When you write 123, PML does its best to guess what you actually mean...

Remark: int is the type of integers of arbitrary size, currently using the bignum library of OCaml. When compilation is available, it will probably correspond to GMP arbitrary precision integers. PML also knows about 32 and 64 bits integers (more sizes will be supported in the future, but we currently only support the sizes that are directly accessible in OCaml). Here is an example:

``examples/simple/third.pml``
open int
open int32
open int64

val x = 123456:int32
val y = 1234567890:int64
val z = 12345678901234567890:int
val x' = 2*x*x + 1
val y' = 2*y*y + 1
val z' = 2*z*z + 1
untyped (x' + y')

This example needs further explanation: The last line starting with the keyword untyped means that the following expression should not be accepted (PML will display an error message if it is accepted). Here x' is of type int32 and y' is of type int64 and there is no add function taking argument with such type. Language like C would automatically convert x' to an int64 but this is considered harmful by the PML developers. Indeed, conversion from int32 to int64 is not a morphism in the mathematical sense, which means that the result of an expression using some conversion is not canonical.

3. Functions(top)

It is very easy to define functions in PML. Let us start with an example:

Correct pml code
open int
val double n = n + n
val square = fun n -> n * n
val norm_square = \n p. square n + square p
val f n m p q = p * q + norm_square n m

We see here various syntaxes for function. The syntax fun x y z -> is equivalent to \x y z. and when defining a value with the val keyword, val f x y z = is equivalent to val f = fun x y z ->.

A very common error is to write the following:

Incorrect pml code (with error message)
open int
val pred x = x-1
val test = pred 3
Pml output
Type error at /tmp/tmpS2V5y2.pml: line 3 column 11 to column 15: 
---
int% at line 3 column 16 to column 17
  used as 
functions at line 2 column 13 to column 16

Here PML is detecting an error at the third line, saying that the integer at the third line, in used as a function at the first line. PML understood x (-1) that is a function applied to -1. one should write x- 1 or better x - 1.

One can also define recursive function as follows:

Correct pml code
open int
open bool
val rec fact n = if n = 0 then 1 else n * fact (n - 1)
val rec fib n = if n = 0 || n = 1  then 1 else fib (n - 1) + fib (n - 2)

We recognize here the classical factorial function and Fibonacci sequence. Notice that the keyword rec is mandatory to inform PML that we define a recursive function. val x = x + 1 defines x using the old value of another variable named x. We say that we are shadowing x.

We can also define mutually recursive functions:

4. Local definitions(top)

One can give local definitions. Here is the definition the arithmetico-geometric mean which is the limit we obtain by computing the arithmetic and geometric mean of two numbers and continuing until we reach the limit (here we take the arbitrary value of 50 to stop the loop:

``examples/simple/ag_average.pml``
open float64
open int

val AG_average n m = 
  let rec f i:int n m =
    if i = 0 then m else f (i - 1) ((n + m) / 2) (sqrt (n * m)) in
  f 20 n m

Notice that in this example, we mix integer and floating point number. For n and m, PML knows that they are float because of the use of the function sqrt which does not exist for integer. However, for the parameter i, we have to help PML by indicating its type at one place writing i:int.

5. Lists(top)

Lists are data structures which are very common in functional programming. The syntax for finite list is [x1;x2;x3;...] which includes the empty list as []. One can also add an element x at the top of a list l using the syntax x::l. As an example, here is a function defining the list of integers from 1 to n:

Correct pml code
open int

val enum_int n =
  let rec fn acc p =
    if p = 0 then acc else fn (p::acc) (p - 1)
  in fn [] n

To read a given list, if you do not use the functions provided in the library $PML_ROOT/lib/list.pml, you need to use pattern matching. Let us start with an example, the traditional append function (sometimes named concat) thats add all the elements of a first list at the top of the elements of a second list.

Correct pml code
val rec append l1 l2 = 
  match l1 with
  | [] -> l2
  | x::l1' -> x::(append l1' l2)
  endmatch

One can see that pattern matching uses three keywords match, with and endmatch. The last keyword is not mandatory to end pattern matching, but is necessary when using nested pattern matching. Between match and with is an expression that is computed and matched against each pattern occurring between the vertical bar and the arrow. A list matches the empty list pattern [] if and only if it is the empty list. A list l1matches the pattern x::l1' if there exists two value x and l1' such that l1 is equal to x::l1'. The variable x and l1'are bound in the right hand side of the pattern case. The result of pattern matching is the right hand side of the first pattern matching the given value.

One can also match more that the top element of a list. Here is an example:

Correct pml code
open bool
val rec is_sorted cmp l = match l with
  | [] | [_] -> true
  | x::(y::_ as l) -> cmp x y && is_sorted cmp l   

This function tests if a list is sorted by comparing adjacent elements. One may notice the or-pattern in the first case, matching both lists with 0 or 1 elements and the catch-all written _ which avoid to waste unused identifier names. In the second cas, one may notice the as feature which allows to give a name both to the tail of the list (here l) and its second element (here y).

6. Tuples(top)

Very often, one needs to manipulate (ordered) pairs, tripple, ... On common case for this are functions returning more than one values. This is not possible in traditional functional language, thus tuple are used for this.

The syntax for tuple is a comma separated sequence of expression. Parenthesis are not mandatory (in mathematics, they are) but it is a good practice to write them.

Here is a classical example: a function taking a list of pairs a returning two lists:

Correct pml code
val rec split l = match l with
  | [] -> [], []
  | (x,y)::l' -> let (l1, l2) = split l' in ((x::l1), (x::l2))
  endmatch

On may notice in this example the use of a pattern in a local definition. let l1, l2 = split l' in x::l1, x::l2 is a shortcut for a pattern matching with one cases.

7. Types(top)

One can write type definitions in PML and indicate the types of expressions in a program. But, what is a type ? It denotes a set of expressions and in fact in PML.

Here is a simple example:

Correct pml code
open int
open list
type seq = list(int)

val sum 
  : (seq -> int)
  = fun l ->
    let rec fn acc l = match l with
      | [] -> acc
      | n::l' -> fn (n + acc) l'
    in fn 0 l

val test = sum [1;2;3;4;5;6;7;8;9;10] 

Here we notice the definition of the type seq as list of integers, using the type int and list from the libraries with the same names. We also remark that the type list as one parameter (as expected). Then, in the definition of the sum that computes the sum of all integers in the list, we remark that we first give its type seq -> int meaning that it is a function taking a list of integer and returning an integer.

Here, we have seen atomic types like int, int32 and function type written t1 -> t2 if t1 and t2 are types. There are other notion of types that we will introduce later.

We have also see type definition written:

Pseudo code
type t = ...

8. Polymorphic variants (disjoint sum)(top)

It is very useful when programming to consider data types that can have different cases for their values. This is done by forming a (disjoint) sum or a (polymorphic) variant:

In fact lists are a particular case of variants with two cases: [] which is an abbreviation for Nil[] and x::l which is an abbreviation from Cons[x,l]. The booleans true and false are also abbreviations for the variants True[] and False[].

The first simple use of sums is for comparison. Indeed, it is often useful to perform a comparison test with three cases and for this, we use comparison function returning either Less[], Equal[] or Greater[]. The function compare available for instance for int does that. Here is an example of function computing the lexicographic combination of two comparisons:

Correct pml code
val lexicographic (cmp1, cmp2) (n, m) (n', m') = 
  match cmp1 n n' with
  | Equal[] -> cmp2 m m'
  | r -> r

val lexicographic_int2 = lexicographic (int.compare, int.compare)

val test = open int in lexicographic_int2 (1,2) (1,3)

Here we see that the syntax of variants uses square bracket. Two variants with distinct names will be considered as distinct values by PML.

We can use sums for other data types. Here is for instance a function performing insertion in an ordered binary tree. The order is defined by the first argument of insertion and uses the constructor introduced in the previous example. We represent the tree with left, right as a left and right sons and data as data by Node[left,data,right] and the empty tree by Nil[] (because PML has polymorphic variants we can reuse constructors among different data types).

Correct pml code
val rec insert cmp data tree =
  match tree with
    [] -> Node[[],data,[]]
  | Node[left,data',right] ->
    match cmp data data' with
      Less[] -> Node[insert cmp data left, data', right]
    | Greater[] -> Node[left, data', insert cmp data right]
    | Equal[] -> tree
    endmatch
  endmatch 

8.1. Default case in pattern matching (open inheritance for sum types)(top)

Because PML uses polymorphic variant which means that many data structures can use the same constructor. This as the advantage of being able to write such function:

Correct pml code
val merge_option o1 o2 =
  match o1, o2 with
    None[], None[] -> None[]
  | None[], y -> y
  | x, _ -> x

This function can be used with o1 and o2 of arbitrary data-types except atomic type like int, int32, int64, float64, ... More precisely, o1 and o2 can be arbitrary sum constructor, tuples, functions and structure that will be introduced below.

8.2. Deep pattern matching problems(top)

The following function definition is not accepted by PML:

Incorrect pml code (with error message)
val f x y = match x, y with
  | A[] ,  _  -> y
  |  _  , A[] -> x
  | B[] , B[] -> B[]
Pml output
Incomplete patterm matching at: /tmp/tmpS2V5y2.pml: line 2 column 4 to column 12

The reason is the following: pattern matching on tuples must match a Cartesian product. But if there is more than one case, in general, the values accepted by a list of patterns is a union of Cartesian products. Unfortunately, a union of products is not a product and there is no larger product included in a union of products.

In the above example, the following Cartesian products are covered by all cases: (? * [ A[] ]), ([ A[] ] * ?) and ([ A[] | B[] ] * [ A[] | B[] ]). Clearly, the two first cases would mean that the last pattern is useless. But PML's developers consider that disambiguation of deep pattern matching based on useless cases may be misleading.

To help PML, it is enough to give the type of x and y as follows:

Correct pml code
val f x y = match (x:[A[]|B[]]), (y:[A[]|B[]]) with
  | A[] ,  _  -> y
  |  _  , A[] -> x
  | B[] , B[] -> B[]

It may be clearer to give a name to the type:

Correct pml code
type A_or_B = [A[]|B[]]

val f x:A_or_B y:A_or_B = match x, y with
  | A[] ,  _  -> y
  |  _  , A[] -> x
  | B[] , B[] -> B[]

8.3. Closed inheritance for sum types(top)

Pseudo code
  | ?x -> ...

?x matches all the variants that are accepted by the right member of the case. There must be only finitely many possibilities. ?x can be used in deep pattern. In fact, ?x in a pattern in a syntactic sugar for (A1[_] | ... | An[_]) is A1, ..., An is the largest list of pattern accepted by the right member of the case.

Here is an example of utilisation (the complete example can be found $PML_ROOT/tests/eval.pml). The idea is to write two functions eval_a_expr and eval_p_expr working on separate variant types a_expr and p_expr and be able to do the union of the two functions in the eval_all function.

Pseudo code
  type a_expr (expr) = [ Add[expr] | ... ]
  type p_expr (expr) = [ Pair[expr] | ... ]

  val eval_a_expr rec_eval = function
      Add[x,y] -> rec_eval x + rec_eval y
    | ...

  val eval_p_expr rec_eval = function
      Pair[x,y] -> (rec_eval x, rec_eval y)
    | ...

  val rec eval_all x = match x with
    | ?x -> eval_a_expr eval_all x
    | ?x -> eval_p_expr eval_all x

Remark: only the final function is recursive, the intermediate functions have an extra arguments rec_eval which whose value will be given only in the final recursive function.

9. Records, tuple and structure(top)

9.1. Basic syntax(top)

We have already seen tuple. In fact tuples are just a syntactic sugar for records. Moreover, records can be used as structures (also called modules). For instance, a pml file is nothing but a large records without the initial and final curly braces.

The syntax for records is a list of definition enclosed by curly braces. Basic definitions are given with the following syntaxes:

Pseudo code
  { val x = ... val y = ... val z = ... }

or

Pseudo code
  { x = ...; y = ...; z = ...; }

Remark: val and semicolon terminated definitions can be mixed, but one sometimes needs a semicolon at the end of a val definition. This is why it is allowed to have a semicolon at the end of a definition introduced by the val keyword.

Records can contain recursive or mutually recursive definition with the following syntax:

Pseudo code
  { val rec f1 = ... and f2 = ... }

It can also contains type and recursive type definitions using the following syntax

Pseudo code
  { type t0 = ... type rec t1 = ... and t2 = ...

A section is dedicated to type later in this document.

When we build a record, eash field can be used to define the following fields (or even the same field when using rec. Here is an example:

Pseudo code
  { val x = 1 val y = x + 1 }

The field identifier here is used both as a field ame used for projection and a binding name for the value in the rest of the record. Both name may be different is you wish:

Pseudo code
  { val number_x as x  = 1 val number_y = x + 1 }

To access the element of a record, one uses the dot notation. The following code will evaluate to A[]:

Pseudo code
  let r = {  a= A[]; b = B[] } in r.a

9.2. Open Inheritance, default field of records(top)

It is possible to define a record from an initial record even if we do not know the exact set of labels this record have. Moreover, a record has a default field, which can sometimes (we will see why later) be accessed without projection. The syntax for both feature is:

Pseudo code
  { r with ... } 

or

Pseudo code
  { r | ... } 

The above syntax can be used for any value of r. If r is not a record, then r will be the default field of the resulting record. For instance, if r is a function, the whole record can be applied to an argument. Here is an example:

Correct pml code
val r = { fun x -> x with val id = A[] }

val x = r B[]
val a = r.id

This feature will be used a lot to add specifications to functions.

Sometimes one wants to remove/select some fields of the record r, or one may want to prevent some field to be present in r. Here is the syntax for that:

Pseudo code
  { r forbid l1,...,ln with ...}
  { r remove l1,...,ln with ...}
  { r select l1,...,ln with ...}
  { r authorize l1,...,ln with ...}

In the above, forbid means that the field l1,...,ln must be absent; remove means that these fields will be removed if present; select means that we only keep the fields present in r which are among the given fields and finally, authorize means that no other fields than those given are present in r.

These keywords can be combined together in any order as in the following example:

Pseudo code
  { r forbid a remove b with ...}

The keyword fresh can be used in front of any definition to add it implicetely in the forbid list. { r with fresh a = ...; } is equivalent to {r forbid a with a = ...; }.

9.3. Pattern matching of records(top)

One can pattern match records, with basically the same syntax (except that type can not be pattern matched, and the rec keyword is clearly useless in pattern). However, the default field can be used in pattern to match the other fields. Here are the basic examples:

The following pattern match records which have exactly three fields l1, l2 and l3:

Pseudo code
  match r with {l1 = l1; l2 = l2; l3 = l3; } -> ...

or using the val keyword:

Pseudo code
  match r with {val l1 = l1   val l2 = l2   val l3 = l3; } -> ...

Because this looks a bit heavy, PML provides a shortcut when writing val l = l:

Pseudo code
  match r with {l1; l2; l3; } -> ...

If you want to match a record whose fields are among l1, l2 and l3, just add ... at the end of the record pattern:

Pseudo code
  match r with {l1; l2; l3; ...} -> ...

To mtch the rest of the record, use the following syntax:

Pseudo code
  match r with {other with l1; l2; l3} -> ...

or

Pseudo code
  match r with {other | l1; l2; l3} -> ...

Here other will be bind to a record containing all the fields of r but l1, l2 and l3.

When matching the default field using a variant pattern, you may want to use or not the ... at the end of the record pattern:

Pseudo code
  match r with {A[] | l1; l2; l3} -> ...

matches records whose default field is A[] and with exactly l1, l2 and l3 as other field while

Pseudo code
  match r with {A[_] | l1; l2; l3; ...} -> ...

matched records whose default field is A[_] and wich have at least the fields l1, l2 and l3.

9.4. Inlined definitions and specifications(top)

Pseudo code
  { 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:

Pseudo code
  { val x as toto  (* x est le nom du champ, mais on l'appelle toto
                      dans la suite du record *)

Exemple:

Pseudo code
  {
    val x as y = ... ,
    val f = ... y ...
  }.x

9.5. Les tableaux (à venir)(top)

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

même contrainte que pour « =: »

9.6. Héritage multiple(top)

Pseudo code
  { 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:

10. Dealing with errors(top)

10.1. Basic notions(top)

PML provides two distincts mechanisms to deal with errors:

The difference between the two is that while errors will always exit the program, exceptions can be caught, inspected and acted upon, either to exit the program or to try to correct something.

Explicitly provoking an error / exception is easy:

Pseudo code
val my_function args =
  ...
  raise exc    (* exception *)
  ...
  error er     (* error *)

Both errors and exceptions are special cases of values, and they explicitly appear in function types. The type of a function is specified by four types:

  1. the type of the argument,
  2. the type of the return value (neither exceptional nor erroneous),
  3. the type of the possible exceptions,
  4. the type of the possible errors.

A typical type of a function thus looks like

Pseudo code
val rec f : (list int -> int | [Invalid_Argument[]] | [Loop[]]) x = ...

Exceptions and/or errors can be empty:

Pseudo code
val rec f : (list int -> int | [Invalid_Argument[]] | []) x = ...

and PML defines A => B as a synonym for A -> B | [] | [], that is, a function which raises no exception and no error.

Similarly, A -> B is a synonym for A -> B | ? | ?, that is, a function that can raise any error and any exception.

10.2. Authorized errors /exceptions(top)

In the default configuration, neither errors nor exceptions are authorized at the "file" level:

Incorrect pml code (with error message)
val pb = raise (undef[])
Pml output
Type error at /tmp/tmpS2V5y2.pml: line 2 column 0 to column 0: 
---
variants "+undef" at line 1 column 16 to column 23
  used as 
empty variants at line 2 column 0 to column 0

Trying to "compile" or open this file will fail.

Note that this is only true of exceptions / errors that are actually evaluated. The following is accepted because the function is already in evaluated form.

Correct pml code (with result)
val f x = raise (undef[])
Pml output

However, the user can give a set of authorized exceptions and errors in a given file by putting #authorized_exception ... and / or #authorized_error ... at the very top of the file. What follows #authorized_exception is a list of constructor names (without the brackets) separated by spaces. The following file is thus a correct pml file:

Correct pml code (with result)
#authorised_exception undef Other_constructor
val test1 = A[]
val pb = raise undef[]
val test2 = B[]
Pml output
/tmp/tmpx4JERm.pml: line 4 column 12 to column 15
Exception: undef[]

"Compiling" this will succeed, but actually evaluating it, or opening it inside another file may fail if the exception undef[] is not caught. Calling pml on this file will provoque a warning as the last line is never reached: "Warning: dead code ...".

Not that since files are just like structures, neither test1 nor test2 are defined after reading this file.

The way this is typically used is when some value is defined using a function in another file:

#authorised_exception Not_found

open list
...
val environment = ...

val name = assoc eq_string "NAME" environment

10.3. Catching exceptions(top)

Just like Caml, pml has a try ... with ... mechanism to allow inspection of exceptions. Exceptions are propagated "up" until they meet a try ... with ... or they reach top-level.

A typical example is

Correct pml code
open unary_nat
val sub_trunc n m =
  (* compute the truncated substraction n-m *)
  try
    sub n m
  with
    Undef[] -> 0

PML allows another construction: let try ... in ... with ... not readily available in Caml. It is used like

Pseudo code
val f x =
  ...
  let try a = exp1
  in exp2
  with
      A[] -> ...
    | B[] -> ...

and the semantics is that only exceptions raised inside exp1 are handled by the with. Exceptions raised inside exp2 are propagated normally.

This construction has the same syntax as normal let ... in and thus allows simultaneaus local definitions to have the same handler:

Correct pml code (with result)
open unary_nat
val f a b =
  let try
    a' = pred(a)
  and
    b' = pred(b)
  in a'+b'
  with Undef[] -> 0
val test0 = f 0 0
val test1 = f 0 2
val test2 = f 2 0
val test3 = f 2 2
Pml output
  val test0 = Z[]
  val test1 = Z[]
  val test2 = Z[]
  val test3 = S[S[Z[]]]
}

Note: in fact, the primitive construction is let try .... The "usual" try ... with ... is just syntactic sugar for let try v = ... in v with ....

Non guarded exceptions / errors(top)

As opposed to Caml, any value can be raised. Thus, both raise {} and error (fun x->x) are valid PML. However, it is probably a very good idea to guard your exceptions and errors with specific constructors to avoid problems.

The only case when unguarded exception can be useful is when they are used as a local way of controlling flow of execution:

Correct pml code (with result)
open binary_nat
val rec mult = fun
    [] -> 1
  | a::l -> if (a=0) then raise 0
                     else a * (mult l)
val compute f e =
  try f e
  with v -> v

val test1 = compute mult [1;2;3;4;0;1;2;3;4]
val test2 = compute mult [1;2;3;4;5]
Pml output
  val mult = fun ...
  val test1 = End[]
  val test2 = Zero[Zero[Zero[One[One[One[One[End[]]]]]]]]
}

11. La suite(top)

TODO: