From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 3DC847FA8B for ; Sun, 22 Mar 2015 15:30:08 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.223.174; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.223.174 as permitted sender) identity=mailfrom; client-ip=209.85.223.174; receiver=mail2-smtp-roc.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 (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-ie0-f174.google.com) identity=helo; client-ip=209.85.223.174; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-ie0-f174.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0DkAADT0A5Vm67fVdFcg1haBIMMs02QBwqFdQKBFAdMAQEBAQEBEQEBAQEBBgsLCRQuhBQBAQEDAQECDxEdARsSCwEDAQsGBQsDCgICCR0CAiIBEQEFAQoSBhMSCAiHeAEDCQgNoyA+MYsxgWuCd449ChknAwpUhGwBAQEBAQUBAQEBAQEWAQUOgROKAIR1B4JogUUFhQsKjymFf4FVkQsSI4EMCYQRPTGCQwEBAQ X-IPAS-Result: A0DkAADT0A5Vm67fVdFcg1haBIMMs02QBwqFdQKBFAdMAQEBAQEBEQEBAQEBBgsLCRQuhBQBAQEDAQECDxEdARsSCwEDAQsGBQsDCgICCR0CAiIBEQEFAQoSBhMSCAiHeAEDCQgNoyA+MYsxgWuCd449ChknAwpUhGwBAQEBAQUBAQEBAQEWAQUOgROKAIR1B4JogUUFhQsKjymFf4FVkQsSI4EMCYQRPTGCQwEBAQ X-IronPort-AV: E=Sophos;i="5.11,446,1422918000"; d="scan'208";a="127923547" Received: from mail-ie0-f174.google.com ([209.85.223.174]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 22 Mar 2015 15:30:07 +0100 Received: by iedfl3 with SMTP id fl3so23054010ied.1 for ; Sun, 22 Mar 2015 07:30: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; bh=yBCGDu0GVG9BecLJYTT3YXU5Shu+fIlvrey81faNGog=; b=zt55QLRsQnM9/h2Oqzs5VWM7jjowpuqQvD/4tXXIn38Hqtq96gsf0McYYiFsMyxCR9 dMoGwf/fTsT1obpC+gpK/T2C/2JZ7oIqTdbNor+W809EP8TLUzUfI9mEZZCISZ3FgjOS FeEkIi7LTr+3FpCZLg4uasKTi0FtMrqJCki6aMhOJKRnu+GX1ibNl43HAGRWicuYWjk9 iv7+PuxtmxWk1mB3Qc8FQpFbCwZwDPJ6nHbQr6SCeHp+7WH9tAsDA8dtmfchNU713lc9 yBYXNIJK1n792X4EQvU0WBO4t8Bo4KsV84bGLU/5qIBeEajQGWxx2kay7vj8MMdtAElk z4qQ== X-Received: by 10.107.164.140 with SMTP id d12mr114346231ioj.13.1427034606430; Sun, 22 Mar 2015 07:30:06 -0700 (PDT) MIME-Version: 1.0 Received: by 10.36.53.69 with HTTP; Sun, 22 Mar 2015 07:29:26 -0700 (PDT) In-Reply-To: References: <002a01d0632b$13cb79b0$3b626d10$@metastack.com> From: Gabriel Scherer Date: Sun, 22 Mar 2015 15:29:26 +0100 Message-ID: To: David Allsopp Cc: OCaml List Content-Type: text/plain; charset=UTF-8 Subject: Re: [Caml-list] More existential escapes (or possibly first class polymorphism) > Is there an unsoundness reason why there isn't a type annotation which can allow it be specified, > rather than inferred, that a function argument is polymorphic? > Or is that the "purity" of wanting the type system of the core language to be inferable? The latter: inferrible potentially-polymorphic arguments without requiring any kind of annotation is undecidable. Various systems exist which require you to add some annotations in some places, but it's rather delicate to know where annotations are necessary, and which kind of principality properties you can expect from the inference process. In OCaml, you have to annotate each polymorphic use of a function parameter (not the abstraction site itself), and that is done by the explicit projection with a field name having polymorphic type. On Sun, Mar 22, 2015 at 12:20 PM, David Allsopp wrote: > Jeremy Yallop wrote: >> On 20 March 2015 at 16:29, David Allsopp wrote: >> > Is there some other wizardry on offer which can allow the polymorphic >> > nature of [f] to be inferred? >> >> Unfortunately not. OCaml doesn't infer polymorphic types for function >> parameters. > > Thanks - it's useful to know to stop looking :o) > > Is there an unsoundness reason why there isn't a type annotation which can allow it be specified, rather than inferred, that a function argument is polymorphic? Or is that the "purity" of wanting the type system of the core language to be inferable? > > > David > > -- > Caml-list mailing list. Subscription management and archives: > https://sympa.inria.fr/sympa/arc/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs