Opened 5 years ago
Last modified 5 months ago
#5927 new feature request
A type-level "implies" constraint on Constraints
Reported by: | illissius | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler (Type checker) | Version: | 7.4.1 |
Keywords: | Cc: | dimitris@…, shane@…, tkn.akio@…, maoe, RyanGlScott | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
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.
Attachments (1)
Change History (24)
Changed 5 years ago by
Attachment: | implies.hs added |
---|
comment:1 Changed 5 years ago by
Cc: | dimitris@… added |
---|---|
difficulty: | → Unknown |
Milestone: | → 7.6.1 |
comment:2 Changed 5 years ago by
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 asfoo :: (Ord Int => Eq Int) -> Int
and then expects anOrd 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 writeforall 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!).
comment:3 Changed 5 years ago by
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.
comment:4 Changed 5 years ago by
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 -> Constraint
s.
I hope this is clearer. Don't hesitate to holler at me if I'm talking nonsense.
comment:5 Changed 5 years ago by
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
comment:6 Changed 5 years ago by
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!
comment:7 Changed 5 years ago by
Milestone: | 7.6.1 → 7.6.2 |
---|
comment:8 Changed 4 years ago by
Cc: | shane@… added |
---|
comment:9 Changed 4 years ago by
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.
comment:10 Changed 4 years ago by
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.
comment:11 Changed 3 years ago by
Cc: | tkn.akio@… added |
---|
comment:13 Changed 2 years ago by
Milestone: | 7.10.1 → 7.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:15 Changed 14 months ago by
Milestone: | 8.0.1 |
---|
comment:16 Changed 12 months ago by
Cc: | maoe added |
---|
comment:17 Changed 7 months ago by
Cc: | RyanGlScott added |
---|
I do have a pratical use-case for this feature: I think it would help solve part of the story for being able to derive Generic
instances for GADTs (see Trac issues #8560 and #10514). In particular, I think ImplicationConstraints
would allow be to be polymorphic over any existentially quanitified constraint in a GADT. In particular, there are GADTs like this:
class GShow a where gshow :: a -> String data T a where MkT :: GShow a => a -> T a
GHC generics currently lacks a facility for expressing the existential GShow
constraint. I think we could add something like this:
data EC c f a where MkEC :: c => f a -> EC c f a
Then we could derive a Generic
instance for T
like so:
instance Generic (T a) where type Rep (T a) = D1 ('MetaData "T" "Ghci2" "interactive" 'False) (C1 ('MetaCons "MkT" 'PrefixI 'False) (EC (GShow a) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))) from (MkT x) = M1 (M1 (MkEC (M1 (K1 x)))) to (M1 (M1 (MkEC (M1 (K1 x))))) = MkT x
So far, so good. Now I want to be able to define a generic GShow
instance for T
(where GShow
comes from the generic-deriving library). We already have cases for all generic datatypes except EC
. This is what I want to be able to write:
class GShow' f where gshow' :: f a -> String instance (c => GShow' f) => GShow' (EC c f) where gshow' (MkEC x) = gshow' x
But for that, I need ImplicationConstraints
. If I want to generalize this to Generic1
instances, I'd probably need QuantifiedConstraints
too.
comment:19 Changed 7 months ago by
Would this Show
instance for Fmt work with ImplicationConstraints
((=>) :: (Type -> Constraints) -> (Type -> Constraints) -> Constraints
):
data Fmt :: (* -> Constraint) -> (* -> *) -> * -> * where Int :: p Int => Fmt p r Int (:&) :: (p a, p b, p (a,b)) => Fmt p r a -> Fmt p r b -> Fmt p r (a,b) Lift :: p (r a) => r a -> Fmt p r a instance (ctx `Implies` Show) => Show (Fmt ctx r a) where show t = case t of Int -> "Int" l :& r -> show l ++ "&" ++ show r Lift r -> show r
A question on QuantifiedConstraints
on this same example in ticket:2893#comment18.
Edit: If I understand correctly (=>)
is the internal hom of constraints, Edward Kmett used the less ambiguous notation (|-)
in private correspondence.
The combination of ImplicationConstraints
+ QuantifiedConstraints
sounds very exciting.
comment:20 Changed 7 months ago by
Are any of these variations of Exists
useful
data Exists1 :: (Type -> Constraint) -> Type where Exists1 :: (ctx `Implies` c, c a) => a -> Exists1 ctx data Exists2 :: (Type -> Constraint) -> Type where Exists2 :: (ctx `Implies` c, ctx a) => a -> Exists2 c data Exists3 :: (Type -> Constraint) -> (Type -> Constraint) -> Type where Exists3 :: (ctx `Implies` c, ctx a) => a -> Exists3 ctx c data Exists4 :: (Type -> Constraint) -> Type where Exists4 :: (ctx `Implies` c, c a) => a -> Exists4 c data Exists5 :: (Type -> Constraint) -> (Type -> Constraint) -> Type where Exists5 :: (ctx `Implies` c, c a) => a -> Exists5 ctx c -- ...
Edit: Will you be able to write
hestur :: (forall ctx. ctx `Implies` Show => Exists ctx -> IO ()) -> ([Exists Show] -> [Exists (Show:&:Ord)] -> IO ()) hestur f xs ys = do traverse_ f xs traverse_ f ys
given combining constraints
class (c a, d a) => (c :&: d) a instance (c a, d a) => (c :&: d) a infixl 7 :&:
comment:21 Changed 7 months ago by
http://yav.github.io/publications/improving-smt-types.pdf
3.1 Implication Constraints
During type inference, GHC uses implication constraints, which do not appear in Haskell source code directly. An implication constraint is, roughly, of the form
G ⇒ W
, whereW
is a collection of constraints that need to be discharged, andG
are assumptions that may be used while discardingW
. In the GHC source code, the constraints inG
are referred to as given constraints, while the ones inW
are known as wanted constraints. The intuition behind an implication constraint is thatW
contains the constraints that were collected while checking a program fragment, whileG
contains local assumptions that are available only in this particular piece of code.
comment:22 Changed 5 months ago by
I believe MonadTrans
should be
class forall m. Monad m `Implies` Monad (t m) => MonadTrans t where lift :: Monad m => m a -> (t m) a
comment:23 Changed 5 months ago by
This has one of the best examples
type f ~> g = forall a. f a -> g a type f ~~> g = forall a b. f a b -> g a b newtype Free0 k p = Free0 (forall q. k q => (p -> q) -> q) newtype Free1 k p a = Free1 (forall q. k q => (p ~> q) -> q a) newtype Free2 k p a b = Free2 (forall q. k q => (p ~~> q) -> q a b) class Semigroup m class Semigroup m => Monoid m class Semigroupoid c class Semigroupoid c => Category c class Category c => Arrow c
you can define
instance p `Implies` Semigroup => Semigroup (Free0 p a) instance p `Implies` Monoid => Monoid (Free0 p a) instance p `Implies` Semigroupoid => Semigroupoid (Free2 p a) instance p `Implies` Category => Category (Free2 p a) instance p `Implies` Arrow => Arrow (Free2 p a) instance p `Implies` ArrowLoop => ArrowLoop (Free2 p a) -- (?)
instead of
instance Semigroup (Free0 Semigroup a) instance Semigroup (Free0 Monoid a) instance Monoid (Free0 Monoid a) instance Semigroupoid (Free2 Semigroupoid p) instance Semigroupoid (Free2 Category p) instance Semigroupoid (Free2 Arrow p) instance Semigroupoid (Free2 ArrowLoop p) instance Category (Free2 Category p) instance Category (Free2 Arrow p) instance Category (Free2 ArrowLoop p) instance Arrow (Free2 Arrow p) instance Arrow (Free2 ArrowLoop p) instance ArrowLoop (Free2 ArrowLoop p)
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
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