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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id B993D7FBC5 for ; Thu, 8 Jan 2015 16:21:59 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of goswin-v-b@web.de) identity=pra; client-ip=212.227.15.3; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="goswin-v-b@web.de"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of goswin-v-b@web.de designates 212.227.15.3 as permitted sender) identity=mailfrom; client-ip=212.227.15.3; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="goswin-v-b@web.de"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mout.web.de) identity=helo; client-ip=212.227.15.3; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="postmaster@mout.web.de"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ak8AAHafrlTU4w8DnGdsb2JhbABchDDLdAKBD0MBAQEBAREBAQEBAQYNCQkULoQMAQEBAwEnE0QLCxgJJQ8FDRs0iBcBAwkIBMJEHysNFYMoAQsBH41PgjEWgwCBEwWVdoFDgQ+EeQyFfoIkgzmEEW6CQwEBAQ X-IPAS-Result: Ak8AAHafrlTU4w8DnGdsb2JhbABchDDLdAKBD0MBAQEBAREBAQEBAQYNCQkULoQMAQEBAwEnE0QLCxgJJQ8FDRs0iBcBAwkIBMJEHysNFYMoAQsBH41PgjEWgwCBEwWVdoFDgQ+EeQyFfoIkgzmEEW6CQwEBAQ X-IronPort-AV: E=Sophos;i="5.07,723,1413237600"; d="scan'208";a="116208671" Received: from mout.web.de ([212.227.15.3]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 08 Jan 2015 16:21:59 +0100 Received: from frosties.localnet ([134.3.241.185]) by smtp.web.de (mrweb003) with ESMTPSA (Nemesis) id 0Md4le-1YQMLs2gmA-00IDY3 for ; Thu, 08 Jan 2015 16:21:58 +0100 Received: from mrvn by frosties.localnet with local (Exim 4.82) (envelope-from ) id 1Y9EuL-0001Ms-Nm for caml-list@inria.fr; Thu, 08 Jan 2015 16:21:57 +0100 Date: Thu, 8 Jan 2015 16:21:57 +0100 From: Goswin von Brederlow To: caml-list@inria.fr Message-ID: <20150108152157.GA4890@frosties> References: <20150107135012.GA17784@frosties> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.5.23 (2014-03-12) X-Provags-ID: V03:K0:/4GqXvdHrNBdm77CpdBbrZTFIW1HpOrdPqJoxkgh6Wsx+ExDdDM tCEp5TUK6nqYGsh/tSdVb+vPdov/c7Ox+Y7znVwABYKfEIxc/YwelqWS11edlVf99La3Sdy 8Pw4zufPRtuKd3bOmMUnC/u3Lw49S5FgfLO1qOYs6SPjOY9aWnADNZBzQwVlBAXh6fyYTbd x/qXVYzdEI6KdBt6L13RQ== X-UI-Out-Filterresults: notjunk:1; Subject: Re: [Caml-list] Problem with universal functions in a module On Thu, Jan 08, 2015 at 09:45:47AM +0000, Ben Millwood wrote: > Parametric polymorphic values in OCaml's type system can be thought of as > "choose an assignment of the variables in this type, and you can use this > value with that monomorphic type". But there's no monomorphic type that > lets 'helper' do the right thing, so you actually need something more > expressive than ordinary polymorphic types. > > In Haskell there's higher-rank polymorphism, which in this case would look > something like 'helper :: (forall a. T a -> b) -> Helper b', so that you > could only pass sufficiently-polymorphic arguments to helper. However, as > Jeremy said, there's a lot of added complexity involved. In ocaml that is 'a . 'a -> 'b, or for GADTS: type a . a -> 'b. The problem is the former is only allowed in records and objects, not for function arguments and the later is only for annotating code and not for signatures. I don't see how there can be much added complexity involved. The higher-rank polymorphism is already allowed in records and objects so the type system knows how to deal with them. At least when they are annotated. I wouldn't need ocaml to infere those types. > On 7 January 2015 at 17:26, Jeremy Yallop wrote: > > > On 7 January 2015 at 13:50, Goswin von Brederlow > > wrote: > > > Why are function arguments less general than their original function? > > > > Polymorphic arguments complicate type checking and make type inference > > impossible, so OCaml doesn't allow them. > > > > > B) is there some way around this I'm not seeing? > > > > I don't think that there's any way of passing polymorphic arguments > > that works out simpler than using a record. > > > > Of course, in your simple example code it's possible to eliminate the > > GADT altogether, which would also eliminate the need for polymorphic > > arguments. Perhaps GADTs play a more essential role in your real > > code, though. The real use case has a GADT as input for a functor. The functor defines the boxing, an equality and unbox_with_equal operation and that helper record. Actually I have a few flavours of the same for different input types: type 'a t, type ('a, 'b) t and GADTs with detached witness: type 'a key + type 'a value and so on. I wish I could make a generic helper record with type ('b, 'c) helper = { fn : 'a 'b -> 'c } *sigh* MfG Goswin