Unlifted data types

[Edward Kmett]

On Wed, Oct 28, 2015 at 9:19 AM, Richard Eisenberg <eir at cis.upenn.edu>
wrote:

> I don't have terribly much to add, but I do want to counter one point:
>
> On Oct 28, 2015, at 5:48 AM, Edward Kmett <ekmett at gmail.com> wrote:
> >  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.
>
> 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.
>

Yes, but this is the job of the particular instance. Remember the instance
gets to know the type it is working at, and its corresponding levity.

class Eq (l :: Levity) (t :: Type l) where
  (==) :: a -> a -> Bool

instance Eq @Unlifted (SmallMutableArray s a) where
  (==) = sameSmallMutableArray

instance Eq @Lifted [] where
  (==) = ...

Your objection arises for things like

instance Eq @l (Foo @l)

Where the same code has to execute with different levities, but if I can't
even case or seq on a value with polymorphic levity, and can't construct
such a value but merely pass it around then such code is still sound. It
isn't safe to write functions that return values of polymorphic levity. I
can however hand them back as (# a #). This is how we handle indexing into
a array today.

If we had a Maybe that was levity polymorphic in its argument

Maybe :: forall (l :: Levity). Type l -> Lifted

instance Eq @l a => Eq @Lifted (Maybe @l a) where
  Just a == Just b = a == b
  _ == _ = False

is still okay under these rules, it never case analyzes a value of
polymorphic levity, never seq's it. Neither of those things is legal
because you can't 'enter' the closure.

If it was levity polymorphic in the result type

Maybe :: forall (i :: Levity) (j :: Levity). Type i -> Type j

then your objection comes true.

I can't naively write:

instance Eq @i a => Eq j (Maybe @i @j a) where
  Just a == Just b = a == b
  _ == _ = False

without compiling the same code twice, because of the act of case analysis.

If we don't have real 'strict data types' in Lifted this situation never
arises though.

Even if we do I can write separate:

instance Eq @i a => Eq Lifted (Maybe @i Lifted a)
instance Eq @i a => Eq Unlifted (Maybe @i Unlifted a)

instances, unless we can do better by writing a class constraint on the
levity that we can use in a clever way here.

I'm mostly concerned with the middle case where we don't overload data
types on their levity, and try to recover the ability to talk about strict
data types by other more explicit means, but rather permit them to accept
arguments of different levities. There none of the code I care about
actually needs to act differently based on levity.

Anything that results in a function space there has to care about levity,
but until a type occurs on the right hand side of an (->) or I go to seq a
value of that type or case analyze it, I don't need to care about if its
lifted or unlifted.

With Dan's (!S) then things get more complicated in ways I don't fully
understand the ramifications of yet, as you might be able to lift some of
those restrictions.

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

In many ways pi comes down to doing typeclass like things, you're tracking
information from the type system. The vehicle we have for doing that today
is typeclasses. I've been thinking about anything that i have that actually
needs the "pi" there as a form of "constraint" passing all along, with the
constraint being whatever introspection you need to allow on the type to
carry on.

Imagine, for a moment, that we have an alternate universe where strict is
> the default, and we have
>
> > data Lazy a = Thunk (() -> a) | WHNF a
>
> The WHNF is a bit of a lie, because this representation would mean that
> the contents of a WHNF are fully evaluated. But let's not get hung up on
> that point.
>
> Then, we have
>
> > type family BaseType a where
> >   BaseType (Lazy a) = a
> >   BaseType a = a
> >
> > class Forceable a where
> >   force :: a -> BaseType a
> >
> > instance Forceable a where
> >   force = id
> >
> > instance Forceable (Lazy a) where
> >  force (Thunk f) = f ()
> >  force (WHNF a) = a
>
> Things that need to behave differently depending on strictness just take a
> dictionary of the Forceable class. Equivalently, they make a runtime
> decision of whether to force or not. So we don't need an exponential number
> of maps. We need a map that makes some runtime decisions. And the optimizer
> can be taught that specializing  these decisions may be helpful.
>
> Of course, none of this would be exposed. And I'm not suggesting that we
> need to make the core language strict-by-default. But it clarified things,
> for me at least, when I realized this is regular old ad-hoc polymorphism,
> not something fancier.


Yep.

-Edward
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20151028/d049ffd6/attachment.html>