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 p7EDtsfI031859 for ; Sun, 14 Aug 2011 15:55:54 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ao4CABTTR07RVdy2mGdsb2JhbABBhzKRCIczAYchYQgUAQEBAQEICQ0HFCWBQAEBAQECARICExkBGxILAQMBCwYFBAcaISEBAREBBQEKEgYTCAoQh04ElTcKjDaCVYNLO4htAgMGhkEEglGQQYl2gmM8g2I X-IronPort-AV: E=Sophos;i="4.67,369,1309730400"; d="scan'208";a="115817291" Received: from mail-vx0-f182.google.com ([209.85.220.182]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 14 Aug 2011 15:55:49 +0200 Received: by vxh11 with SMTP id 11so6324355vxh.27 for ; Sun, 14 Aug 2011 06:55:48 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; bh=RBnfoCNAANjj2Ot7Y3txtoOjTtX5VCFOyTZ9jZ3RNVY=; b=DgsgXMj7JavxUG2efZpD3Bh1g7rcrlInoGHQWJgux9FhiHwDma1PJVRDLMPzX3SQ2v G2dtk+N46e792s8Ti5nUhuYYS6IxcJZ+mtksepbxQUnO/B/KeKUsdj0PRXkYMyVpdcj8 ZsF4uUtBv17MIQoPXZqlaUSkV2mXSi6NBlkZw= Received: by 10.52.100.6 with SMTP id eu6mr2553766vdb.30.1313330148104; Sun, 14 Aug 2011 06:55:48 -0700 (PDT) MIME-Version: 1.0 Received: by 10.52.157.41 with HTTP; Sun, 14 Aug 2011 06:55:28 -0700 (PDT) In-Reply-To: <1F991690-DC08-4BF6-BB41-6B9402C043FC@gmail.com> References: <1F991690-DC08-4BF6-BB41-6B9402C043FC@gmail.com> From: Gabriel Scherer Date: Sun, 14 Aug 2011 15:55:28 +0200 Message-ID: To: Ruslan Ledesma Garza Cc: OCaml List Content-Type: multipart/alternative; boundary=20cf3071c6bcf3587404aa7780d8 Subject: Re: [Caml-list] Type generalization problem --20cf3071c6bcf3587404aa7780d8 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable You have hit the "value restriction": http://caml.inria.fr/resources/doc/faq/core.en.html#eta-expansion # let g =3D (fun x -> x) (fun x -> x);; val g : '_a -> '_a =3D # let g x =3D (fun x -> x) (fun x -> x) x;; val g : 'a -> 'a =3D Polymorphism annotation ( : 'a . 'a -> 'a ) have no use here, as you can easily see in the return type if the value is polymorphic (type variables 'a, implicitly quantified at the beginning of the type) or not ("weak" type variable '_a, which are just unknowns waiting to be unified). On Sun, Aug 14, 2011 at 3:46 PM, Ruslan Ledesma Garza < ruslanledesmagarza@gmail.com> wrote: > Dear list, > > Consider the following OCaml session. > > Objective Caml version 3.12.0 > > # let f : 'v . 'v -> 'v =3D fun x -> x;; > val f : 'a -> 'a =3D > # let g : 'v . 'v -> 'v =3D (fun x -> x) (fun x -> x);; > Error: This definition has type 'a -> 'a which is less general than > 'b. 'b -> 'b > # > > Why doesn't OCaml generalize the type 'a -> 'a? According to the typing > rules in "Principal type-schemes for functional programs" ( > http://portal.acm.org/citation.cfm?id=3D582176 ), the type 'a -> 'a can be > generalized. > > Something similar happens in the following OCaml session. > > Objective Caml version 3.12.0 > > # let f : 'v . 'v -> 'v =3D fun x -> x;; > val f : 'a -> 'a =3D > # let h =3D f f;; > val h : '_a -> '_a =3D > # h 1;; > - : int =3D 1 > # h h;; > Error: This expression has type int -> int > but an expression was expected of type int > # > > I want the type of h to be \forall 'a . 'a -> 'a. :'( > > Best regards, > Rusl=E1n. > > > > > -- > Caml-list mailing list. Subscription management and archives: > https://sympa-roc.inria.fr/wws/info/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs > > --20cf3071c6bcf3587404aa7780d8 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable You have hit the "value restriction":
=A0 http://caml.inria= .fr/resources/doc/faq/core.en.html#eta-expansion

# let g =3D (fu= n x -> x) (fun x -> x);;
val g : '_a -> '_a =3D <fun>
# let g x =3D (fun x ->= x) (fun x -> x) x;;
val g : 'a -> 'a =3D <fun>
<= br>Polymorphism annotation ( : 'a . 'a -> 'a ) have no use h= ere, as you can easily see in the return type if the value is polymorphic (= type variables 'a, implicitly quantified at the beginning of the type) = or not ("weak" type variable '_a, which are just unknowns wai= ting to be unified).

On Sun, Aug 14, 2011 at 3:46 PM, Ruslan Lede= sma Garza <ruslanledesmagarza@gmail.com> wrote:
Dear list,

Consider the following OCaml session.

=A0 =A0 =A0 =A0Objective Caml version 3.12.0

# let f : 'v . 'v -> 'v =3D fun x -> x;;
val f : 'a -> 'a =3D <fun>
# let g : 'v . 'v -> 'v =3D (fun x -> x) (fun x -> x);= ;
Error: This definition has type 'a -> 'a which is less general t= han
=A0 =A0 =A0 =A0 'b. 'b -> 'b
#

Why doesn't OCaml generalize the type 'a -> 'a? According to= the typing rules in "Principal type-schemes for functional programs&q= uot; ( http://portal.acm.org/citation.cfm?id=3D582176 ), the type = 9;a -> 'a can be generalized.

Something similar happens in the following OCaml session.

=A0 =A0 =A0 =A0Objective Caml version 3.12.0

# let f : 'v . 'v -> 'v =3D fun x -> x;;
val f : 'a -> 'a =3D <fun>
# let h =3D f f;;
val h : '_a -> '_a =3D <fun>
# h 1;;
- : int =3D 1
# h h;;
Error: This expression has type int -> int
=A0 =A0 =A0 but an expression was expected of type int
#

I want the type of h to be \forall 'a . 'a -> 'a. =A0 =A0 = =A0 =A0 :'(

Best regards,
Rusl=E1n.




--
Caml-list mailing list. =A0Subscription management and archives:
https://sympa-roc.inria.fr/wws/info/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs


--20cf3071c6bcf3587404aa7780d8--