Unlifted data types

[Edward Kmett]

On Wed, Oct 28, 2015 at 5:05 AM, Simon Peyton Jones <simonpj at microsoft.com>
wrote:

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

This is one of the things we'd like to be able to fix. Right now I have a
small explosion of code going on that is being duplicated over and over to
parameterize over different unlifted types.

In the discussions about levity/lifting so far Dan and I have been trying
to tease apart what cases can be handled "forall" style rather than "pi"
style to borrow the split from Richard's presentation, just to get at a
sense of what really could be talked about without needing different
calling conventions, despite lifting. There are situations where we are
truly polymorphic in lifting, e.g. (==) from Eq and compare from Ord don't
care if the arguments of type 'a' are lifted or not.

Until you go to write a function application that returns a value of that
type. If all you do is rearrange them then that machinery can be parametric
in the choice. `map` on the other hand, cares about the selection because
of the `f x` application.

(Similarly, `min` and `max` from Ord do care about the convention on hand.)

One could see a world wherein you could parameterize such an instance on
levity explicitly, but it is pretty exhausting to think about.


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

I was actually quite surprised to see a subtyping relationship rear its
head in:

https://ghc.haskell.org/trac/ghc/attachment/wiki/ImpredicativePolymorphism/Impredicative-2015/impredicativity.pdf

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


I'm somewhat dubious of most approaches that try to mix strictness and
laziness under one umbrella. That is why trying to tease out the small
handful of cases where we are truly parametric in levity seems interesting.
Finding out some situations existed where we really don't care if a type is
lifted or not was eye opening to me personally, at least.

-Edward


> |  -----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
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20151028/43ca4900/attachment.html>