From mboxrd@z Thu Jan  1 00:00:00 1970
Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105])
	by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p8RNx1sR005445
	for <caml-list@sympa-roc.inria.fr>; Wed, 28 Sep 2011 01:59:01 +0200
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: ArQBAE1igk7RVdU2kGdsb2JhbABBhGWjFQgUAQEBAQkJDQcUBCKBUwEBAQECARICDwQZATgBAwELAQUFGgImAgI0AQUBHAY1h1acQwqLCIMghQ6JKQIEBoEmhE4xYASHcItihSKBKoY+PYFIgjQ
X-IronPort-AV: E=Sophos;i="4.68,452,1312149600"; 
   d="scan'208";a="110875583"
Received: from mail-yw0-f54.google.com ([209.85.213.54])
  by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 28 Sep 2011 01:58:57 +0200
Received: by ywp17 with SMTP id 17so9157081ywp.27
        for <caml-list@inria.fr>; Tue, 27 Sep 2011 16:58:56 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=gmail.com; s=gamma;
        h=sender:subject:mime-version:content-type:from:in-reply-to:date:cc
         :content-transfer-encoding:message-id:references:to:x-mailer;
        bh=TX9KTmuO7G3es2PTTbNNlMZck/YbF0RETqrhxro7s7s=;
        b=wxhusrNzm0fU8+v5MP5ueUKwlBqoaK2fkXMPGWR3XMQfmV9BzKj5xszY/MIN1MHSK7
         rNTDJN6tR8XfhRFOvmTPzS3vpJZ8athysP7+xM8h2kAiMfOYHV3bHp+Iu6NSLgIU4IpS
         8GoAORtMs6tX3+WkVTHTi+oOlPQF7M4oz/Nxg=
Received: by 10.68.0.167 with SMTP id 7mr27131024pbf.106.1317167936520;
        Tue, 27 Sep 2011 16:58:56 -0700 (PDT)
Received: from [10.6.63.137] ([118.103.30.26])
        by mx.google.com with ESMTPS id 4sm1565340pbk.5.2011.09.27.16.58.47
        (version=TLSv1/SSLv3 cipher=OTHER);
        Tue, 27 Sep 2011 16:58:55 -0700 (PDT)
Sender: Jacques Garrigue <jacques.garrigue@gmail.com>
Mime-Version: 1.0 (Apple Message framework v1084)
Content-Type: text/plain; charset=utf-8
From: Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>
In-Reply-To: <alpine.LFD.2.00.1109272159470.2778@surtur.dico.unimi.it>
Date: Wed, 28 Sep 2011 08:58:36 +0900
Cc: OCaML Mailing List <caml-list@inria.fr>
Message-Id: <6C6F75D3-BE10-47A6-90D9-65AEE678A9B3@math.nagoya-u.ac.jp>
References: <alpine.LFD.2.00.1109271335550.8918@surtur.dico.unimi.it> <6A020199-D53D-443E-9683-D225D495AEB5@math.nagoya-u.ac.jp> <alpine.LFD.2.00.1109271554420.8918@surtur.dico.unimi.it> <091F94EF-9F08-41E2-8AD7-415548045A72@free.fr> <alpine.LFD.2.00.1109272159470.2778@surtur.dico.unimi.it>
To: Walter Cazzola <cazzola@dico.unimi.it>
X-Mailer: Apple Mail (2.1084)
Content-Transfer-Encoding: 8bit
X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id p8RNx1sR005445
Subject: Re: [Caml-list] still silly issues on polymorphic types

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