Unlifted data types

[Simon Peyton Jones]

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 call-by-value; 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 (Haskell-style) 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 source-language 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 low-hanging fruit to be had. Maybe we can get a lot more benefit without completely re-imagining 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 re-imagining 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; ghc-devs
|  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