<div dir="ltr">The idea of treating !S as a subtype of S and then relying on the potential for new impredicativity machinery to let us just talk about how !S <= S makes me really happy.<div><br></div><div>data Nat = Z | S !Nat</div><div><br></div><div>Pattern matching on S could give back the tighter type !Nat rather than Nat for the argument, and if we ever have to show that to a user, the 'approximation' machinery would show it to users as Nat, concealing this implementation detail. Similarly matching with an as-pattern as part of a pattern that evaluates could do the same.</div><div><br></div><div>The constructor is a bit messier. It should really give back S :: Nat -> Nat as what the constructor should behave as rather than S :: !Nat -> Nat, because this will match existing behavior. Then the exposed constructor would force the argument before storing it away, just like we do today and we could recover via a sort of peephole optimization the elimination of the jump into the closure to evaluate when it is fed something known to be of type !Nat by some kind of "case/(!)-coercion" rule in the optimizer.</div><div><br></div><div>I'm partial to those parts of the idea and think it works pretty well.<br></div><div><div><br></div><div>I'm not sure how well it mixes with all the other discussions on levity polymorphism though. Notably: Trying to get to having !Nat live in an Unlifted kind, while Nat has a different kind seems likely to cause all sorts of headaches. =/</div></div><div><br></div><div>-Edward</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Oct 27, 2015 at 7:42 PM, Dan Doel <span dir="ltr"><<a href="mailto:dan.doel@gmail.com" target="_blank">dan.doel@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello,<br>
<br>
I've added a section with my notes on the minimal semantics required<br>
to address what Haskell lacks with respect to strict types.<br>
<br>
Ed Kmett pointed me to some stuff that I think may fix all the<br>
problems with the !T sort of solution. It builds on the new constraint<br>
being considered for handling impredicativity. The quick sketch goes<br>
like this. Given the declaration:<br>
<br>
    data Nat = Z | S !Nat<br>
<br>
then:<br>
<br>
    Nat :: *<br>
    !Nat :: Unlifted<br>
    S :: Nat -> Nat<br>
<br>
But we also have:<br>
<br>
    !Nat <~ Nat<br>
<br>
and the witness of this is just an identity function, because all<br>
values of type !Nat are legitimate values of type Nat. Then we can<br>
have:<br>
<br>
    case n of<br>
      S m -> ...<br>
      Z -> ...<br>
<br>
where m has type !Nat, but we can still call `S m` and the like,<br>
because !Nat <~ Nat. If we do use `S m`, the S call will do some<br>
unnecessary evaluation of m, but this can (hopefully) be fixed with an<br>
optimization based on knowing that m has type !Nat, which we are<br>
weakening to Nat.<br>
<br>
Thoughts?<br>
<span class="HOEnZb"><font color="#888888"><br>
-- Dan<br>
</font></span><div class="HOEnZb"><div class="h5"><br>
<br>
On Thu, Oct 8, 2015 at 8:36 AM, Richard Eisenberg <<a href="mailto:eir@cis.upenn.edu">eir@cis.upenn.edu</a>> wrote:<br>
><br>
> On Oct 8, 2015, at 6:02 AM, Simon Peyton Jones <<a href="mailto:simonpj@microsoft.com">simonpj@microsoft.com</a>> wrote:<br>
><br>
>> What's the wiki page?<br>
><br>
> <a href="https://ghc.haskell.org/trac/ghc/wiki/UnliftedDataTypes" rel="noreferrer" target="_blank">https://ghc.haskell.org/trac/ghc/wiki/UnliftedDataTypes</a><br>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</div></div></blockquote></div><br></div>