Unlifted data types

[Edward Kmett]

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.

data Nat = Z | S !Nat

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.

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.

I'm partial to those parts of the idea and think it works pretty well.

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. =/

-Edward

On Tue, Oct 27, 2015 at 7:42 PM, Dan Doel <dan.doel at gmail.com> wrote:

> Hello,
>
> I've added a section with my notes on the minimal semantics required
> to address what Haskell lacks with respect to strict types.
>
> Ed Kmett pointed me to some stuff that I think may fix all the
> problems with the !T sort of solution. It builds on the new constraint
> being considered for handling impredicativity. The quick sketch goes
> like this. Given the declaration:
>
>     data Nat = Z | S !Nat
>
> then:
>
>     Nat :: *
>     !Nat :: Unlifted
>     S :: Nat -> Nat
>
> But we also have:
>
>     !Nat <~ Nat
>
> and the witness of this is just an identity function, because all
> values of type !Nat are legitimate values of type Nat. Then we can
> have:
>
>     case n of
>       S m -> ...
>       Z -> ...
>
> where m has type !Nat, but we can still call `S m` and the like,
> because !Nat <~ Nat. If we do use `S m`, the S call will do some
> unnecessary evaluation of m, but this can (hopefully) be fixed with an
> optimization based on knowing that m has type !Nat, which we are
> weakening to Nat.
>
> Thoughts?
>
> -- Dan
>
>
> On Thu, Oct 8, 2015 at 8:36 AM, Richard Eisenberg <eir at cis.upenn.edu>
> wrote:
> >
> > On Oct 8, 2015, at 6:02 AM, Simon Peyton Jones <simonpj at microsoft.com>
> wrote:
> >
> >> What's the wiki page?
> >
> > https://ghc.haskell.org/trac/ghc/wiki/UnliftedDataTypes
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20151027/c7f6c030/attachment.html>