Phil Wadler wrote:
> Mark suggests that Mu types might be better that recursive type
> synonyms. I think of them as pretty much equivalent, and it's
> simply a question of whether one makes the `mu' syntax accessible
> to the user. One certainly needs `mu' or an equivalent internally
> for doing the typechecking. The advantage of the way I put it
> is that it makes for a minimal change from the current language:
> just get rid of one restriction. -- P
They are not quite equivalent:
The difference between mu-types and recursive type synonyms is the
difference between decidable and undecidable type inference.
The problem is that type synonyms are parametric and one could write
type synonyms in which the recursive occurrence of the type identifier
is used with a non-type-variable argument, e.g.
type Rec a = Rec (a->a)
Type synonyms like this are not expressible with mu-types.
Stefan Kahrs
