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 <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 > <javascript:_e(%7B%7D,'cvml','dan.d...@gmail.com');>> wrote: > >> On Wed, Sep 9, 2015 at 9:03 AM, Richard Eisenberg <e...@cis.upenn.edu >> <javascript:_e(%7B%7D,'cvml','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 >> <javascript:_e(%7B%7D,'cvml','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