Unlifted data types

[Dan Doel]

I've added a section on parametric levity polymorphism to the wiki.
Sorry it took so long.

I might add some thoughts about first-class `!a` being the only
semantic hole in our current strict data type situation later if I
remember to do so.

On Thu, Sep 10, 2015 at 10:26 AM, Richard Eisenberg <eir at cis.upenn.edu> wrote:
> These observations from Ed and Dan are quite helpful. Could one of you put
> them on the wiki page? I hadn't considered the possibility of truly
> parametric levity polymorphism.
>
> Thanks!
> Richard
>
> On Sep 9, 2015, at 3:30 PM, Edward Kmett <ekmett at gmail.com> wrote:
>
> I think ultimately the two views of levity that we've been talking diverge
> along the same lines as the pi vs forall discussion from your Levity
> polymorphism talk.
>
> I've been focused entirely on situations where forall suffices, and no
> distinction is needed in how you compile for both levities.
>
> Maybe could be polymorphic using a mere forall in the levity of the boxed
> argument it carries as it doesn't care what it is, it never forces it,
> pattern matching on it just gives it back when you pattern match on it.
>
> Eq or Ord could just as easily work over anything boxed. The particular Eq
> _instance_ needs to care about the levity.
>
> Most of the combinators for working with Maybe do need to care about that
> levity however.
>
> e.g. consider fmap in Functor, the particular instances would care. Because
> you ultimately wind up using fmap to build 'f a' values and those need to
> know how the let binding should work. There seems to be a pi at work there.
> Correct operational behavior would depend on the levity.
>
> But if we look at what inference should probably grab for the levity of
> Functor:
>
> you'd get:
>
> class Functor (l : Levity) (l' : Levity') (f :: GC l -> GC l') where
>    fmap :: forall a b. (a :: GC l) (b :: GC l). (a -> b) -> f a -> f b
>
> Baed on the notion that given current practices, f would cause us to pick a
> common kind for a and b, and the results of 'f'. Depending on how and if we
> decided to default to * unless annotated in various situations would drive
> this closer and closer to the existing Functor by default.
>
> These are indeed distinct functors with distinct operational behavior, and
> we could implement each of them by supplying separate instances, as the
> levity would take part in the instance resolution like any other kind
> argument.
>
> Whether we could expect an average Haskeller to be willing to do so is an
> entirely different matter.
>
> -Edward
>
>
> On Wed, Sep 9, 2015 at 12:44 PM, Dan Doel <dan.doel at gmail.com> wrote:
>>
>> On Wed, Sep 9, 2015 at 9:03 AM, Richard Eisenberg <eir at cis.upenn.edu>
>> wrote:
>> > No functions (excepting `error` and friends) are truly levity
>> > polymorphic.
>>
>> I was talking with Ed Kmett about this yesterday, and he pointed out
>> that this isn't true. There are a significant array of levity
>> polymorphic functions having to do with reference types. They simply
>> shuffle around pointers with the right calling convention, and don't
>> really care what levity their arguments are, because they're just
>> operating uniformly either way. So if we had:
>>
>>     MVar# :: forall (l :: Levity). * -> TYPE (Boxed l) -> TYPE (Boxed
>> Unlifted)
>>
>> then:
>>
>>     takeMVar :: forall s (l :: Levity) (a :: TYPE (Boxed l)). MVar# s
>> l a -> State# s -> (# State# s, a #)
>>     putMVar :: forall s (l :: Levity) (a :: Type (Boxed l)). MVar# s l
>> a -> a -> State# s -> State# s
>>
>> are genuinely parametric in l. And the same is true for MutVar#,
>> Array#, MutableArray#, etc.
>>
>> I think data type constructors are actually parametric, too (ignoring
>> data with ! in them for the moment; the underlying constructors of
>> those). Using a constructor just puts the pointers for the fields in
>> the type, and matching on a constructor gives them back. They don't
>> need to care whether their fields are lifted or not, they just
>> preserve whatever the case is.
>>
>> But this:
>>
>> > We use levity polymorphism in the types to get GHC to use its existing
>> > type inference to infer strictness. By the time type inference is done, we
>> > must ensure that no levity polymorphism remains, because the code generator
>> > won't be able to deal with it.
>>
>> Is not parametric polymorphism; it is ad-hoc polymorphism. It even has
>> the defaulting step from type classes. Except the ad-hoc has been
>> given the same notation as the genuinely parametric, so you can no
>> longer identify the latter. (I'm not sure I'm a great fan of the
>> ad-hoc part anyway, to be honest.)
>>
>> -- Dan
>> _______________________________________________
>> ghc-devs mailing list
>> ghc-devs at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
>
>