<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
  </head>
  <body>Currently:<br><br>   head ~(a :| _) = a<br>   tail ~(_ :| as) = as<br><br>But head and tail are both strict. At best the '~'s have no effect.<br><br>Should I open a PR to change it to<br><br>   head (a :| _) = a<br>   tail (_ :| as) = as<br><br>or maybe even more clearly<br><br>   head !(a :l _) = a<br>   tail !(_ :| as) = as<br><br>?<br>--Keith<br>Sent from my phone with K-9 Mail.<br><br><div class="gmail_quote">On January 4, 2021 2:40:58 PM UTC, John Ericson <john.ericson@obsidian.systems> wrote:<blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">

    <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>
  
</blockquote></div></body></html>