A type-level "implies" constraint on Constraints

[illissius]

I have a datatype:

data Exists c where Exists :: c a => a -> Exists c

I have an instance for it:

instance Show (Exists Show) where
    show (Exists a) = show a

And that's alright, as far as it goes: any Exists Show can indeed itself be shown. But I want more. I want to be able to say:

instance (c `Implies` Show) => Show (Exists c) where
    show (Exists a) = show a

In other words, I want to be able to say that any (Exists c) where the constraint c implies Show can be shown. For example, if Num still had a Show constraint, I wouldn't want to have to write a separate instance Show (Exists Num) to be able to show an Exists Num; I would want to be able to write a single instance (along the lines of the above) which works for both.

GHC clearly has this information: it lets me use a function of type forall a. Eq a => a -> r as one of type forall a. Ord a => a -> r, but not vice versa, so it knows that Ord implies Eq, but not vice versa. I've attached a file which demonstrates this and a couple of other examples.

What's not completely clear to me is what would be the appropriate way to be able to ask it about this. An Implies constraint to parallel the (~) constraint would work, but with what syntax? (Just straightforwardly call it Implies?) And what semantics -- what would be the kind of Implies? It's notable that in the above example its arguments aren't of type Constraint, but rather * -> Constraint, and for (* -> *) -> Constraint it could similarly work, and with MPTCs * -> * -> Constraint and (* -> *) -> (* -> *) -> Constraint and * -> (* -> *) -> Constraint and so on probably also make sense... but I have no idea how to formalize this, where the boundaries lie, and whether it makes any kind of sense. I can try to think harder about it if that would help, but hopefully the outlines of the situation are more immediately obvious to someone on the GHC team.

[simonpj]

What you say makes sense, but I don't have any idea how to achieve it. One way to get what you want woudl be something like

instance (forall a. c a => Show a) => Show (Exists c) where ...

and that is close to the idea in Section 7.2 of  Derivable Type Classes.

I have no idea how difficult this would to actually implement, but last time I thought about it, it seemed pretty hard. I'll milestone it at 7.6 for now, but it's much more than an incremental feature.

Simon

[illissius]

If I'm understanding correctly, the problem could be decomposed into two parts?

- On the one hand you would have an implication constraint between Constraints, c => d meaning that c implies d. GHC actually accepts this kind of syntax already, but it seems to mean something different (if I write foo :: (Ord Int => Eq Int) => Int, it seems to treat this as foo :: (Ord Int => Eq Int) -> Int and then expects an Ord Int => Eq Int, whatever that is, as a value-level argument?).

- On the other hand you would have the quantified constraints feature from #2893. In the same way that you could write forall a. Monoid (m a), together with the previous feature you could write forall a. c a => Show a.

If that's the case then, seeing that quantified constraints already has a ticket, I'll clarify that this one is referring to the other half. It's also more useful by itself for my own use case because quantified constraints can be emulated to some extent with GADTs and  evil hacks, but I don't see any way at all to express something like c => d (but correct me if I'm wrong!).

[simonpj]

Yes, I was referring exclusively to #2893 (but I'd forgotten we have a ticket for it).

I'm afraid I don't understand the other part you describe.

[illissius]

The canonical example of what #2893 lets you write is something like:

instance (Monad m, forall a. Monoid (m a)) => MonadPlus m where ...

The example from the paper is:

instance (Binary a, forall b. Binary b => Binary (f b)) => Binary (GRose f a) where ...

And the example here was:

instance (forall a. c a => Show a) => Show (Exists c) where ...

The way I have it in my head it's not clear to me that #2893 would, on its own, let you write the latter two examples. To put it simplistically it would you write the forall, but not the =>.

The way I'm reading the second example above is, "if (Binary a), and also (Binary (f b)) follows from (Binary b) for any b, then Binary (GRose f a)". The first example is saying, "if (Monad m), and also (Monoid (m a)) for any a, then (MonadPlus m)". The difference is that in the MonadPlus example and all existing Haskell there's noplace where you say "if b follows from a, then c", you only say "if b, then c". But the latter two examples do also have this "if b follows from a, then c" construct. And I think #2893 is what would let you say the "for any a" part of it, while the feature described by this ticket is what would let you say the "if b follows from a, then" part.

If we look at three simple examples:

instance forall a. C (A a) => D A where ...

instance (C a => C (A a)) => E (A a) where ...

instance (forall a. C a => C (A a)) => D A where ...

then #2893 (let's call it QuantifiedConstraints) would let you write the first example, this ticket (let's call it ImplicationConstraints) would let you write the second example, but only their combination would let you write the third example.

I'm imagining that, with ImplicationConstraints, (=>) would be a type level operator similar to (~):

(~)  :: forall k. k -> k -> Constraint
(=>) :: Constraint -> Constraint -> Constraint

and you would need QuantifiedConstraints to be able to use (=>) to also talk about k1...kN -> Constraints.

I hope this is clearer. Don't hesitate to holler at me if I'm talking nonsense.

[simonpj]

OK well

• Indeed I was thinking of the combination of QuantifiedConstraints and ImplicationConstraints; thanks for clarifying
• The design and implementation would be a significant task.
• I don't have a clear picture of the cost/benefit ratio

[illissius]

Right; obviously it's up to you and the rest of the GHC team to figure out what it makes sense to spend time on. This is just to keep track of one of the things that would be nice. Thanks for your time!

[goldfire]

There's not really built-in compiler support for these ideas, but have you seen the  constraints package? It allows you to manually enter and use implication relationships. This doesn't solve the fundamental problem here, but it may help with a workaround.

[illissius]

I know about it (referenced it actually in an earlier comment), thanks! I don't think I have an actual practical problem to be worked around. I was just experimenting, exploring, and testing the limits of what's possible. As usual I hit them.