<div dir="ltr"><div>Hi Alex,</div><div>Also de-railing the conversation, the Utrecht Haskell Compiler supports existential types in addition to universally-quantified ones. The work on Atze Dijkstra (among others) describes some of the problems and possible solutions to inference:</div><div>- His PhD thesis [<a href="https://dspace.library.uu.nl/handle/1874/7352" target="_blank">https://dspace.library.uu.nl/handle/1874/7352</a>] describes existentials in Section 8.</div><div>- Their paper "A Lazy Language Needs a Lazy Type System" [<a href="https://dspace.library.uu.nl/handle/1874/346316" target="_blank">https://dspace.library.uu.nl/handle/1874/346316</a>] proposes treating existential types as "polymorphic contexts".</div><div><br></div><div>Going back to impredicativity, adding existential types would only complicate inference more, since there are more types to choose from while instantiating. But the delta would not be that large, since once a type constructor guards a type, everything inside of it should be equal, and checking equality of existential types is as hard as checking for universal types.</div><div><br></div><div>Alejandro<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">El vie., 6 sept. 2019 a las 16:21, Alex Rozenshteyn (<<a href="mailto:rpglover64@gmail.com" target="_blank">rpglover64@gmail.com</a>>) escribió:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>Hi Simon,</div><div><br></div><div>You're exactly right, of course. My example is confusing, so let me see if I can clarify.</div><div><br></div><div>What I want in the ideal is <code>map show [1, 'a', "b"]</code>. That is, minimal syntactic overhead to mapping a function over multiple values of distinct types that results in a homogeneous list. As the reddit thread points out, there are workarounds involving TH or wrapping each element in a constructor or using bespoke operators, but when it comes down to it, none of them actually allows me to say what I <i>mean</i>; the TH one is closest, but I reach for TH only in times of desperation.</div><div><br></div><div>I had thought that one of the things preventing this was lack of impredicative instantiation, but now I'm not sure. Suppose Haskell <i>did</i> have existentials; would <code>map show @(exists a. Show a => a) [1, 'a', "b"]</code> work in current Haskell and/or in quick-look?</div><div><br></div><div>Tangentially, do you have a reference for what difficulties arise in adding existentials to Haskell? I have a feeling that it would make working with GADTs more ergonomic.<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Sep 6, 2019 at 12:33 AM Simon Peyton Jones <<a href="mailto:simonpj@microsoft.com" target="_blank">simonpj@microsoft.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">





<div lang="EN-GB">
<div class="gmail-m_-2258385302581388879gmail-m_-1216500096407594109gmail-m_-7528168171117436718WordSection1">
<p class="MsoNormal"><span>I’m confused.   Char does not have the type (forall a. Show a =>a), so our example is iill-typed in System F, never mind about type inference.  Perhaps there’s a typo?   I think you may have ment<u></u><u></u></span></p>
<p class="MsoNormal"><span>               exists a. Show a => a<u></u><u></u></span></p>
<p class="MsoNormal"><span>which doesn’t exist in Haskell.  You can write existentials with a data type<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>data Showable where<u></u><u></u></span></p>
<p class="MsoNormal"><span>   S :: forall a. Show a => a -> Showable<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>Then<u></u><u></u></span></p>
<p class="MsoNormal"><span>               map show [S 1, S ‘a’, S “b”]<u></u><u></u></span></p>
<p class="MsoNormal"><span>works fine today (without our new stuff), provided you say<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>               instance Show Showable where<u></u><u></u></span></p>
<p class="MsoNormal"><span>                 show (S x) = show x<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>Our new system can only type programs that can be written in System F.   (The tricky bit is inferring the impredicative instantiations.)<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>Simon<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<div style="border-color:currentcolor currentcolor currentcolor blue;border-style:none none none solid;border-width:medium medium medium 1.5pt;padding:0cm 0cm 0cm 4pt">
<div>
<div style="border-color:rgb(225,225,225) currentcolor currentcolor;border-style:solid none none;border-width:1pt medium medium;padding:3pt 0cm 0cm">
<p class="MsoNormal"><b><span lang="EN-US">From:</span></b><span lang="EN-US"> ghc-devs <<a href="mailto:ghc-devs-bounces@haskell.org" target="_blank">ghc-devs-bounces@haskell.org</a>>
<b>On Behalf Of </b>Alex Rozenshteyn<br>
<b>Sent:</b> 06 September 2019 03:31<br>
<b>To:</b> Alejandro Serrano Mena <<a href="mailto:trupill@gmail.com" target="_blank">trupill@gmail.com</a>><br>
<b>Cc:</b> GHC developers <<a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a>><br>
<b>Subject:</b> Re: New implementation for `ImpredicativeTypes`<u></u><u></u></span></p>
</div>
</div>
<p class="MsoNormal"><u></u> <u></u></p>
<div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6pt;margin-left:0cm">
I didn't say anything when you were requesting use cases, so I have no right to complain, but I'm still a little disappointed that this doesn't fix my (admittedly very minor) issue:
<a href="https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.reddit.com%2Fr%2Fhaskell%2Fcomments%2F3am0qa%2Fexistentials_and_the_heterogenous_list_fallacy%2Fcsdwlp2%2F%3Fcontext%3D8%26depth%3D9&data=02%7C01%7Csimonpj%40microsoft.com%7Cf5bddbe8c13b424fad8a08d732724d04%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637033338810706935&sdata=a5c3ujC0kiPlocgHg8AX%2BwIP6ZH2hnqszCpnWOiqpGQ%3D&reserved=0" target="_blank">
https://www.reddit.com/r/haskell/comments/3am0qa/existentials_and_the_heterogenous_list_fallacy/csdwlp2/?context=8&depth=9</a><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6pt;margin-left:0cm">
For those who don't want to click on the reddit link: I would like to be able to write something like<code><span style="font-size:10pt"> map show ([1, 'a', "b"] :: [forall a. Show a => a])</span></code><code><span style="font-size:10pt;font-family:"Arial",sans-serif">,
 and have it work.</span></code><u></u><u></u></p>
</div>
</div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6pt;margin-left:0cm">
<u></u> <u></u></p>
<div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6pt;margin-left:0cm">
On Wed, Sep 4, 2019 at 8:13 AM Alejandro Serrano Mena <<a href="mailto:trupill@gmail.com" target="_blank">trupill@gmail.com</a>> wrote:<u></u><u></u></p>
</div>
<blockquote style="border-color:currentcolor currentcolor currentcolor rgb(204,204,204);border-style:none none none solid;border-width:medium medium medium 1pt;padding:0cm 0cm 0cm 6pt;margin-left:4.8pt;margin-right:0cm">
<div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6pt;margin-left:0cm">
Hi all,<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6pt;margin-left:0cm">
As I mentioned some time ago, we have been busy working on a new implementation of `ImpredicativeTypes` for GHC. I am very thankful to everybody who back then sent us examples of impredicativity which would be nice to support, as far as we know this branch
 supports all of them! :)<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6pt;margin-left:0cm">
