From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by sympa.inria.fr (Postfix) with ESMTPS id 95CB37ED34 for ; Tue, 3 Jul 2012 14:43:08 +0200 (CEST) Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.160.182; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail4-smtp-sop.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.160.182 as permitted sender) identity=mailfrom; client-ip=209.85.160.182; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-gh0-f182.google.com) identity=helo; client-ip=209.85.160.182; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-gh0-f182.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AiQCAI7n8k/RVaC2kGdsb2JhbABFhVqgEpB2CCIBAQEBCQkNBxQEI4IYAQEBAwESAg8EGQEbEgsBAwELBgULDQICCRoDAgIhAQERAQUBCgERBhMSBwmHWgEDBgULnDAJA4tUT4JxhU0KGScDCleIcQEFDIEUiTJmhQiBEgOVNYESiXGDIz6EAA X-IronPort-AV: E=Sophos;i="4.77,515,1336341600"; d="scan'208";a="149490047" Received: from mail-gh0-f182.google.com ([209.85.160.182]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 03 Jul 2012 14:43:07 +0200 Received: by ghbz22 with SMTP id z22so7785658ghb.27 for ; Tue, 03 Jul 2012 05:43:06 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; bh=fYaLYTHD96Rti7k1Lh3Y94YnIFv3U8ndPBoqpMjRp00=; b=BErrc7BpB5cKP8WCDMVTgmGotMUzy2HVjEmKoDaurp2vUgL/QNtzTcMXTFrqjSL7NU k+/PAbsPW+U94EF+NKxdspWr5xu4An5fOPpSJ5LOhAxLFXxmPRQZbAz2+kBNsNhyC0Gk RThmnT1v4mpF2ODHpZaqt7wqul1KuhNu5ZeGlMsDjJxLlNCTxoEGQa0I/lomtq7hF/b9 +hBlLWZt5SMW7i6XrbatDnVlV3cpvrTiLvUNqla5jgqjgnC8Fq1I83kdpw5jxTBCxvwa /tY9zjGId2V0Hl35JUUhfuGF03p9029ogcF01Bewnx/4YDijyoKOL+KZq8/htMDAioH+ biuA== Received: by 10.50.217.137 with SMTP id oy9mr8200667igc.56.1341319386101; Tue, 03 Jul 2012 05:43:06 -0700 (PDT) MIME-Version: 1.0 Received: by 10.50.94.39 with HTTP; Tue, 3 Jul 2012 05:42:25 -0700 (PDT) In-Reply-To: <4FF2E6A9.3010807@gmail.com> References: <4FF2E319.9070004@ircam.fr> <4FF2E6A9.3010807@gmail.com> From: Gabriel Scherer Date: Tue, 3 Jul 2012 14:42:25 +0200 Message-ID: To: Jonathan Protzenko Cc: Philippe Veber , caml-list@inria.fr, jean-louis.giavitto@ircam.fr Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Subject: Re: [Caml-list] Initialization of a polymorphic field in a record > I really did think there was a way of doing that with the newer (type t) > features, so I'm hoping for someone to correct my example above :). I don't think there is. Indeed, as you remarked, the type required for `make1` to work would use higher-order polymorphism (a quantification inside the left type of an arrow), which does not exist in the Hindley-Milner (HM) type system (because it couldn't be completely inferred), and is not supported by OCaml in the general case. The only place where polymorphism can happen is on the function type as a whole (usual HM prenex polymorphism), or in record fields and object methods -- but then there is no inference. So as you suggest, `make1` have to take a structure that already has this first-class polymorphism baked in : a record or an object (which has the advantage of needing no type declaration), or possibly a first-class module (I did not check). let make1 (f : < poly : 'a . 'a -> bool >) =3D { check =3D fun x -> f#pol= y x } On Tue, Jul 3, 2012 at 2:33 PM, Jonathan Protzenko wrote: > The type you would like to assign to make1 is: > > make1: (=E2=88=80x. x =E2=86=92 bool) =E2=86=92 t > > However, as far I understand, the type-system of OCaml introduces the =E2= =88=80 > quantifier in front of the function, namely: > > make1: =E2=88=80x. (x =E2=86=92 bool) =E2=86=92 t > > This means by the time you enter your make1 function, the f function has > already lost its polymorphic type, since x has been "opened" already. > > I tried to eta-convert, but that doesn't work either: > > let make2 f =3D let g: 'b. 'b -> bool =3D fun (type t) (x: t) -> f x in {= check > =3D g };; > Error: This expression has type t but an expression was expected of type t > The type constructor t would escape its scope > > although I *did* think that would be legal. > > The only way I know of achieving that is by making make1 take a parameter= of > type t, that is, leave it up to the caller to wrap the function in a reco= rd > with type t so as to keep the polymorphic nature of the function... > > I really did think there was a way of doing that with the newer (type t) > features, so I'm hoping for someone to correct my example above :). > > Cheers, > > jonathan > > > On Tue 03 Jul 2012 02:25:36 PM CEST, Philippe Veber wrote: >> >> Hi, >> >> how about that: >> >> # type t =3D { check : 'a. 'a -> bool };; >> type t =3D { check : 'a. 'a -> bool; } >> >> # let return_true : 'a. 'a -> bool =3D fun _ -> true;; >> val return_true : 'a -> bool =3D >> >> # let make1 () =3D { check =3D return_true; };; >> val make1 : unit -> t =3D >> >> cheers, >> Philippe. >> >> >> 2012/7/3 Jean-Louis Giavitto > > >> >> >> Hello. >> >> I am trying to build a record with a polymorphic field and I am >> unable to initialize this field. The problem can be summarized as >> follow. The following definitions works well: >> >> type t =3D { check : 'a. 'a -> bool } >> >> let return_true _ =3D true >> >> let make1 () =3D { check =3D return_true; } >> >> But this definition raises an error: >> >> let make2 f =3D { check =3D f; } >> >> with the message: >> >> Error: This field value has type 'a -> bool which is less >> general than >> 'b. 'b -> bool >> >> Note that >> >> let return_false _ =3D true >> >> let make3 c =3D { check =3D if c then return_false else return_tr= ue; } >> >> is working but that >> >> let g c =3D if c then return_false else return_true >> let make4 c =3D { check =3D g c; } >> >> raises the same error message. Making explicit the argument of >> make does not helps: >> >> let make5 f =3D { check =3D f; } >> in make5 return_true >> >> (same error message). And making explicit the type of make does >> not help neither: >> >> let make6 : 'a. ('a -> bool) -> t >> =3D function f -> { check =3D f; } >> >> (same error message). >> >> >> >> Do you have an idea how I can specify a function similar to make >> to buid a record of type t? >> >> In the real life, the argument f will be the result of a >> computation and instead of a simple signature 'a -> bool, I must >> deal with a signature >> >> 'a 'b. (('b) #SomeClass as 'a) * 'b -> bool >> >> >> Thanks for your advice, >> Jean-Louis Giavitto. >> >> -- >> 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 >> >> >> > > -- > 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 >