<div dir="ltr">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.<div><br></div><div>I've been focused entirely on situations where forall suffices, and no distinction is needed in how you compile for both levities.</div><div><br></div><div>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.</div><div><br></div><div>Eq or Ord could just as easily work over anything boxed. The particular Eq _instance_ needs to care about the levity.<br></div><div><br></div><div><div>Most of the combinators for working with Maybe do need to care about that levity however.</div></div><div><br></div><div>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.</div><div><br></div><div>But if we look at what inference should probably grab for the levity of Functor:</div><div><br></div><div>you'd get:</div><div><br></div><div>class Functor (l : Levity) (l' : Levity') (f :: GC l -> GC l') where </div><div>   fmap :: forall a b. (a :: GC l) (b :: GC l). (a -> b) -> f a -> f b</div><div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>Whether we could expect an average Haskeller to be willing to do so is an entirely different matter.</div><div><br></div><div>-Edward</div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Sep 9, 2015 at 12:44 PM, Dan Doel <span dir="ltr"><<a href="mailto:dan.doel@gmail.com" target="_blank">dan.doel@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On Wed, Sep 9, 2015 at 9:03 AM, Richard Eisenberg <<a href="mailto:eir@cis.upenn.edu">eir@cis.upenn.edu</a>> wrote:<br>
> No functions (excepting `error` and friends) are truly levity polymorphic.<br>
<br>
</span>I was talking with Ed Kmett about this yesterday, and he pointed out<br>
that this isn't true. There are a significant array of levity<br>
polymorphic functions having to do with reference types. They simply<br>
shuffle around pointers with the right calling convention, and don't<br>
really care what levity their arguments are, because they're just<br>
operating uniformly either way. So if we had:<br>
<br>
    MVar# :: forall (l :: Levity). * -> TYPE (Boxed l) -> TYPE (Boxed Unlifted)<br>
<br>
then:<br>
<br>
    takeMVar :: forall s (l :: Levity) (a :: TYPE (Boxed l)). MVar# s<br>
l a -> State# s -> (# State# s, a #)<br>
    putMVar :: forall s (l :: Levity) (a :: Type (Boxed l)). MVar# s l<br>
a -> a -> State# s -> State# s<br>
<br>
are genuinely parametric in l. And the same is true for MutVar#,<br>
Array#, MutableArray#, etc.<br>
<br>
I think data type constructors are actually parametric, too (ignoring<br>
data with ! in them for the moment; the underlying constructors of<br>
those). Using a constructor just puts the pointers for the fields in<br>
the type, and matching on a constructor gives them back. They don't<br>
need to care whether their fields are lifted or not, they just<br>
preserve whatever the case is.<br>
<br>
But this:<br>
<span class=""><br>
> 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.<br>
<br>
</span>Is not parametric polymorphism; it is ad-hoc polymorphism. It even has<br>
the defaulting step from type classes. Except the ad-hoc has been<br>
given the same notation as the genuinely parametric, so you can no<br>
longer identify the latter. (I'm not sure I'm a great fan of the<br>
ad-hoc part anyway, to be honest.)<br>
<span class="HOEnZb"><font color="#888888"><br>
-- Dan<br>
</font></span><div class="HOEnZb"><div class="h5">_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</div></div></blockquote></div><br></div>