<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>I talked to Carter a bit on IRC for my progress on that front,
but I thought maybe this would be a good time to mention this more
widely<br>
</p>
<p>- The constraint side is iffy. Local constraints and constraint
kinds make it hard to have some sort of codata guardedness /
cotermination checking argument for higher order coercion
"instances" that doesn't also need to apply to the constraint
system at large, which makes it quite laborious to increase
expressive power without trade-offs like no local quantified
constraints. (Yay mission creep.)<br>
</p>
<p>- The core side looks good. Cale and I pretty confident in the
"coercions as fixed points of products", with {0, 1,
multiplication, and exponentiation, limits} passing my cardinality
sniff test that coercions still have no computational content and
thus can be erased.</p>
<p>- Additionally, I am less but decently confident (though I
haven't talked to Cale about this) that the existing role
admissibility solver can be repurposed to produce those
(to-be-erased) terms rather than just merely deciding the
admissibility of (opaque) axiomatic coercions. This change would
have no expressive power implications one way or the other, but
complete the "theory refactor" so that the "sans-nth" version
could be said to work end to end.</p>
<p>So tl;dr I <i>can't</i> actually do anything to help Carter's
problem at the moment, but I think I can get David's
<a class="moz-txt-link-freetext" href="https://github.com/ghc-proposals/ghc-proposals/pull/276">https://github.com/ghc-proposals/ghc-proposals/pull/276</a> over the
finish line, with the side benefit of loosening things up and
getting us closer so the higher-order roles problem seems less out
of reach.</p>
<p>I have revised my "progress report" wildly since I started
thinking about these things, but with the latest ratchet back, I
think I finally have a stable prediction.</p>
<p>Cheers,<br>
</p>
<p>John<br>
</p>
<div class="moz-cite-prefix">On 1/4/21 9:12 AM, Carter Schonwald
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAHYVw0yGm0Q_7a=Zpaq2T4_tojGQ5zQ6zSpAkHA=qLyOiVugyA@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<div dir="auto">Thx for the link. I’ll take a look at your
suggested reading. </div>
<div dir="auto"><br>
</div>
<div dir="auto">What are ways I could help progress whatever’s
needed to get to a nice ending?</div>
<div><br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Mon, Jan 4, 2021 at 9:00
AM Richard Eisenberg <<a href="mailto:rae@richarde.dev"
moz-do-not-send="true">rae@richarde.dev</a>> wrote:<br>
</div>
<blockquote class="gmail_quote" style="margin:0 0 0
.8ex;border-left:1px #ccc solid;padding-left:1ex">
<div
style="word-wrap:break-word;line-break:after-white-space"><br>
<div><br>
<blockquote type="cite">
<div>On Jan 3, 2021, at 1:02 PM, Carter Schonwald <<a
href="mailto:carter.schonwald@gmail.com"
target="_blank" moz-do-not-send="true">carter.schonwald@gmail.com</a>>
wrote:</div>
<br>
<div><span
style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration:none;float:none;display:inline!important">This
limitation is a misfeature, how can we make this
get addressed sooner rather than later? Is this
somewhere where Eg Haskell foundation or something
could help?</span></div>
</blockquote>
</div>
<br>
<div>Lifting the limitation would be nice, but it's a lot
of work. First, we need an updated theory for Core, with
a type safety proof. This proof is essential: it's what
our safety as a language depends on. Then, we'd need to
implement it. I'm more worried about the former than the
latter.</div>
<div><br>
</div>
<div>> i think its worth emphasizing that ghc today
uses a simplification of the original 2011 paper...</div>
<div><br>
</div>
<div>Yes, that was originally true, but the current
formulation goes beyond the 2011 paper in some respects.
See section 7.1 of <a
href="https://richarde.dev/papers/2016/coercible-jfp/coercible-jfp.pdf"
target="_blank" moz-do-not-send="true">https://richarde.dev/papers/2016/coercible-jfp/coercible-jfp.pdf</a>.</div>
<div><br>
</div>
<div>Roman writes:</div>
<div><br>
</div>
<div>> <span
style="font-family:Menlo-Regular;font-size:11px">I
think it's important we keep the definitions of
Functor and other</span></div>
<span style="font-family:Menlo-Regular;font-size:11px">fundamental
classes understandable by newcomers, and this change
would</span><br
style="font-family:Menlo-Regular;font-size:11px">
<span style="font-family:Menlo-Regular;font-size:11px">make
the definition look scary for a marginal benefit.</span>
<div><span
style="font-family:Menlo-Regular;font-size:11px"><br>
</span></div>
<div><span
style="font-family:Menlo-Regular;font-size:11px">This
is tough. I've considered a Functor definition like
the one Carter proposes before. I would personally
rather come up with the best definition first, then
figure out how to make it palatable to newcomers
second. For example, we could write (today)</span></div>
<div><span
style="font-family:Menlo-Regular;font-size:11px"><br>
</span></div>
<div><span
style="font-family:Menlo-Regular;font-size:11px">>
type Representational f = forall a b. Coercible a b
=> Coercible (f a) (f b)</span></div>
<div><span
style="font-family:Menlo-Regular;font-size:11px"><br>
</span></div>
<div><span
style="font-family:Menlo-Regular;font-size:11px">and
then the class constraint looks more pleasant. Or we
could create ways of suppressing confusing
information. Or there are other solutions. Depending
on the benefit of the change (here or elsewhere), I
would advocate holding off on making the change until
we can support it without disrupting the newcomer
story. But I wouldn't want to abandon the idea of an
improvement a priori just because of a disruption to
the newcomer experience.</span></div>
</div>
<div
style="word-wrap:break-word;line-break:after-white-space">
<div><span
style="font-family:Menlo-Regular;font-size:11px"><br>
</span></div>
<div><span
style="font-family:Menlo-Regular;font-size:11px">Richard</span></div>
</div>
</blockquote>
</div>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
Libraries mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Libraries@haskell.org">Libraries@haskell.org</a>
<a class="moz-txt-link-freetext" href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a>
</pre>
</blockquote>
</body>
</html>