<html><head>
<style id="css_styles" type="text/css"><!--blockquote.cite { margin-left: 5px; margin-right: 0px; padding-left: 10px; padding-right:0px; border-left: 1px solid #cccccc }
blockquote.cite2 {margin-left: 5px; margin-right: 0px; padding-left: 10px; padding-right:0px; border-left: 1px solid #cccccc; margin-top: 3px; padding-top: 0px; }
a img { border: 0px; }
li[style='text-align: center;'], li[style='text-align: right;'] { list-style-position: inside;}
body { font-family: Segoe UI; font-size: 12pt; }--></style></head><body class="plain"><div>Hi,</div><div><br /></div><div>FWIW, I'm neither a proponent of adding an unlifted keyword or modifier, nor a strong opponent.</div><div>I just want to make aware of the point I raise in https://github.com/ghc-proposals/ghc-proposals/pull/265#issuecomment-901904173, namely that</div><div><ul style="list-style-type: disc;"><li>No keyword is sufficient to describe the full spectrum of levity-polymorphic data types</li><li>Our language server is already smart enough to give the necessary info on hover, without even needing to navigate to the definition (where we would hope to see `unlifted` or a lack thereof). It also works with levity-polymorphism.</li></ul><div>Cheers,<br />Sebastian</div></div>
<div><br /></div>
<div>------ Originalnachricht ------</div>
<div>Von: "Eric Seidel" <<a href="mailto:eric@seidel.io">eric@seidel.io</a>></div>
<div>An: "Simon Peyton Jones" <<a href="mailto:simonpj@microsoft.com">simonpj@microsoft.com</a>>; "<a href="mailto:ghc-steering-committee@haskell.org">ghc-steering-committee@haskell.org</a>" <<a href="mailto:ghc-steering-committee@haskell.org">ghc-steering-committee@haskell.org</a>>; "Sebastian Graf" <<a href="mailto:sgraf1337@gmail.com">sgraf1337@gmail.com</a>></div>
<div>Gesendet: 19.08.2021 21:16:39</div>
<div>Betreff: Re: [ghc-steering-committee] Unlifted data types</div><div><br /></div>
<div id="x026c17e1ae604db"><blockquote type="cite" class="cite2">
<div class="plain_line">On Thu, Aug 19, 2021, at 06:14, Simon Peyton Jones wrote:</div>
<blockquote type="cite" class="cite">
<div class="plain_line"> | We use types to communicate the externally-visible behavior of our</div>
<div class="plain_line"> | programs: the number of arguments to a function and their types, effects</div>
<div class="plain_line"> | incurred in the form of monads, etc. Why should liftedness and the</div>
<div class="plain_line"> | implications for evaluation strategies be different?</div>
<div class="plain_line"> </div>
<div class="plain_line"> We use them to *communicate* behaviour, but not to *specify* behaviour.</div>
<div class="plain_line"> That is done by the definition of the function itself.</div>
</blockquote>
<div class="plain_line"> </div>
<div class="plain_line">I disagree, types are a great specification language. The whole point of advanced</div>
<div class="plain_line">type system features is to enhance the specification language so we can</div>
<div class="plain_line">specify more interesting properties.</div>
<div class="plain_line"> </div>
<div class="plain_line">Often, we do this so that the type checker can *verify* our code, but there are plenty</div>
<div class="plain_line">of cases where we use types to *drive code generation*. Consider GHC.Generics.</div>
<div class="plain_line">We can write a highly-polymorphic JSON serialization function</div>
<div class="plain_line"> </div>
<div class="plain_line"> gToJSON :: Generic a => a -> JSON</div>
<div class="plain_line"> </div>
<div class="plain_line">which we can then instantiate at different types, e.g.</div>
<div class="plain_line"> </div>
<div class="plain_line"> data Foo</div>
<div class="plain_line"> fooToJSON :: Foo -> JSON</div>
<div class="plain_line"> fooToJSON = gToJSON</div>
<div class="plain_line"> </div>
<div class="plain_line"> data Bar</div>
<div class="plain_line"> barToJSON :: Bar -> JSON</div>
<div class="plain_line"> barToJSON = gToJSON</div>
<div class="plain_line"> </div>
<div class="plain_line">fooToJSON and barToJSON have the exact same definition, but very different</div>
<div class="plain_line">semantics. Their complete semantics depends on *both* their definition *and*</div>
<div class="plain_line">their type signatures.</div>
<div class="plain_line"> </div>
<div class="plain_line">I think the deeper point here is that Haskell's dynamic semantics depends on</div>
<div class="plain_line">its static semantics. We can't evaluate a Haskell program without knowing the</div>
<div class="plain_line">types involved.</div>
</blockquote></div>
</body></html>