Opened 5 years ago

Last modified 4 weeks 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, Artyom.Kazak, int-index, kosmikus
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)

implies.hs (816 bytes) - added by illissius 5 years ago.

Download all attachments as: .zip

Change History (26)

Changed 5 years ago by illissius

Attachment: implies.hs added

comment:1 Changed 5 years ago by simonpj

Cc: dimitris@… added
difficulty: Unknown
Milestone: 7.6.1

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

comment:2 Changed 5 years ago by 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!).

comment:3 Changed 5 years ago by 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.

comment:4 Changed 5 years ago by 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.

comment:5 Changed 5 years ago by 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

comment:6 Changed 5 years ago by 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!

comment:7 Changed 5 years ago by igloo

Milestone: 7.6.17.6.2

comment:8 Changed 4 years ago by duairc

Cc: shane@… added

comment:9 Changed 4 years ago by 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.

comment:10 Changed 4 years ago by 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.

comment:11 Changed 4 years ago by akio

Cc: tkn.akio@… added

comment:12 Changed 3 years ago by thoughtpolice

Milestone: 7.6.27.10.1

Moving to 7.10.1.

comment:13 Changed 3 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:14 Changed 22 months ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

comment:15 Changed 17 months ago by thomie

Milestone: 8.0.1

comment:16 Changed 15 months ago by maoe

Cc: maoe added

comment:17 Changed 11 months ago by RyanGlScott

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:18 Changed 10 months ago by Iceland_jack

Last edited 10 months ago by Iceland_jack (previous) (diff)

comment:19 Changed 10 months ago by Iceland_jack

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.

Last edited 10 months ago by Iceland_jack (previous) (diff)

comment:20 Changed 10 months ago by Iceland_jack

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 :&:
Last edited 10 months ago by Iceland_jack (previous) (diff)

comment:21 Changed 10 months ago by Iceland_jack

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, where W is a collection of constraints that need to be discharged, and G are assumptions that may be used while discarding W. In the GHC source code, the constraints in G are referred to as given constraints, while the ones in W are known as wanted constraints. The intuition behind an implication constraint is that W contains the constraints that were collected while checking a program fragment, while G contains local assumptions that are available only in this particular piece of code.

comment:22 Changed 8 months ago by Iceland_jack

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 8 months ago by Iceland_jack

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)

comment:24 Changed 4 weeks ago by Artyom.Kazak

Cc: Artyom.Kazak int-index added

comment:25 Changed 4 weeks ago by kosmikus

Cc: kosmikus added
Note: See TracTickets for help on using tickets.