If you want to try it, at <a href="https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Ftrupill%2Fghc%2Fcommit%2Fa3f95a0fe0f647702fd7225fa719a8062a4cc0a5%2Fpipelines%3Fref%3Dquick-look-build&data=02%7C01%7Csimonpj%40microsoft.com%7Cf5bddbe8c13b424fad8a08d732724d04%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637033338810716935&sdata=PP1imEsNrkIhloEV3AS52nrZBtyjen4i1e3pJTcMi6M%3D&reserved=0" target="_blank">
https://gitlab.haskell.org/trupill/ghc/commit/a3f95a0fe0f647702fd7225fa719a8062a4cc0a5/pipelines?ref=quick-look-build</a> you can find the result of the pipeline, which includes builds for several platforms (click on the "Artifacts" button, the one which looks
 like a cloud, to get them). The code is being developed at <a href="https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Ftrupill%2Fghc&data=02%7C01%7Csimonpj%40microsoft.com%7Cf5bddbe8c13b424fad8a08d732724d04%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637033338810716935&sdata=IgtSqJP4%2BhCfy3%2FHVsqX6wpPYVMS8D1wN46aXHnFcUw%3D&reserved=0" target="_blank">
https://gitlab.haskell.org/trupill/ghc</a>.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6pt;margin-left:0cm">
Any code should run *unchanged* except for some eta-expansion required for some specific usage patterns of higher-rank types. Please don't hesitate to ask any questions or clarifications about it. A merge request for tracking this can be found at
<a href="https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2Fmerge_requests%2F1659&data=02%7C01%7Csimonpj%40microsoft.com%7Cf5bddbe8c13b424fad8a08d732724d04%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637033338810716935&sdata=YJ5N9d7gXC2JbpqTvpqs4wjY%2F7Ev%2FikRdYIK%2Bhv4rRE%3D&reserved=0" target="_blank">
https://gitlab.haskell.org/ghc/ghc/merge_requests/1659</a><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6pt;margin-left:0cm">
Kind regards,<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6pt;margin-left:0cm">
Alejandro<u></u><u></u></p>
</div>
</div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6pt;margin-left:0cm">
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<a href="https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-devs&data=02%7C01%7Csimonpj%40microsoft.com%7Cf5bddbe8c13b424fad8a08d732724d04%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637033338810726922&sdata=jw0sroJW1D8MoBBxVKJROdGefo5gir%2BtQSto0b%2Bj3NA%3D&reserved=0" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><u></u><u></u></p>
</blockquote>
</div>
</div>
</div>
</div>

</blockquote></div>
</blockquote></div>