Eq1 & Ord1 deriving - #2703

I was thinking the derived instances would just look like eq1 = eq. Would that be straightforward?

I was thinking the derived instances would just look like eq1 = eq. Would that be straightforward?

That's what I'm proposing for the cases there is an Eq instance already. We could just make that a requirement though, and that's fine too - I still think the ability to take advantage of Eq1 constraints in Eq / Eq1 deriving is useful though.

I still think the ability to take advantage of Eq1 constraints in Eq / Eq1 deriving is useful though.

Can you elaborate? I'm not sure what you mean.

So in the code I have here, if there's an Eq1 constraint on a type, it will use eq1 when comparing rather than eq. Say you have a constructor like this:

data Foo f a 
  = Foo (f Int) a
  | Bar (f String) a
  | Baz (f a)

You can just derive eq for that with (Eq1 f, Eq a) => Eq (Foo f a) if Eq1 constraints are usable.

Another option might be to define data App f a = App (f a) with an instance (Eq1 f, Eq a) => Eq (App f a), and then to always use Eq. If the user wants to derive using Eq1, they could use App.

That would be like the trick of using Flip to derive a functor instance for an argument which is not the last argument. Not exactly elegant, but it reduces the amount of code, compared to special-casing it in the compiler.

Another option could be to use Eq1 when we see a type variable applied to some argument.

Let me think about this a bit more though.

Not exactly elegant, but it reduces the amount of code, compared to special-casing it in the compiler.

I don't think I follow you there? How could introducing a bunch of extra type-juggling stuff like App be less code than the derived Eq calling eq1 when it appears to be suitable according to the provided constraints?

You don't really need Eq1 to deal with that case I gave an example of earlier, it's just you end up with an awful set of constraints if you don't: (Eq a, Eq (f String), Eq (f Int), Eq (f a)) => Eq (Foo f a), but I'd probably use that over something like App if I had no other choice, since it would be less painful to deal with everywhere else the type is used.

Unless we had pattern synonyms that is, that's the only thing that would make the Flip / App style tricks a realistic prospect for me 😄

How could introducing a bunch of extra type-juggling stuff like App be less code than the derived Eq calling eq1

I just meant less compiler code, but it's not a big deal, I'm just thinking about other possible approaches. I think this is a fine approach. I would rather case on the syntax of the terms than the syntax of the constraint context, if possible, which is why I suggested looking for applications of a type variable to some other type.

@garyb What do you think about the idea of using eq1 when an argument is of type f a for some type variable f, instead of looking in the context?

Also, I think it would be cool to add an example for newtype Rec f = Rec (f (Rec f)) since we used to have trouble with infinite instances for that.

What do you think about the idea of using eq1 when an argument is of type f a for some type variable f, instead of looking in the context?

I think we might run into trouble with that - I don't think it's possible to make every type constructor Eq1 - Compose, for example.

Not really the point, I know, but Compose does have an Eq1 instance, you just need an adapter to go back to Eq (g a) and an unfortunate Functor constraint:

http://try.purescript.org/?gist=375025e006ceccd9975f89279e347a78

(I think you really don't need the Functor constraint actually, since App is a newtype, so you could just use unsafeCoerce, but still...)

Oh! Cool, I didn't think of that, and I tried for quite a while to come up with something too 😕

How would we make this work then? I would have thought the Eq1 constraint would be needed on an instance anyway, just as Eq is needed for something like Box a => Eq (Box a). Are we saying that the constraint is still needed, but just using the kind to determining whether eq1/ compare1 should be used instead? I mean, I'm fine with that, just not sure what it gains us over checking the constraints.

I would have thought the Eq1 constraint would be needed on an instance anyway

Yes, it'll be needed. I just want to explore options, and usually these things have been directed by the structure of the types, not the context, so I just wanted to go over pros and cons.

So, if we were doing this based on the kind of types, would it be a case of using eq1 for anything k -> Type -> Type? Say we had this nonsense:

newtype Weird a f = Weird (f a)

data MySum a
  = Value a
  | CouldBe (Maybe a)
  | HowAbout (Either a String)
  | Fuse (Coyoneda MySum a)
  | Pointless (Weird a MySum)

If we derived Eq for MySum, it'd try to use:

?

I'm suggesting only using eq1 when a type variable is applied to a type. The only case there would be the f a in Weird.

Hello, I'm Gary, and I miss extremely obvious points sometimes.

I've not forgotten about this one, I'll be working on it again soon.

What's left to do here? 🙂 Implementing Ord1 in the same manner as Eq1, or does Eq1s implementation need to change?

Will revive shortly.