This file has been processed with:
| ocamlorn --library stdlib.mli \ --library implicit_polymorphism.in.ml --input implicit_polymorphism.in.ml --lifting implicit_polymorphism.lif.ml \ > implicit_polymorphism.out.ml |
| type nat = | Z | S of nat |
In a previous example, we have seen this ornament :
| type ornament natunit : nat => () with | Z => () | S _ => ~ |
But what are the types of the injection and projection functions of this ornament? In particular, we are going to look at the skeleton type of nat in those types. (The type of both functions being composed of the skeleton type and the patch type, which is not relevant here and tedious to write.)
Let us recall that the skeleton of nat is:
| type 'a nat_skel = Z_skel | S_skel of 'a |
It could be nat nat_skel, but this does not work. Let us take the same example as before:
| let rec add m n = match m with | Z -> n | S m' -> S(add m' n) |
whose generic term is
| let _add = lifting add |
| let rec _add m n = match (orn-match #5) m #6 with | Z_skel -> n | S_skel m' -> (orn-cons #2) (S_skel (_add m' n)) #3 |
Then if the skeleton is nat nat_skel, m’ is nat and so is m, which is not.
Indeed, the skeleton type should be natunit nat_skel. So, this could be specified with:
| type ornament natunit : nat => () with | Z => () | S n => ~ when n: natunit |
However, for this ornament, projection and injection functions may be best typed with a polymorphic type, i.e. with the skeleton ’a nat_skel. Indeed, any value can be in the wildcards of the left pattern as we do not use it. As a conquence, when a function is lifted, this type variable can be instantiated with any type, including an ornament type.
By default, any wildcards on the left may (or may not, if some other clause constraints the type) result in a polymorphic variables.