Re: [Caml-list] polymorphic variants in match statements

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

On 2012/02/11, at 7:20, Milan Stanojević wrote:

> A small follow-up question
> 
> Polymorphic variant types are not allowed to have non-regular
> recursion, i.e. the following type definition gives an error
> 
> type 'a t = [ `A of 'a | `B of ('a * 'a) t ]
> 
> Error: In the definition of t, type ('a * 'a) t should be 'a t
> 
> I guess the reason why this is not allowed has something to do with
> our previous discussion, but I'm struggling to connect the dots.
> 
> Can you please explain this restriction?

Actually, this is not directly related.
The problem here is with type inference of recursive types.
To do that, we need to do type inference on (possibly infinite) recursive trees.
This is easy for regular trees (which can be represent as a directed graph),
as the usual algorithm for first-order unification works.
So what ocaml does is building such a regular tree on the fly, by creating a
back edge to a previous ['a t] node when it meets another ['b t] node below it.

So for instance, with definition
  type 'a t = [ `A of 'a | `B of 'a t ]

the type [int t] would expand to ([`A of int | `B of 'r] as 'r)

However, for this to work, any occurrence of t inside its own definition
should have identical parameters. Hence the enforced restriction.

	Jacques Garrigue