From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 6F51D7F088 for ; Thu, 19 Nov 2015 10:10:13 +0100 (CET) IronPort-PHdr: 9a23:vNMtWRK2Qnj+MhS9MtmcpTZWNBhigK39O0sv0rFitYgVKv3xwZ3uMQTl6Ol3ixeRBMOAu68C1bCd6vqwEUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35nxibr5oseDKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46Fp34d6XK77Z6U1S6BDRHRjajhtpZ7djgTYVQaE+lcbV2wXlFIIX1mEv1nGWcLLry36v+xykA2bdZnsULY0UDKtx79sUwPlj2EBOiJvo0/Njcklo6tRuhOso1REyI7ZeoyPfK5xd6nHfN4eA3FKXstLWjZpDYa1bo9JBO0Ea7UL57LhrkcD+EPtTTKnA/nin3oV33I= Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gabriel.scherer@gmail.com; spf=Pass smtp.mailfrom=gabriel.scherer@gmail.com; spf=None smtp.helo=postmaster@mail-ig0-f180.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.213.180; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.213.180 as permitted sender) identity=mailfrom; client-ip=209.85.213.180; receiver=mail3-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 (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-ig0-f180.google.com) identity=helo; client-ip=209.85.213.180; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-ig0-f180.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0ClAADRkE1WlbTVVdFeg1o0bwatQoFPhTWIB4QNI4VsAoE7BzwQAQEBAQEBAQEQAQEBAQcLCwkfMIItgggBAQIBARIRBBkBGxICAgcBAwELBgMCCxodAgIiAREBBQEKEgYTCAoQh3YBAwoIDZEzj02BMT4xi0iBaoJ5hiMKGScDClaEBAEBAQEBBQEBAQEBAQEBFQEFDoZGhH6ENFSCbYFEBYYMDJAyhSGICoFbSZYvgiUSJIEXESeCLyOBXj00AYNVgUoBAQE X-IPAS-Result: A0ClAADRkE1WlbTVVdFeg1o0bwatQoFPhTWIB4QNI4VsAoE7BzwQAQEBAQEBAQEQAQEBAQcLCwkfMIItgggBAQIBARIRBBkBGxICAgcBAwELBgMCCxodAgIiAREBBQEKEgYTCAoQh3YBAwoIDZEzj02BMT4xi0iBaoJ5hiMKGScDClaEBAEBAQEBBQEBAQEBAQEBFQEFDoZGhH6ENFSCbYFEBYYMDJAyhSGICoFbSZYvgiUSJIEXESeCLyOBXj00AYNVgUoBAQE X-IronPort-AV: E=Sophos;i="5.20,317,1444687200"; d="scan'208";a="154365359" Received: from mail-ig0-f180.google.com ([209.85.213.180]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 19 Nov 2015 10:10:12 +0100 Received: by igl9 with SMTP id 9so120512119igl.0 for ; Thu, 19 Nov 2015 01:10:11 -0800 (PST) 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=AGx/7kG2zFx9sOB4C8e9bCOpayJx/U+otTdqblVz11k=; b=PHTYH2icSIjta9SC6a92ZT1p8COyzlS+9hFCoc2QZJi4aMVD93N3328ennBE0LhEFv v8RWKDmXE7N93OBh7uTokLzPDdJXtXgg/WSSP0HonHEo2xtFZy619b4H2YLhEVDes5TT AFigcGvphZ6/h9XAWcdlhl+Xg6khNjp8ujdCRDx2jTAD4qee3+iHVH7e3KyM50u/fMFL De0zF1khZJIREFZfK6fCBQMGIqUairt0YZlEhElPTpLDIW7A+aiMy1jNZKfX42lwGIIO f5NxSkftTku4ZEJkL78kU/HCor+xPor3DjSRklyPI8C9RsaZyo/hCt4R27z803RU30QW a2Kg== X-Received: by 10.50.20.73 with SMTP id l9mr7207100ige.50.1447924211403; Thu, 19 Nov 2015 01:10:11 -0800 (PST) MIME-Version: 1.0 Received: by 10.79.39.200 with HTTP; Thu, 19 Nov 2015 01:09:32 -0800 (PST) In-Reply-To: References: From: Gabriel Scherer Date: Thu, 19 Nov 2015 10:09:32 +0100 Message-ID: To: Runhang Li Cc: Ocaml Mailing List Content-Type: multipart/alternative; boundary=047d7bd6b0204876590524e120c1 Subject: Re: [Caml-list] GADT and weak polymorphism --047d7bd6b0204876590524e120c1 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Hi Runhang, There is an interaction between two advanced aspects of the OCaml language: 1. The relation between (non)-covariance and (non)-generalization of type variables due to the "relaxed value restriction" https://www.reddit.com/r/ocaml/comments/t8g2e/pdf_relaxing_the_value_restri= ction_by_jacques/ http://caml.inria.fr/pub/papers/garrigue-value_restriction-fiwflp04.pdf 2. The difficult analysis of variance of GADT parameters https://sympa.inria.fr/sympa/arc/caml-list/2012-02/msg00059.html https://hal.inria.fr/hal-00772993 There is no simple way to solve any of these questions, so I don't expect the OCaml language to improve on your example on the short/medium term. After thinking of these issues a bit more, I would personally support adding a notion of "pure arrow" ('a =3D> 'b), giving your interface the type ( **> ) : 'c =3D> ('a, 'b) hlist =3D> ('c -> 'a, 'b) hlist which would make any term built solely of ( **> ) and empty (and Empty and Cons) generalizable. However, this feature would be very limited in scope (due to the inherent difficulty of tracking effect) and suitable generalization require advanced type system features (effect systems, for example as found in Koka or F*). I think a minimal, advanced-uses-only feature (just a separation of pure and impure arrow) would already be a nice feature to have (also for functors), but there is no clear consensus on the question. On Tue, Nov 17, 2015 at 7:14 PM, Runhang Li wrote: > Hi, camels > > Consider the following module: > > module HList =3D struct > > type (_, _) hlist =3D > | Empty : ('a, 'a) hlist > | Cons : 'c * ('a, 'b) hlist -> ('c -> 'a, 'b) hlist > > let cons : type a b c. c -> (a, b) hlist -> (c -> a, b) hlist =3D > fun h tl -> Cons (h, tl) > > let empty =3D Empty > > let ( **> ) =3D cons > > let l =3D '2' **> "str" **> empty > > end > > The type of ``l`` is ``(char -> string -> =E2=80=98_a, =E2=80=98_a) hlist= ``. I would like > to know the reason that weak polymorphism shows up here. > > Thank you > > > Kindly, > > Runhang > > > -- > 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 --047d7bd6b0204876590524e120c1 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
Hi Runhang,

The= re is an interaction between two advanced aspects of the OCaml language:

1. The relation between (non)-covariance and (non)-generalizatio= n of type variables due to the "relaxed value restriction"
=C2= =A0 =C2=A0 https://www.reddit.com/r/ocaml/com= ments/t8g2e/pdf_relaxing_the_value_restriction_by_jacques/
=C2=A0=C2= =A0=C2=A0 http://caml.inria.fr/pub/papers/garrigue-value_restricti= on-fiwflp04.pdf
2. The difficult analysis of variance of GADT = parameters
=C2=A0=C2=A0=C2=A0 https://sympa.inria.fr/sympa/arc/caml-li= st/2012-02/msg00059.html
=C2=A0=C2=A0=C2=A0 https://hal.inria.fr/hal-00772993

Th= ere is no simple way to solve any of these questions, so I don't expect= the OCaml language to improve on your example on the short/medium term. Af= ter thinking of these issues a bit more, I would personally support adding = a notion of "pure arrow" ('a =3D> 'b), giving your int= erface the type
=C2=A0 ( **> ) : 'c =3D> ('a, 'b= ) hlist =3D> ('c -> 'a, 'b) hlist
which would ma= ke any term built solely of ( **> ) and empty (and Empty and Cons) gener= alizable. However, this feature would be very limited in scope (due to the = inherent difficulty of tracking effect) and suitable generalization require= advanced type system features (effect systems, for example as found in Kok= a or F*). I think a minimal, advanced-uses-only feature (just a separation = of pure and impure arrow) would already be a nice feature to have (also for= functors), but there is no clear consensus on the question.

