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 p7E79Pfn023860 for ; Sun, 14 Aug 2011 09:09:25 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AjMGACd0R05V2gB5gWdsb2JhbABBmHGPHQEBFiYlgUABAQQBJ1IFCwtGFCg0h3ACsnsOhjkEpAk X-IronPort-AV: E=Sophos;i="4.67,369,1309730400"; d="scan'208";a="115798715" Received: from emailfrontal2.citycable.ch ([85.218.0.121]) by mail1-smtp-roc.national.inria.fr with SMTP; 14 Aug 2011 09:09:20 +0200 X-Alinto-smtpauth-localdomain: Yes Received: from seldon (unknown [85.218.93.239]) (Authenticated sender: guillaume.yziquel@citycable.ch) by emailfrontal2.citycable.ch (Postfix) with ESMTPA id 2A22B20C188; Sun, 14 Aug 2011 09:09:14 +0200 (CEST) Received: from yziquel by seldon with local (Exim 4.72) (envelope-from ) id 1QsUns-00076W-Ad; Sun, 14 Aug 2011 09:08:12 +0200 Date: Sun, 14 Aug 2011 09:08:12 +0200 From: Guillaume Yziquel To: rixed@happyleptic.org Cc: caml-list@inria.fr Message-ID: <20110814070811.GT4235@localhost> References: <20110806125021.GB10154@ombreroze.happyleptic.org> <4E3D3A89.90007@inria.fr> <20110814061959.GC32098@yeeloong.happyleptic.org> MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Disposition: inline In-Reply-To: <20110814061959.GC32098@yeeloong.happyleptic.org> User-Agent: Mutt/1.5.20 (2009-06-14) Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id p7E79Pfn023860 Subject: Re: [Caml-list] typer strangeness (3.12.0) Le Sunday 14 Aug 2011 à 08:19:59 (+0200), rixed@happyleptic.org a écrit : > Thank you for your answers, but you aimed too high above my > understanding :-) > > -[ Sat, Aug 06, 2011 at 02:58:49PM +0200, Fabrice Le Fessant ]---- > > The type constraint that you specified does not constraint the > > polymorphism of the type. To declare a polymorphic constraint, you must > > use (with OCaml >= 3.12.0) : > > > > let pipe : 'a 'b 'c. ('a, 'b) parzer -> ('c, 'a) parzer -> ('c, 'b) parzer = > > Never saw this notation before. I checked in the manual but beside in > the language grammar (in the definition of a poly-typexpr) I could find > more explanation. > Is it explained somewhere why this notation was required and why this: > > let pipe : ('a, 'b) parzer -> ('c, 'a) parzer -> ('c, 'b) parzer = > > is not enough? What's adding the "'a 'b 'c. " exactly ? It does explicit universal quantification on the type. So you create a monomorphic type out of that. \forall 'a. 'a -> 'a is a type for functions that can be used as int -> int, float -> float, string -> string, etc... \forall 'a. 'a -> 'a is not a polymorphic type as 'a is bound. By contrast, 'a -> 'a is polymorphic in the sense that is does depend on the 'a to form a monomorphic type. > I understand > that it forbids ocaml to consider that the various 'a (for instance) may > be differents 'a, but I don't understand why ocaml migh do that in the > first place (especially to produce a _less general_ type than the one > given) ? If it's not a bug, then what's the purpose ? Allowing universal quantification of types allows you to have a richer type system. Such as system F or ML^F. Typical issues it helps to solve are existential types or polymorphic recursion. It does more than simply force the various 'a to be distinct. It also binds them to form a monomorphic type. If you just want the types to be different, but not bound, you have the (type s) syntax to introduce types explicitely. > As for my second question, I received no answer (was: why changing the > pattern match for something that should be equivalent changes the infered > type). If you suspect this can be a bug then I can look for a simple > reproductible case. It's likely not a bug. What you did is replace | Fail -> Fail | Wait -> Wait by | x -> x. If you take into consideration the fact that Fail and Wait are constructors for a polymorphic type, what you have in the clauses and what is returned may have different types because you have not unified the type parameters of this datatype. However, when you write | x -> x, you unify x and x, and hence unify the type parameters. That likely explains what you observe. -- Guillaume Yziquel