Opened 4 years ago

Last modified 2 years ago

#8767 new task

Add rules involving `coerce` to the libraries

Reported by: nomeata Owned by:
Priority: normal Milestone:
Component: Core Libraries Version: 7.9
Keywords: Cc: ekmett, hvr, dfeuer, core-libraries-committee@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: tests/simplCore/should_run/T2110.hs
Blocked By: #8718 Blocking:
Related Tickets: #2110 Differential Rev(s):
Wiki Page:

Description

With #2110 fixed, we can now add rules like

{-# RULES "map/coerce" [0] map coerce = coerce #-}

to the standard libraries. But probably this should happen together or after #8718.

Change History (32)

comment:1 Changed 4 years ago by Austin Seipp <austin@…>

In f96dc5470355ce52741c717b6387d7f61b6a8dc1/base:

Add RULE for "map coerce = map" (#8767)

Signed-off-by: Austin Seipp <austin@well-typed.com>

comment:2 Changed 4 years ago by thoughtpolice

Cc: hvr added
Milestone: 7.8.1
Status: newmerge
Version: 7.97.8.1-rc2

comment:3 Changed 4 years ago by thoughtpolice

Test Case: tests/simplCore/should_run/T2110.hs

comment:4 Changed 4 years ago by thoughtpolice

Please excuse the completely stupid commit message.

comment:5 Changed 4 years ago by goldfire

But, there should be many more similar RULES than just this, no? For example, any lawful Functor instance should have a RULE for its fmap, as I understand.

comment:6 Changed 4 years ago by nomeata

I don’t think there is a point in merging this into 7.8; the support for coerce in rules was added to master after the freeze ([b4715d6] up to [cde88e2]).

comment:7 Changed 4 years ago by thoughtpolice

Resolution: fixed
Status: mergeclosed

Ah, I see. In that case that's fine - it's strictly an optimization, so I'm don't really care about missing this little thing.

comment:8 Changed 4 years ago by thoughtpolice

Cc: ekmett added
Resolution: fixed
Status: closednew

(Whoops, accidentally closed.)

Richard, Edward probably has something to say about the fmap rule, but in general do we want it right now when it can break things? I'm under the impression there's not a sensible and safe one we can write that won't break for non-lawful Functors. (I guess we can tell everyone to always write ones that obey the rules, but I'm not sure how much that might backfire).

There was some discussion of related approaches a few months ago around ICFP time (don't have a link on me). Anyway, worth a good discussion.

comment:9 Changed 4 years ago by nomeata

I still believe that people should be free to write non-law-abiding instances (or maybe law-abiding up to some interface), and the compiler should not interfere with that.

We should simply suggest them to add a fmap coerce = coerce rule for their particular fmap if they care.

comment:10 Changed 4 years ago by ekmett

You can defintely have users write the rule for particular functors of course, but that means reasonably polymorphic code that is too complicated to INLINE will get penalized asymptotically, so in the long run I'd really like to find a better solution that might have a chance of firing on my code. ;)

comment:11 Changed 4 years ago by goldfire

Right. I forgot that #2110 isn't getting into 7.8. Then, neither should this.... which is good, because I agree that maybe some more thought is required.

I was not suggesting that there be a blanket fmap coerce --> coerce rule, just that we should add the specific rules for all the individual (lawful) Functors that we define. I agree completely that users should be free to write unlawful Functors if they wish to do so.

I don't believe there's a link to earlier discussions on fmap coerce issue because the discussions happened among actual humans, in an actual room, instead of among computers online. It's an amazing thought. In any case, I remember one conclusion being a suggestion to add a new method to Functor being fmapCoerce :: Coercible a b => f a -> f b. This would have a default implementation of fmapCoerce = fmap coerce (no surprise there) but could be reimplemented where there would be a performance improvement.

Returning to Edward's comment, I guess I don't understand the limits of the RULES mechanism to respond all that intelligently. In Core, anything that looks like fmap coerce in the source code would look something like $fmapIdForSomeInstance <type parameters> (\x -> x |> co). This should be easy enough to match at the Core level. If it's impossible to write a RULE that desugars to the pattern above, then I think it's a bug (er, feature request) in the RULES mechanism, not a call for a change to the Functor definition.

Though I'm not dead set against fmapCoerce in Functor, I believe that if we have to add such a thing, then there is a weakness in our design somewhere. During the conversations at ICFP, I was unaware of #2110 and Joachim's efforts to fix that bug. Now that we have that fixed, I believe fmapCoerce should be avoidable.

comment:12 Changed 4 years ago by nomeata

I was not suggesting that there be a blanket fmap coerce --> coerce rule, just that we should add the specific rules for all the individual (lawful) Functors that we define. I agree completely that users should be free to write unlawful Functors if they wish to do so.

Ok, good. Then we fully agree :-)

comment:13 Changed 4 years ago by ekmett

The fmapCoerce solution turned out not to be powerful enough to handle things like Compose f g while g remains polymorphic or many monad transformers. We vacillated between a few other solutions that let you add a different member to Functor that could lift coercions by the end of ICFP, but with GHC 7.8 happening "any day now" at the time we agreed to just punt on it until we could give it due deliberation.

My main point was that if the code is still polymorphic in the functor and complicated enough not to inline into a place where that rule can fire the rule doesn't help. We encourage people to write very polymorphic code. e.g. It solves many of the bugaboos people trot out about monad transformers and the like if you avoid picking a concrete instance until the last second. I'd be really sad to see that part of our culture die to get a few zero-cost newtype applications.

Anyways, not sure what the right solution is yet, but I did want to interject that whatever it is, fmapCoerce isn't it. ;)

comment:14 Changed 4 years ago by goldfire

Right -- of course. I guess I always am thinking that we have to know the Functor instance even to be thinking about any of this, because the Functor instance might not be lawful, in which case this optimization is bogus. But I do see how you might make progress with yet-to-be-imagined solution.

comment:15 Changed 4 years ago by ekmett

That is why I think any solution that works in a polymorphic setting or one too big to INLINE really involves adding something to Functor that permits the lifting of coercions for lawful functors. fmapCoerce was the first such candidate. It just isn't strong enough.

A more viable alternative is to add something like liftCoercion :: Functor f => Coercion a b -> Maybe (Coercion (f a) (f b)) to Functor, analogous to the precedent of how (<$) is already added there to permit faster 'scrubbing' of functor contents with increased sharing.

This'd permit liftCoercion Coercion = Just Coercion to be written (or generated) as a witness for the representational or phantom role of the argument, and it could be used inside an fmapCoerce to lift over complex polymorphic functors.

There are admittedly a lot of moving parts in such a design, though, and even that design as I recall isn't sufficient to address more complicated transformers and recursive data types, so there is still work to be done.

comment:16 Changed 4 years ago by thoughtpolice

Milestone: 7.8.17.10.1
Version: 7.8.1-rc27.9

comment:17 Changed 4 years ago by dmcclean

I'm out of my depth here, not even sure this thread is about what I'm running in to.

I want to coerce from f (Quantity d v) to f v where f is a functor, so that I can add up all the values without their wrappers in the way and then wrap the answer.

This works a charm if I specialize f to [], but doesn't compile ("because 'f (Quantity d v)' and 'f v' are different types") in the polymorphic version. (Full function below.)

sum :: forall f d v.(Num v, Foldable f, Functor f) => f (Quantity d v) -> Quantity d v
sum = coerce . Data.Foldable.sum . (\x -> x :: f v) . coerce

sum :: forall d v.(Num v) => [Quantity d v] -> Quantity d v
sum = coerce . F.sum . (\x -> x :: [v]) . coerce

Is this thread about making a workaround for that?

Is the reason that it's complicated because some functors have nominal roles? (Maybe a SortedList would break if you changed out Ord instances under it?) Or is there more to it than that?

comment:18 Changed 4 years ago by nomeata

Is this thread about making a workaround for that?

No. Or, not mainly.

Is the reason that it's complicated because some functors have nominal roles? (Maybe a SortedList would break if you changed out Ord instances under it?) Or is there more to it than that?

Precisely: We don’t know about the roles of type variables, so we cannot lift coercions through them.

I believe that a subsequent design of the system that will be able to cope with Monad’s join might be able to handle that, but I’m not up on that.

comment:19 Changed 4 years ago by dmcclean

Could the compiler always generate (Functor f, Coercible a b) => Coercible f a -> Coercible f b instances that magically either fmap coerce or coerce depending on the role of f's parameter? Wouldn't the concrete type of f be known by the time it came around to generating the instance?

comment:20 Changed 4 years ago by ekmett

dmcclean: Note: such a RULE is predicated on your Functor actually being lawful as well as having a representational argument.

(It'd also result in Coercible (f a) (f b).)

comment:21 Changed 4 years ago by dmcclean

I knew about the representational parameter part, that's why I thought maybe it was possible to only generate the instance if f has a representational parameter. i.e. it's not one once-and-for-all instance for all functors, instead it's "magically" (as the current coercible instances are) generated once at each functor type with the branching between fmap coerce and coerce happening after considering the concrete type of f.

The bit about the lawfulness I had missed.

I don't understand how it results in Coercible (f a) (f b) with no context, even if it is once-and-for-all and not the magical akin-to-an-axiom-schema way, but I'm sure you're correct.

It seems like the unlawful functor desideratum is very difficult to handle because we don't have a way to have a qualified type that is qualified by whether or not the Functor is lawful.

One possible thing would be to have an {-# UNLAWFUL #-} pragma, and when you are magically generating instances you branch three ways instead of 2. (Possibly such a pragma could allow more aggressive optimizations in other cases too, with an opt out for 'criminals'?)

1) If the role is representational and there's no unlawful pragma, you generate coerce. 2) If there's no unlawful pragma, but the role is something other than representational you generate fmap coerce. 3) If there's an unlawful pragma, you generate error "Attempt to coerce through unlawful functor Foo declared at line ...", on the grounds that error is not pretty, but neither is unlawfulness.

comment:22 Changed 4 years ago by goldfire

dmcclean: I think you want #9123.

comment:23 Changed 4 years ago by thoughtpolice

Component: libraries/baseCore Libraries
Owner: set to ekmett

Moving over to new owning component 'Core Libraries'.

comment:24 Changed 4 years ago by thomie

Cc: dfeuer core-libraries-committee@… added
commit 603b7be7bd3abaf0e2c210e8d9015b1d613b4715
Author: David Feuer <David.Feuer@gmail.com>
Date:   Thu Nov 13 21:12:05 2014 +0100

    Implement amap/coerce for Array (re #9796)
    
    Implement an `amap`/`coerce` rule in `GHC.Arr` to match the
    `map`/`coerce` rule in GHC.Base.
    
    In order to do so, delay inlining `amap` until phase 1.
    
    To prevent the inlining delay from causing major inefficiencies due to
    missed list fusion, rewrite `amap` to avoid relying on list fusion. This
    has the extra benefit of reducing the size of the compiled amap code by
    skipping the impossible case of an array with a negative size.
    
    Reviewed By: nomeata
    
    Differential Revision: https://phabricator.haskell.org/D471

comment:25 in reply to:  21 Changed 4 years ago by dfeuer

Replying to dmcclean:

One possible thing would be to have an {-# UNLAWFUL #-} pragma, and when you are magically generating instances you branch three ways instead of 2. (Possibly such a pragma could allow more aggressive optimizations in other cases too, with an opt out for 'criminals'?)

I think it would make more sense to track Functor instances believed to be (sufficiently) lawful. A functor could be labeled {-# LAWFUL #-} in either Unsafe or Trustworthy modules, and any derived Functor instance without a Functor context could be treated as lawful as well. A functor labeled as {-# LAWFUL #-} could of course be lawful only up to some isomorphism; the pragma would declare that the instance won't break in any important way if the compiler relies on the functor laws. A similar mechanism could presumably be applied to other classes as well.

Interaction with extreme polymorphism: to really take advantage, you'd presumably need to be able to express lawfulness in a context. So you'd need to be able to write something like

g :: ({-# LAWFUL #-} Functor f) => ...
}}}}

comment:26 Changed 4 years ago by thoughtpolice

Milestone: 7.10.17.12.1

Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

comment:27 Changed 3 years ago by htebalaka

I'm a little out of my depth with rewrite rules, but is there anything preventing rules being associated with a typeclass? Then you could have zero method typeclasses like

class Functor f => LawfulFunctor f where
    {-# RULES "fmap/coerce" fmap coerce = coerce #-}

and then any datatype that wants the rule just implements the typeclass, which is trivial. It would also address dfeuer's comment about lawfullness in constraints, though it would also generate a lot of noise in documentation (and might inherit the same issue with typeclasses that they can be hard to refactor).

comment:28 in reply to:  27 Changed 3 years ago by dfeuer

Replying to htebalaka:

I'm a little out of my depth with rewrite rules, but is there anything preventing rules being associated with a typeclass? Then you could have zero method typeclasses like

class Functor f => LawfulFunctor f where
    {-# RULES "fmap/coerce" fmap coerce = coerce #-}

and then any datatype that wants the rule just implements the typeclass, which is trivial. It would also address dfeuer's comment about lawfullness in constraints, though it would also generate a lot of noise in documentation (and might inherit the same issue with typeclasses that they can be hard to refactor).

I don't know too much about these things either, but I don't think this will work too well. The problem, as I understand it, is that the LawfulFunctor constraint has to be in place at the call site, which will generally not be the case even when the functor is actually an instance of LawfulFunctor.

comment:29 Changed 3 years ago by nomeata

Data.Map already has rules for map, this [pull request](https://github.com/haskell/containers/pull/163) adds them for mapKeysMonotonic.

comment:30 Changed 3 years ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

comment:31 Changed 3 years ago by thomie

Owner: ekmett deleted

comment:32 Changed 2 years ago by thomie

Milestone: 8.0.1
Note: See TracTickets for help on using tickets.