Unlifted data types

[Carter Schonwald]

Would this allow having a strict monoid instance for maybe, given the right
hinting at the use site?

On Wednesday, September 9, 2015, 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
> <javascript:_e(%7B%7D,'cvml','dan.doel at gmail.com');>> wrote:
>
>> On Wed, Sep 9, 2015 at 9:03 AM, Richard Eisenberg <eir at cis.upenn.edu
>> <javascript:_e(%7B%7D,'cvml','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
>> <javascript:_e(%7B%7D,'cvml','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/20150910/a8b72125/attachment.html>