Re: [Caml-list] still silly issues on polymorphic types

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

On 2011/09/28, at 5:22, Walter Cazzola wrote:

> I still have one problem: how can I assign to a the type 'a list? by
> using «type a= 'a list» I get
> 
> Error: Unbound type parameter 'a

Same thing: you need to make explicit the contents of the list.
So this can be type a = int list.
On the other hand if you are trying to refine the signature, you
can also write
 type t
 type a = t list
keeping t abstract.

But maybe I should first make clearer what instantiation and inclusion
mean, because this is often confusing.

For type schemes (types containing type variables), the more general
type can be used in more contexts, so it is actually a subtype, and you have

  'a -> 'b  <=  int -> 'b  < = int -> bool

I.e., by instantiating a variable you can go to a less general type,
which you can view as a super-type.

For abstract types in signatures, this works the other way round:

 sig type a = int end  <=  sig type a end

This is because an abstract type denotes existential abstraction, rather
than the universal quantification of type variables in type schemes.
So for signatures, instantiating a type declaration creates a subtype.

They still have in common that instantiation substitutes all occurrences
of a name simultaneously.

Hope this helps.

	Jacques