# Examples

## PML is like ML

Here is the factorial function that should look familiar to most ML programmer and be readable by newcomers:

Here is the quick sort algorithm (the partition function split a list in two parts according to the given predicate):

## PML is more than ML

PML is entirely based on subtyping with polymorphic variants and records, both being extensible. Records in PML can be used as first class modules or objects because they support [multiple and open inheritance]. Open inheritance means that record can be constructed from an initial object having any type (which allows one to decorate values with arbitrary fields). Like any ML, PML supports exceptions, but uncaught exception should not be possible (except the ones you explicitly allow).

This first example illustrates subtyping with polymorphic variants. It defines three types: natural numbers (nat), non zero natural numbers (nat') and integers (int) all in binary notation, with the intended subtyping and uniqueness of the representation for each number (the least significant bits comes first and End[] represents the number zero with no bit at all):

You could define the same types in OCaml using polymorphic variants ... but this is almost unusable.

The second example illustrates the use of record types and open inheritance. It defines the type of binary-tree, red-black-binary-tree, binary-search-tree and red-black-binary-search-tree with the intended subtyping. You can then reuse a lot of code for all these trees:

Finally, here is the encoding of point classes in PML using the same features. Expert will recognize Cardelli's encoding for functional objects and PML's subtyping allows for override (even at the level of types), multiple inheritance and binary methods (not all these feature are illustrated here):

## PML allows you to prove your programs

Here is just one example, showing some properties of addition using natural numbers. The 8< sign means that this branch of the proof is finished.