Unlifted data types

[Dan Doel]

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.

You can't insantiate `b` to `!Int` without map quantifying over
levity, which is somewhat orthogonal (although it would have
interactions). Without that, b has kind *, and !Int has kind Unlifted,
so this is a kind error. Or, map is explicitly written having b ::
Unlifted, in which case it already has the right calling convention.

> That's one reason that GHC doesn't let you instantiate a polymorphic type variable with an unlifted type, even if it is boxed.

It's a reason to not put boxed, unlifted types in *. I don't think
it's a reason not to allow quantifying over a separate kind of
uniformly represented, unlifted types (i.e. doesn't include Int#,
Double#, etc.).

> 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'm not sure how much of this would be required. But how are you saved
from this in the impredicativity proposal, which is already attempting
to handle more of the induced subtyping of higher-rank types? I would
guess it's mostly a matter of, "we're not going to support all that."
Which might be fine for the unlifted stuff as well.

Richard wrote:
> But these do, I think. In running code, if (==) is operating over a lazy type, it has to check if the pointer points to a thunk. If (==) is operating over a strict one, it can skip the check. This is not a big difference, but it *is* a difference.

Yeah. It's not that (==) is parametric really. It's that Eq might be
able to be parameterized on levity. But this is very useful, since it
allows you to instantiate Eq on a bunch of unlifted reference types
instead of having to use one-off functions like sameMutableArray#.

> A little more thinking about this has led here: The distinction isn't really forall vs. pi. That is, in the cases where the levity matters, we don't really need to pi-quantify. Instead, it's exactly like type classes.

Yes, I think so, too. It is ad-hoc polymorphism that can be handled by
type classes. There is no reason for an explicit value-level witness
of levity that can be cased on, which is presumably what pi would
allow.