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 p7E9l1eh027248
	for <caml-list@sympa-roc.inria.fr>; Sun, 14 Aug 2011 11:47:01 +0200
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: Ap8DAH+YR07RVdKwmGdsb2JhbABBmG+DXYskCBQBAQEBAQgJDQcUJYFAAQEBAQIBEgITEwYBOAEDAQsBBQU0EjQBBQEcGSKHTpY5Co8Lgz6JKAIDBoViXwSHXYs1hjSGJTyBP4Iw
X-IronPort-AV: E=Sophos;i="4.67,369,1309730400"; 
   d="scan'208";a="115805680"
Received: from mail-iy0-f176.google.com ([209.85.210.176])
  by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 14 Aug 2011 11:46:55 +0200
Received: by iyn35 with SMTP id 35so5483739iyn.35
        for <caml-list@inria.fr>; Sun, 14 Aug 2011 02:46:54 -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=NSqCI2Ki4XyKUlKCFabGyv9OmojDhx+sEqlIb6I0ND0=;
        b=EPPjibBuYj5BwAgjqCJGbirYdz3M7DAXPEK/bGUEAoC3O/fCAkoFuIKj4xA51jr5rB
         bpsyiRr6ITQ0D/hgn91Ux2fPQPnMYCGTOrNBVPCRIjVYAQ/ZalD4xJ8qf4rmj3QrohIa
         Z0R/m0MY8UzvhYWNu5KJDjtNIVAf0171Bf4Og=
Received: by 10.42.130.68 with SMTP id u4mr2948890ics.464.1313315214005;
        Sun, 14 Aug 2011 02:46:54 -0700 (PDT)
Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157])
        by mx.google.com with ESMTPS id q4sm3161437ibb.32.2011.08.14.02.46.51
        (version=TLSv1/SSLv3 cipher=OTHER);
        Sun, 14 Aug 2011 02:46:52 -0700 (PDT)
Sender: Jacques Garrigue <jacques.garrigue@gmail.com>
Mime-Version: 1.0 (Apple Message framework v1084)
Content-Type: text/plain; charset=us-ascii
From: Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>
In-Reply-To: <20110806125021.GB10154@ombreroze.happyleptic.org>
Date: Sun, 14 Aug 2011 18:46:50 +0900
Cc: caml-list@inria.fr
Message-Id: <BEFA87A9-C4D3-4235-B7A6-D4F8CBE2E0B1@math.nagoya-u.ac.jp>
References: <20110806125021.GB10154@ombreroze.happyleptic.org>
To: rixed@happyleptic.org
X-Mailer: Apple Mail (2.1084)
Content-Transfer-Encoding: 8bit
X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id p7E9l1eh027248
Subject: Re: [Caml-list] typer strangeness (3.12.0)

On 2011/08/06, at 21:50, rixed@happyleptic.org wrote:

> Given these types:
> 
> (* A parser is given a list of items and returns either a Failure indication, a
>   Wait for more inputs indication, or a result (composed of a new value and the list
>   of tokens that were unused) *)
> type ('a, 'b) parzer_result = Wait | Res of ('a * 'b list) | Fail
> type ('a, 'b) parzer = 'b list -> ('a, 'b) parzer_result
> 
> And this function used to pipe two parsers together:
> 
> (* Use the results of the first parser as the input elements of the second.
>   Stop as soon as p2 returns a result or fails.
>   Notice that if p1 is a ('a, 'b) parzer and p2 a ('c, 'a) parzer
>   then pipe p1 p2 is a ('c, 'b) parzer, which comes handy but p2 is then
>   forced to consume everything ! *)
> let (pipe : ('a, 'b) parzer -> ('c, 'a) parzer -> ('c, 'b) parzer) p1 p2 =
>    let p1_rem = ref [] in
>    fun bs -> match p1 (!p1_rem @ bs) with
>        | Fail -> Fail
>        | Wait -> Wait
>        | Res (res, rem) ->
>            p1_rem := rem ;
>            (match p2 [res] with
>                | Res (res', rem') ->
>                    if rem' <> [] then Printf.printf "WRN: second end of a pipe did not consume eveything !\n" ;
>                    Res (res', !p1_rem)
>                | Fail -> Fail | Wait -> Wait)
> 
> This pipe function has the expected type :
> 
> # pipe;;
> - : ('a, 'b) parzer -> ('c, 'a) parzer -> ('c, 'b) parzer = <fun>
> 
> Now, if I change it's last line for : "| x -> x)", ie not repeating Wait and Fail, the result is
> very different :
> 
> # pipe;;
> - : ('a, 'a) parzer -> ('b, 'a) parzer -> ('b, 'a) parzer = <fun>
> 
> How come?

If you write "x -> x", the output of p1 is forced to be the same type as the output of the function,
which forces the unification of 'a and 'b. Note that this second type is equivalent to
> - : ('a, 'a) parzer -> ('c, 'a) parzer -> ('c, 'a) parzer = <fun>

If you explicitly write "Fail -> Fail | Wait -> Wait", no such unification happens, and you get
the intended type.
You can get the same behaviour by writing "Fail | Wait as x -> x", i.e. the type checker is clever
enough to not unify the pattern type and the variable type.

> And why didn't the compiler complain since I explicitely typed the function definition?


You already got your answer. A simple type annotation does not enforce polymorphism.

Hope this helps,

	Jacques