[Caml-list] difference between locally abstract types and polymorphic annotations?

[Caml-list] difference between locally abstract types and polymorphic annotations?

[Alexey Egorov]

[-- Attachment #1: Type: text/plain, Size: 368 bytes --]


Hello,

I'm noticed that GADT typechecking depends on whether free variables are annotated as locally abstract types (in form of "type a b c . <typeexpr>") or just polymoprhic annotations (in form of " 'a 'b 'c . <typeexpr> ").

Code here -  http://pastebin.com/36ZAjw0J  

What is the difference? I was thinking that both of this are equivalent, isn't it?

Thanks.

[-- Attachment #2: Type: text/html, Size: 781 bytes --]

Re: [Caml-list] difference between locally abstract types and polymorphic annotations?

[Jacques Garrigue]

On 2016/08/15 08:22, Alexey Egorov wrote:
> 
> Hello,
> 
> I'm noticed that GADT typechecking depends on whether free variables are annotated as locally abstract types (in form of "type a b c . <typeexpr>") or just polymoprhic annotations (in form of " 'a 'b 'c . <typeexpr> ").
> 
> Code here - http://pastebin.com/36ZAjw0J 
> 
> What is the difference? I was thinking that both of this are equivalent, isn't it?
> 
> Thanks.

They are not equivalent.
Polymorphic annotations are about checking, a posteriori, that some types are indeed polymorphic,
and also about allowing polymorphic recursion.
Locally abstract types are about creating an abstract type and using it locally. It will be turned into a type variable when you leave the scope. Only abstract types can be refined by GADT pattern matching, not type variables.
Using GADTs, you often want both refinement and polymorphic recursion, this is why “type a b c. <typeexp>” is actually a combination of the two.

Jacques