Unlifted data types
Simon Peyton Jones
simonpj at microsoft.com
Wed Oct 28 09:05:07 UTC 2015
I'm out of bandwidth at the moment, but let me just remark that this is swampy territory. It's easy to mess up.
A particular challenge is polymorphism:
map :: forall a b. (a>b) > [a] > [b]
map f (x:xs) = (f x) : (map f xs)
In the compiled code for map, is a thunk built for (f x), or is it evaluated eagerly. Well, if you can instantiate the 'b' with !Int, say, then it should be evaluated eagerly. But if you instantiate with Int, then build a thunk. So, we really need two compiled versions of 'map'. Or perhaps four if we take 'b' into account. In general an exponential number.
That's one reason that GHC doesn't let you instantiate a polymorphic type variable with an unlifted type, even if it is boxed.
That is the reason that in "Types are calling conventions" we turn the entire intermediate language around, to make it callbyvalue; and add a lazy type constructor. Not Int and (Strict Int), but rather Int and (Lazy Int).
Another big issue is that *any* mixture of subtyping and (Haskellstyle) parametric polymorphism gets very complicated very fast. Especially when you add higher kinds. (Then you need variance annotations, and before long you want variance polymorphism.) I'm extremely dubious about adding subtyping to Haskell. That's one reason Scala is so complicated.
As a way to keep the discussion sane, I'd suggest focusing initially on the *intermediate language*, ignoring the sourcelanguage issues. That's what we did in "Types as calling conventions". There is a chance of writing out a complete syntax, a complete type system, and a complete operational semantics; and proving soundness etc. Once that foundation is done we can think about the source language.
Finally, there may be lowhanging fruit to be had. Maybe we can get a lot more benefit without completely reimagining GHC! Let's do that first. (I think that some of the proposals on the wiki page were in that direction.) But even for the low hanging fruit, getting the intermediate language changes (Core) nailed first would be good.
Bur reimagining GHC is good too. Swampy territory it may be, but it's also important, and there really *ought* to be a more seamless of combining strictness and laziness.
Simon
 Original Message
 From: Dan Doel [mailto:dan.doel at gmail.com]
 Sent: 27 October 2015 23:42
 To: Richard Eisenberg
 Cc: Simon Peyton Jones; ghcdevs
 Subject: Re: Unlifted data types

 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
More information about the ghcdevs
mailing list