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 <ekm...@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.d...@gmail.com> wrote: > On Wed, Sep 9, 2015 at 9:03 AM, Richard Eisenberg <e...@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@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
