Unlifted data types

Dan Doel dan.doel at gmail.com
Tue Oct 27 23:42:13 UTC 2015


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


    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

    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.


-- 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

More information about the ghc-devs mailing list