Unlifted data types

[Dan Doel]

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