Unlifted data types
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.
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?
More information about the ghc-devs