<html>
<head>
<meta http-equiv="Content-Type" content="text/html;
charset=windows-1252">
</head>
<body>
<p><br>
</p>
<div class="moz-cite-prefix">On 9/7/21 8:41 PM, Richard Eisenberg
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:010f017bc2da0727-00662b22-2002-46db-8989-ae5874af25f5-000000@us-east-2.amazonses.com">
<meta http-equiv="Content-Type" content="text/html;
charset=windows-1252">
<br class="">
<div><br class="">
<blockquote type="cite" class="">
<div class="">On Sep 6, 2021, at 11:21 AM, John Ericson <<a
href="mailto:john.ericson@obsidian.systems" class=""
moz-do-not-send="true">john.ericson@obsidian.systems</a>>
wrote:</div>
<br class="Apple-interchange-newline">
<div class="">
<meta http-equiv="Content-Type" content="text/html;
charset=windows-1252" class="">
<div class="">
<p class="">On 9/2/21 11:04 PM, Richard Eisenberg wrote:<br
class="">
</p>
<blockquote type="cite"
cite="mid:010f017ba99d4730-68884819-acc3-427b-93ef-7c26e3cd0b53-000000@us-east-2.amazonses.com"
class="">On Sep 2, 2021, at 2:56 PM, john.ericson <<a
href="mailto:john.ericson@obsidian.systems" class=""
moz-do-not-send="true">john.ericson@obsidian.systems</a>>
wrote:
<div class="">
<blockquote type="cite" class=""><br
class="Apple-interchange-newline">
<div class="">
<meta content="text/html; charset=windows-1252"
http-equiv="Content-Type" class="">
<div class="">
<div
style="font-size:10pt;font-family:Verdana,Arial,Helvetica,sans-serif;"
class="">Does the most basic e.g.
<div class=""><br class="">
</div>
<div class="">newtype Some f where</div>
<div class=""> MkSome :: forall a. f a ->
Some f<br id="br3" class="">
<br class="">
Have one of those problematic equalities?<br
id="br3" class="">
</div>
</div>
</div>
</div>
</blockquote>
<div class=""><br class="">
</div>
<div class="">No. That's not a GADT -- the constructor
doesn't restrict anything about `f`.</div>
</div>
</blockquote>
<p class="">Morally, sure, but GHC doesn't know about
this.<br class="">
</p>
</div>
</div>
</blockquote>
<div><br class="">
</div>
<div>Sure it does -- GHC doesn't include an equality constraint
as one of the fields of MkSome. This isn't about extensions --
it's about the way the data constructor is interpreted.</div>
</div>
</blockquote>
<p>Oops, agreed. I guess meant extensions didn't seem to check for
this in a really syntax-driven way. But yes deciding the cases
apart is not hard once the data definition is compiled.<br>
</p>
<blockquote type="cite"
cite="mid:010f017bc2da0727-00662b22-2002-46db-8989-ae5874af25f5-000000@us-east-2.amazonses.com">
<div>
<blockquote type="cite" class="">
<div class="">
<div class="">
<blockquote type="cite"
cite="mid:010f017ba99d4730-68884819-acc3-427b-93ef-7c26e3cd0b53-000000@us-east-2.amazonses.com"
class="">
<div class="">
<div class=""><br class="">
</div>
<div class="">I think you're after newtype
existentials. I think these should indeed be
possible, because what you propose appears to be the
same as</div>
<div class=""><br class="">
</div>
<div class="">newtype Some f = MkSome (exists a. f a)</div>
<div class=""><br class="">
</div>
<div class="">We can probably support the syntax you
wrote, too, but I don't want to commit to that right
now.</div>
</div>
</blockquote>
<p class="">The syntax I wrote is already basically valid?</p>
<pre class="">data Some f = forall a. Some (f a)
</pre>
<pre class="">data Some f where MkSome :: forall a f. f a -> Some f</pre>
<p class="">Is accepted</p>
<pre class="">newtype Some f = forall a. Some (f a)
</pre>
<pre class="">newtype Some f where MkSome :: forall a f. f a -> Some f
</pre>
<p class="">Is not with "A newtype constructor cannot have
existential type variables"</p>
<p class="">I propose we teach GHC how these "GADTs" in
fact merely have existential variables, and not the FC
constraints that require the extra evaluation for
soundness. Than we can get the operational/runtime
benefits of what you propose for cheap. Don't get me
wrong -- the other aspects in the paper this doesn't
address are still quite valuable, but I think this is a
useful stepping stone / removal of artificial
restrictions we should do first.</p>
<p class="">This sort of thing is brought up in #1965,
where it is alleged this is in fact more difficult than
it sounds. All more reason it is a good stepping stone,
I say!<br class="">
</p>
</div>
</div>
</blockquote>
<div><br class="">
</div>
<div>This is more difficult than it sounds. :) Newtypes are
implemented via coercions in Core, and coercions are
inherently bidirectional. The appearance of an existential in
this way requires one-way conversions, which are currently not
supported. So, to get what you want, we'd have to modify the
core language as in the existentials paper, along with some
extra work to automatically add `pack` and `open` -- rather
similar to the type inference described in the existentials
paper. The bottom line for me is that this seems just as hard
as implementing the whole thing, so I see no value in having
the stepping stone. If we always wrote out the newtype
constructor, then maybe we could use its appearance to guide
the `pack` and `open` but we don't: sometimes, we just use
`coerce`. So I really don't think this is any easier than
implementing the paper as written. Once that's done, we can
come back and add this new feature relatively easily (I
think).</div>
</div>
</blockquote>
Makes sense. That route is indeed harder than I was thinking.<br>
<p>There was a time before coercions when I gather newtypes were
mostly implemented with a special-case lowering to STG. I imagine
it would be quite easy to implement this that way, but that door
is now mostly shut.</p>
<p>I had a few more thoughts, but I am not sure if I should trouble
the list with them as they are still a bit rough around the edges.
Suffice to say, I hope we could sort of "smooth out" the feature
space a bit so that these and GADTs are not completely different,
e.g. I think all existential variables can be projected like this
(I opened #20337 for this), and perhaps connect GADTs to the
existentials with evidence you mention in the "future work"
section, so "true" GADTs also have structural counterparts in a
similar way.</p>
<p>Happy to just continue mulling on it until a proposal or
something, however. :)</p>
<p>John<br>
</p>
</body>
</html>