[Caml-list] Fun with fixpoints

[John Skaller <skaller@ozemail.com.au>]

type 't t0' = [`A of 't]
type 't t1' = [`B of 't]
type 't t' = [ 't t0' | 't t1'] (* unify *)

type t0 = 't t0' as 't  (* fix *)
type t1 = 't t1' as 't  (* fix *)

type t = 't t' as 't  (* fix *)
type tt = [t0 | t1] (* unify *)

Ocaml replies with ....

type t = 'a t' as 'a
type tt = [ `A of 'a t0' as 'a | `B of 'b t1' as 'b ]


   param pair ----- fix ----> pair
     |                         |
    unify                    unify
     |                         |
     |                       coerce
     |                         |
     V                         V
    param type --- fix ----> type

This example shows how expressive polymorphic
variants really are. In particular, they can not
only union types, they can union type functors
(parameterised types).

Ocaml even knows the subtype relations:

let f(x:tt) = (x:tt:>t)
let f(x:t1):t = (x:t1:>t)
let f(x:t1):tt = (x:t1:>tt

but you have to use a double coercion to tell it.

-- 
John Max Skaller, mailto:skaller@ozemail.com.au
snail:10/1 Toxteth Rd, Glebe, NSW 2037, Australia.
voice:61-2-9660-0850


-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners