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 c5ff346549e7 (Postfix) with ESMTPS id 16E255D5 for ; Fri, 10 Jan 2020 19:51:51 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.69,418,1571695200"; d="scan'208,217";a="430854520" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 10 Jan 2020 20:51:50 +0100 Received: by sympa.inria.fr (Postfix, from userid 20132) id E10017F3CD; Fri, 10 Jan 2020 20:51:50 +0100 (CET) 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 48EAB7F214 for ; Fri, 10 Jan 2020 20:51:47 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ivg@ieee.org; spf=Pass smtp.mailfrom=ivg@ieee.org; spf=None smtp.helo=postmaster@mail-lf1-f44.google.com IronPort-PHdr: =?us-ascii?q?9a23=3AubiH0BEohN1xqYkcwEtjeZ1GYnF86YWxBRYc798d?= =?us-ascii?q?s5kLTJ78pMWwAkXT6L1XgUPTWs2DsrQY0rGQ6f67EjVavd6oizMrSNR0TRgLiM?= =?us-ascii?q?EbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVr?= =?us-ascii?q?O+/7BpDdj9it1+C15pbffxhEiCCybL9vIhi6txvdu8gYjIdtN6o91BTEqWZUdu?= =?us-ascii?q?pLwm9lOUidlAvm6Meq+55j/SVQu/Y/+MNFTK73Yac2Q6FGATo/K2w669HluhfF?= =?us-ascii?q?TQuU+3sTSX4WnQZSAwjE9x71QJH8uTbnu+Vn2SmaOcr2Ta0oWTmn8qxmRgPkhD?= =?us-ascii?q?sBOjUk62zclNB+g7xHrxKgvxx/wpDbYIeJNPplY6jRecoWSXddUspNUiBMBJ63?= =?us-ascii?q?YYkSAOobJetXoIf9qFkOoxWwBgeiGf3hxSNTi3DswaE3yf4sHR3a0AEiGd8FrX?= =?us-ascii?q?TarM/yNKcXSe27z7fIwi/Fb/hL2Dn975TIchc/of6QXbJwcNbRyVIyHA7Cj1WQ?= =?us-ascii?q?t4PlMiiU1usTrWeU8fBsVeW1i24osgx8pCWkyMQ0ioTRmI4Z1lTJ+T96zYs1P9?= =?us-ascii?q?G0VU92bNy+HJZfuCyXMZZ9TNk4TGFyoik6z6ULuZ6lcygOz5Qq3xvfZOaGc4iM?= =?us-ascii?q?+x7jUOiRLSphiHJrd7+yiAy+8Uenyu37Wcm01EhFojBZndnLs3ABzx3T6s6ZRf?= =?us-ascii?q?th5kqtxyqD2gTJ5uxHIU04j7fXJp8jz7IqmZcevlzPHirsl0X3iK+WeF8k+u+t?= =?us-ascii?q?6+n/Y7XmuJCcOpR1ig7gLKshhNazAeMiMggBR2Sb4/iz1KX//U3lR7VHluE5nb?= =?us-ascii?q?PcsJDePMgboq+5AxRJ0os48Ba+DzKm0MwCknUdLVJFfgiHj4nzNF3ULvD4F6T3?= =?us-ascii?q?v1P5tT5vzPfCO/XEC4nEKnvK2OPkeL9h4kpfwSI8yNle49RfDbRXc9zpXUqklc?= =?us-ascii?q?LRCFcWNBCz3e3nCclmntcfR22nA6KUPeXVq1DetbFnGPWFeIJA4GW1EPMi/fO7?= =?us-ascii?q?yCZhwQZML5ns5oMebTWDJtojJkyYZXT2hdJYSTULswczCuvwhw/bCGIBVzOJR6?= =?us-ascii?q?s5owoDJse+F46aHtKsjbGMmiChEc8OPz0UOhW3CX7tMr68dbIMZSaVeJIzlzUF?= =?us-ascii?q?Uf2lRdZk203y8gD9zLVjI6zf/ShK7Z8=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0DsAgC71BhehiynVdFlhD6CHyqEDIEcj?= =?us-ascii?q?X6CEYlgDok9iAsJAQMBDC8BAYRAAoFyHAcBBDQTAhABAQQBAQECAQIDBAETAQE?= =?us-ascii?q?BCAsLCCmFPgyCOykBgnoBAQECARIRBBkBATcBBAsLCwM0AgIhARIBBQEcBhMbB?= =?us-ascii?q?4MEgksDCQUgoBKBAz2LJn8zgn4BAQWFCQ1jgTQJEoEkjBkagUE/gRE2gi8uPoI?= =?us-ascii?q?bhT6CXpdtlwpEgkGRK1yEJhuCd5dzmVSQEw8jgUaBen0IOzEGgjVQGA2SaYENA?= =?us-ascii?q?QKHXYVdJjCRIwEB?= X-IPAS-Result: =?us-ascii?q?A0DsAgC71BhehiynVdFlhD6CHyqEDIEcjX6CEYlgDok9iAs?= =?us-ascii?q?JAQMBDC8BAYRAAoFyHAcBBDQTAhABAQQBAQECAQIDBAETAQEBCAsLCCmFPgyCO?= =?us-ascii?q?ykBgnoBAQECARIRBBkBATcBBAsLCwM0AgIhARIBBQEcBhMbB4MEgksDCQUgoBK?= =?us-ascii?q?BAz2LJn8zgn4BAQWFCQ1jgTQJEoEkjBkagUE/gRE2gi8uPoIbhT6CXpdtlwpEg?= =?us-ascii?q?kGRK1yEJhuCd5dzmVSQEw8jgUaBen0IOzEGgjVQGA2SaYENAQKHXYVdJjCRIwE?= =?us-ascii?q?B?= X-IronPort-AV: E=Sophos;i="5.69,418,1571695200"; d="scan'208,217";a="430854509" X-MGA-submission: =?us-ascii?q?MDEeUn/qbkJTMKiJudEk8o00b51LjoPtGvokyn?= =?us-ascii?q?G5ECLlilLa1sJzwdZPSHgP/DWmXueCENOSWJcUlViwbRJJJrSftosCOM?= =?us-ascii?q?GqCPRoYFeJ9bZAJv28lZtrRc9Iu+RvlBD5c6ToDd1Gq7x+RgnvhCRpSN?= =?us-ascii?q?7PuYHGUF9Kpnwjb7CrJ7sCNw=3D=3D?= Received: from mail-lf1-f44.google.com ([209.85.167.44]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 10 Jan 2020 20:51:45 +0100 Received: by mail-lf1-f44.google.com with SMTP id f15so2342183lfl.13 for ; Fri, 10 Jan 2020 11:51:45 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=ieee.org; s=google; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=z0YVzUq1lWB0Noj8mgsMJqvWiLEAgCo3+SIHb68e9dM=; b=HiPOrPFdTSlOzu79Sscathw7LLL7XR/iHLckAzad67KNdTvbChSN326yf0bVXGyuC/ NmX3MH/E3fj/aWzit/SsNvNhA9szzlP0DVy1FEvZXR7ID/rBEU9tVtHalAhUK49RtdhV VPB+GTSa90Y8sxhu+VPrRWJj6vw8XPsZFdveY= X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:references:in-reply-to:from:date :message-id:subject:to:cc; bh=z0YVzUq1lWB0Noj8mgsMJqvWiLEAgCo3+SIHb68e9dM=; b=XOS4nCPjFX4loOiReY9nYe2+IlKMpDdgMBHCUnCmS313JKO4W28GXqE1Afl0qg/7Ke lAaAVsRiZD+7Gap0nxZTjcPHUI/RGTB4sjco5fr/4ujaEIXjebCZwV1JeEzU3Crv7fuO r8iopRE0DIvWgdvqh7xOP/tAjk7UFZ+IadO6TUCFwnhtAugreUlYrKYAdFXaQXWS+gv0 Ptj3mJbVY4ql5YLNaa9eJGkmkWWijpWz2NL2D3NnPdLllYtk2G/QW+7S9YJWvOQAA4RD e3DJ7dpN2caobpUFylSY161rIdTA9plSDWCgBI0ZroLDpnl+luNFUExMl0Lb35nz0BOr xP6g== X-Gm-Message-State: APjAAAVae4WfnLt3+dxn9Um1IA7fNY1wQSupjKrNfvvJy+t29jsiPzeY AdzPIEglL0u5azwc3Mzm/ZtXaJkjZ6b+/C71UiMR48y1r4w= X-Google-Smtp-Source: APXvYqyvJ+RQIcUsrR3Q88juxeCxqQhGvB8luO2ODDqRud4h8X05dW7Iiy7OdfbijYgPDwE4II+/q6EKF92LO/lKgQI= X-Received: by 2002:a19:dc14:: with SMTP id t20mr3379709lfg.47.1578685904822; Fri, 10 Jan 2020 11:51:44 -0800 (PST) MIME-Version: 1.0 References: <4d2b5367-a869-42bc-9547-b58864c10cf8@www.fastmail.com> <41592816-f82e-43a4-b67f-02e69623fe23@www.fastmail.com> <86wo9zljy0.fsf@gmail.com> In-Reply-To: <86wo9zljy0.fsf@gmail.com> From: Ivan Gotovchits Date: Fri, 10 Jan 2020 14:52:12 -0500 Message-ID: To: Malcolm Matalka Cc: rixed@happyleptic.org, caml-list Content-Type: multipart/alternative; boundary="00000000000091c8dd059bce74ff" Subject: Re: [Caml-list] Calling a single function on every member of a GADT? Reply-To: Ivan Gotovchits X-Loop: caml-list@inria.fr X-Sequence: 17947 Errors-to: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: --00000000000091c8dd059bce74ff Content-Type: text/plain; charset="UTF-8" On Fri, Jan 10, 2020 at 4:50 AM Malcolm Matalka wrote: > Thank you for the explanation Ivan. I have two questions inline. > > Ivan Gotovchits writes: > > > It has type `unit -> 'a -> 'a` therefore, if we would have the rank-1 > > polymorphism enabled for functions, we could apply it to the function > > > > let map2 : fun ('a. 'a -> 'a) -> 'b -> 'c -> 'b * 'c = fun f (x,y) > -> > > f x, f y > > Small thing, but wouldn't the faux type be the following, based on your > usage (making sure I'm following): > > fun ('a. 'a -> 'a) -> ('b * 'c) -> 'b * 'c > Yep, sure :) That's the problem with faux-typing) > Why is type checking creating a record different than type checking a > function argument? > > If we had the syntax (or something like it): > > let map2 : ('a. 'a -> 'a) -> ('b * 'c) -> ('b * 'c) > > Why would the type checker not be able to see that > > map2 good_id ("hi", 42) > > is valid but > > map2 (fine_id ()) ("hi", 32) > > is not, using the same logic that is verifying creating the "id" record > is not valid? > I believe it is possible, as it is possible in Haskell (with RankNTypes and ScopedTypeVariables). The main (theoretical) difference is that in OCaml we need to check whether an expression is expansive and use a specialized generalization in case if it is (for the relaxed value restriction). It will, however, complicate the type inference engine a lot, but most importantly, changing the typing rule of functions will have a tremendous impact on the language. So this would be a very impractical solution. Especially, since we don't have the mechanism of language extensions, enabling RankNTypes will make a lot of programs untypeable, as they will now require type annotations (recall that RankN is undecidable in general). It could probably be implemented as a compiler command line parameter, like `-rectypes` but this will be still quite impractical since more often code like `fun f -> f 1, f true` is a programmer error, rather than a true request for universal polymorphism (the same as with rectypes, recursive types a more often an error rather than a deliberate attempt). Therefore, enabling RankN(^1) polymorphism will type too many programs (not that it is unsound, just many programs won't have sense) at the cost of even more obscure type errors. On the other hand, we have three syntactic constructs that let us express non-prenex polymorphism of the necessary rank(^2) without breaking anything else. So it looks like a good deal - we can have rankN polymorphism and decidable type checker at the same time. Just think of polymorphic records/methods as an embedded DSL for rankN polymorphism. ============ Footnotes: 1) An important point, that I forgot to notice, is that enabling scoped type variables, will inevitably enable rankN polymorphism, e.g., since now any type could be a polytype, then suppose we have type `'a. ('b.'b -> 'a) -> 'a` could be instantiated to 'a = 'd. ('c. -> 'd) -> 'd, so that our type is now `'d. ('b. 'b -> ('c. 'c -> 'd) -> 'd) -> ('c. 'c -> 'd) -> 'd` which is now rank3. Therefore, enabling arbitrary quantification in the arrow type will lead to rankN and immediately make undecidable most of the type checker. 2) We can craft arbitrary rank using records with universally quantified type variables, e.g., here is an example of rank3 polymoprhism: type 'a rank1 = {f1 : 's. 's -> 'a} type 'a rank2 = {f2 : 'r. 'r -> 'a rank1} Indeed, `f2` has type `'a.('r. 'r -> ('s. 's -> 'a)` --00000000000091c8dd059bce74ff Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable


=
On Fri, Jan 10, 2020 at 4:50 AM Malco= lm Matalka <mmatalka@gmail.com= > wrote:
Than= k you for the explanation Ivan.=C2=A0 I have two questions inline.

Ivan Gotovchits <ivg@i= eee.org> writes:

> It has type `unit -> 'a -> 'a` therefore, if we would ha= ve the rank-1
> polymorphism enabled for functions, we could apply it to the function<= br> >
>=C2=A0 =C2=A0 =C2=A0 let map2 : fun ('a. 'a -> 'a) ->= 'b -> 'c -> 'b * 'c =3D fun f (x,y) ->
> f x, f y

Small thing, but wouldn't the faux type be the following, based on your=
usage (making sure I'm following):

fun ('a. 'a -> 'a) -> ('b * 'c) -> 'b * &#= 39;c

Yep, sure :) That's the proble= m with faux-typing)=C2=A0


Why is type checking creating a record different than type checking a
function argument?

If we had the syntax (or something like it):

let map2 : ('a. 'a -> 'a) -> ('b * 'c) -> (= 9;b * 'c)

Why would the type checker not be able to see that

map2 good_id ("hi", 42)

is valid but

map2 (fine_id ()) ("hi", 32)

is not, using the same logic that is verifying creating the "id" = record
is not valid?

I believe it is possible,= as it is possible in Haskell (with RankNTypes and ScopedTypeVariables). Th= e main (theoretical) difference is that in OCaml we need to check whether a= n expression is expansive and use a specialized generalization in case if i= t is (for the relaxed value restriction). It will, however, complicate the = type inference engine a lot, but most importantly, changing the typing rule= of functions will have a tremendous impact on the language. So this would = be a very impractical solution. Especially, since we don't have the mec= hanism of language extensions, enabling RankNTypes will make a lot of progr= ams untypeable, as they will now require type annotations (recall that Rank= N is undecidable in general). It could probably be implemented as a compile= r command line parameter, like `-rectypes` but this will be still quite imp= ractical since more often code like `fun f -> f 1, f true` is a programm= er error, rather than a true request for universal polymorphism (the same a= s with rectypes, recursive types a more often an error rather than a delibe= rate attempt). Therefore, enabling RankN(^1) polymorphism will type too man= y programs (not that it is unsound, just many programs won't have sense= ) at the cost of even more obscure type errors. On the other hand, we have = three syntactic constructs that let us express non-prenex polymorphism of t= he necessary rank(^2) without breaking anything else. So it looks like a go= od deal - we can have rankN polymorphism and decidable type checker at the = same time. Just think of polymorphic records/methods as an embedded DSL for= rankN polymorphism.

=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D
Footnotes:

1) An important poi= nt, that I forgot to notice, is that enabling scoped type variables, will i= nevitably enable rankN polymorphism, e.g., since now any type could be a po= lytype, then suppose we have type `'a. ('b.'b -> 'a) -&g= t; 'a` could be instantiated to 'a =3D 'd. ('c. ->=C2=A0= 'd) -> 'd, so that our type is now `'d. ('b. 'b -&g= t; ('c. 'c -> 'd) -> 'd) -> ('c. 'c -> = 'd) -> 'd` which is now rank3. Therefore, enabling arbitrary qua= ntification in the arrow type will lead to rankN and immediately make undec= idable most of the type checker.

2) We can craft a= rbitrary rank using records with universally quantified type variables, e.g= ., here is an example of rank3 polymoprhism:

=C2= =A0 type 'a rank1 =3D {f1 : 's. 's -> 'a}
=C2=A0 type= 'a rank2 =3D {f2 : 'r. 'r -> 'a rank1}
Indeed, `f2` has type `'a.('r. 'r -> ('s. &= #39;s -> 'a)`
--00000000000091c8dd059bce74ff--