On Tue, Nov 17, 2015 a= t 7:14 PM, Runhang Li <runhang@posteo.net> wrote:
Hi, camels

Consider the following module:

=C2=A0 =C2=A0 module HList =3D struct

=C2=A0 =C2=A0 =C2=A0 type (_, _) hlist =3D
=C2=A0 =C2=A0 =C2=A0 =C2=A0 | Empty : ('a, 'a) hlist
=C2=A0 =C2=A0 =C2=A0 =C2=A0 | Cons=C2=A0 : 'c * ('a, 'b) hlist = -> ('c -> 'a, 'b) hlist

=C2=A0 =C2=A0 =C2=A0 let cons : type a b c. c -> (a, b) hlist -> (c -= > a, b) hlist =3D
=C2=A0 =C2=A0 =C2=A0 =C2=A0 fun h tl -> Cons (h, tl)

=C2=A0 =C2=A0 =C2=A0 let empty =3D Empty

=C2=A0 =C2=A0 =C2=A0 let ( **> ) =3D cons

=C2=A0 =C2=A0 =C2=A0 let l =3D '2' **> "str" **> em= pty

=C2=A0 =C2=A0 end

The type of ``l`` is ``(char -> string -> =E2=80=98_a, =E2=80=98_a) h= list``. I would like to know the reason that weak polymorphism shows up her= e.

Thank you


Kindly,

Runhang


--
Caml-list mailing list.=C2=A0 Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocam= l_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs<= /blockquote>

--047d7bd6b0204876590524e120c1--