<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">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_-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>