From mboxrd@z Thu Jan  1 00:00:00 1970
Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82])
	by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p8RDnX7n018429
	for <caml-list@sympa-roc.inria.fr>; Tue, 27 Sep 2011 15:49:33 +0200
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AjkBAAXUgU6flYLKmWdsb2JhbABBp3wUAQEBAQEICwsHFCaBUwEBBAEnEQI4BwULC0ZXBogLuHaHCwSTUoUQjCY
X-IronPort-AV: E=Sophos;i="4.68,449,1312149600"; 
   d="scan'208";a="121721106"
Received: from smtp.dico.unimi.it ([159.149.130.202])
  by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 27 Sep 2011 15:49:31 +0200
Received: from surtur.docenti.dico.unimi.it (surtur.docenti.dico.unimi.it [159.149.152.56])
	(authenticated bits=0)
	by smtp.dico.unimi.it (8.14.4/8.14.4) with ESMTP id p8RDnP0u019046
	(version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO);
	Tue, 27 Sep 2011 15:49:25 +0200
Date: Tue, 27 Sep 2011 15:49:25 +0200 (CEST)
From: Walter Cazzola <cazzola@dico.unimi.it>
To: Christophe Papazian <christophe.papazian@gmail.com>
cc: OCaML Mailing List <caml-list@inria.fr>
In-Reply-To: <E923C544-C166-46CC-B02B-B36CFBE79E39@gmail.com>
Message-ID: <alpine.LFD.2.00.1109271546540.8918@surtur.dico.unimi.it>
References: <alpine.LFD.2.00.1109271335550.8918@surtur.dico.unimi.it> <E923C544-C166-46CC-B02B-B36CFBE79E39@gmail.com>
User-Agent: Alpine 2.00 (LFD 1167 2008-08-23)
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
X-Greylist: Sender succeeded SMTP AUTH, not delayed by milter-greylist-4.0 (smtp.dico.unimi.it [159.149.130.202]); Tue, 27 Sep 2011 15:49:25 +0200 (CEST)
X-DSI-MailScanner-Information: Please contact the staff for more information
X-DSI-MailScanner-ID: p8RDnP0u019046
X-DSI-MailScanner: Found to be clean
X-DSI-MailScanner-From: cazzola@dico.unimi.it
Subject: Re: [Caml-list] still silly issues on polymorphic types

On Tue, 27 Sep 2011, Christophe Papazian wrote:

> Please remember how types can be subtypes of other types :
>
> consider
>
> val f : int -> int
> val g : int -> 'a
> val h : 'a -> int
> val i : 'a -> 'b
>
> then the most general type is the type of g
> and most specific type is type of h. In fact we have a diamond relation 
> between types :
>
> h<f<g
> h<i<g
> and i and f are not related.
>
> Why ?
>
> because if you need a function of type like f (int -> int)
> you can give h (if h can eat anything, it can eat int), but not g
> (i don't now how to handle 'a if I only need a int).
>
> So int is a subtype of 'a,
> but int -> int is not a subtype of 'a -> 'b,
> and 'a -> 'a is a valid subtype of int-> int.

uhm, I have a couple of questions I don't understand on your
explanation:
  - why the most general type is int->'a and not 'a -> 'b?
  - does this mean that I can't have a general type that could be matched
    by 'a -> 'a list -> 'a list  and int -> int -> int ?

Walter

--