Re: [Caml-list] type abbreviation is cyclic

[Brian Hurt <bhurt@janestcapital.com>]

William W Smith wrote:

> I wonder whether this error is an example of the language being 
> defined more restrictively than required.  What is the reason that I 
> get these results?
>
> type a  = int -> one -> int and one = Unused | One of a;;
> type b = int -> b -> int
>
> type a is accepted while type b is not. (b gives "The type 
> abbreviation b is cyclic"  However, in the uses that I intended, there 
> won't be any actual difference between the two.
>
> I'd appreciate an explanation about why there is difference  between a 
> and   b.


I *think* this has to do with being able to bottom out data structures.  
I mean, consider the following two (similiar) types:

type a = int * one * int and one = Unused | One of a;;
type b = int * b * int;;

How do you specify a limited-length member of type b?  You can with a 
just by inserting Unused in the correct location.  But there's no such 
"stopping point" for b.

This makes more sense when you make the linked-list aspect more plain:

type a = int * next and next = EmptyList | Cons of a;;
type b = int * b;;

Hopefully someone more knowledgeable than I will post an actual 
type-theoretical reason this is so, but this is the pragmatic reason 
I've found.

Brian