Improving the instances of Data.Functor.{Product,Sum}

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
21 messages Options
12
Reply | Threaded
Open this post in threaded view
|

Improving the instances of Data.Functor.{Product,Sum}

chessai .
Consider the Eq instance for these types. Currently we rely on:

(Eq1 f, Eq1 g, Eq a)

But some potential improvements include changing to:

(Eq (f (g a))) (FlexibleContexts)

or

(forall x. Eq x => Eq (f x), forall x. Eq x => Eq (g x), Eq a)
(QuantifiedConstraints)

There was a discussion sometime last year about the same thing
regarding Semigroup/Monoid instances for `Compose` [1]. Additionally,
the question has been raised again for Data.Functor.{Product,Sum} on
Gitlab [2, 3]. There has been no consensus in either case, but that's
not too worrying as both discussions have been brief. I'm currently
not happy with the {Eq,Ord,Show}{1,2} family of classes, and would
hope to work toward their removal, or at least the shrinking of their
presence in base. Even though the linked proposals are about a single
type, I think it's important that we come up with a decision and stick
with it. Having different APIs for different types here would be
pretty confusing, and some could even say sloppy.

Please let me know your thoughts.

[1]: https://mail.haskell.org/pipermail/libraries/2019-July/029771.html
[2]: https://gitlab.haskell.org/ghc/ghc/issues/17015
[3]: https://gitlab.haskell.org/ghc/ghc/merge_requests/1704
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Improving the instances of Data.Functor.{Product,Sum}

Eric Mertens
I prefer to avoid FlexibleInstances wherever I can. The last thing I'd heard about quantified constraints was that they were buggy and I've been avoiding relying on them. (I should probably review that assumptions at some point.) Having a class like Eq1 is the cleaner option. I'd rather fix up these classes than work to get rid of them.

On Fri, Mar 13, 2020 at 8:59 PM chessai . <[hidden email]> wrote:
Consider the Eq instance for these types. Currently we rely on:

(Eq1 f, Eq1 g, Eq a)

But some potential improvements include changing to:

(Eq (f (g a))) (FlexibleContexts)

or

(forall x. Eq x => Eq (f x), forall x. Eq x => Eq (g x), Eq a)
(QuantifiedConstraints)

There was a discussion sometime last year about the same thing
regarding Semigroup/Monoid instances for `Compose` [1]. Additionally,
the question has been raised again for Data.Functor.{Product,Sum} on
Gitlab [2, 3]. There has been no consensus in either case, but that's
not too worrying as both discussions have been brief. I'm currently
not happy with the {Eq,Ord,Show}{1,2} family of classes, and would
hope to work toward their removal, or at least the shrinking of their
presence in base. Even though the linked proposals are about a single
type, I think it's important that we come up with a decision and stick
with it. Having different APIs for different types here would be
pretty confusing, and some could even say sloppy.

Please let me know your thoughts.

[1]: https://mail.haskell.org/pipermail/libraries/2019-July/029771.html
[2]: https://gitlab.haskell.org/ghc/ghc/issues/17015
[3]: https://gitlab.haskell.org/ghc/ghc/merge_requests/1704
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries


--
Eric Mertens

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Improving the instances of Data.Functor.{Product,Sum}

Zemyla
Also, keeping it Haskell98 compliant makes it easier for newer users to grok.

On Fri, Mar 13, 2020, 23:15 Eric Mertens <[hidden email]> wrote:
I prefer to avoid FlexibleInstances wherever I can. The last thing I'd heard about quantified constraints was that they were buggy and I've been avoiding relying on them. (I should probably review that assumptions at some point.) Having a class like Eq1 is the cleaner option. I'd rather fix up these classes than work to get rid of them.

On Fri, Mar 13, 2020 at 8:59 PM chessai . <[hidden email]> wrote:
Consider the Eq instance for these types. Currently we rely on:

(Eq1 f, Eq1 g, Eq a)

But some potential improvements include changing to:

(Eq (f (g a))) (FlexibleContexts)

or

(forall x. Eq x => Eq (f x), forall x. Eq x => Eq (g x), Eq a)
(QuantifiedConstraints)

There was a discussion sometime last year about the same thing
regarding Semigroup/Monoid instances for `Compose` [1]. Additionally,
the question has been raised again for Data.Functor.{Product,Sum} on
Gitlab [2, 3]. There has been no consensus in either case, but that's
not too worrying as both discussions have been brief. I'm currently
not happy with the {Eq,Ord,Show}{1,2} family of classes, and would
hope to work toward their removal, or at least the shrinking of their
presence in base. Even though the linked proposals are about a single
type, I think it's important that we come up with a decision and stick
with it. Having different APIs for different types here would be
pretty confusing, and some could even say sloppy.

Please let me know your thoughts.

[1]: https://mail.haskell.org/pipermail/libraries/2019-July/029771.html
[2]: https://gitlab.haskell.org/ghc/ghc/issues/17015
[3]: https://gitlab.haskell.org/ghc/ghc/merge_requests/1704
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries


--
Eric Mertens
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Improving the instances of Data.Functor.{Product,Sum}

chessai .
Eric,

Could you expound on why you try to avoid Flexible{Contexts,Instances} in your own code? That might be useful to look at here.

On Fri, Mar 13, 2020, 9:22 PM Zemyla <[hidden email]> wrote:
Also, keeping it Haskell98 compliant makes it easier for newer users to grok.

On Fri, Mar 13, 2020, 23:15 Eric Mertens <[hidden email]> wrote:
I prefer to avoid FlexibleInstances wherever I can. The last thing I'd heard about quantified constraints was that they were buggy and I've been avoiding relying on them. (I should probably review that assumptions at some point.) Having a class like Eq1 is the cleaner option. I'd rather fix up these classes than work to get rid of them.

On Fri, Mar 13, 2020 at 8:59 PM chessai . <[hidden email]> wrote:
Consider the Eq instance for these types. Currently we rely on:

(Eq1 f, Eq1 g, Eq a)

But some potential improvements include changing to:

(Eq (f (g a))) (FlexibleContexts)

or

(forall x. Eq x => Eq (f x), forall x. Eq x => Eq (g x), Eq a)
(QuantifiedConstraints)

There was a discussion sometime last year about the same thing
regarding Semigroup/Monoid instances for `Compose` [1]. Additionally,
the question has been raised again for Data.Functor.{Product,Sum} on
Gitlab [2, 3]. There has been no consensus in either case, but that's
not too worrying as both discussions have been brief. I'm currently
not happy with the {Eq,Ord,Show}{1,2} family of classes, and would
hope to work toward their removal, or at least the shrinking of their
presence in base. Even though the linked proposals are about a single
type, I think it's important that we come up with a decision and stick
with it. Having different APIs for different types here would be
pretty confusing, and some could even say sloppy.

Please let me know your thoughts.

[1]: https://mail.haskell.org/pipermail/libraries/2019-July/029771.html
[2]: https://gitlab.haskell.org/ghc/ghc/issues/17015
[3]: https://gitlab.haskell.org/ghc/ghc/merge_requests/1704
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries


--
Eric Mertens
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Improving the instances of Data.Functor.{Product,Sum}

Henning Thielemann

On Fri, 13 Mar 2020, chessai . wrote:

> Could you expound on why you try to avoid Flexible{Contexts,Instances}
> in your own code? That might be useful to look at here.

I also try to avoid FlexibleInstances. FlexibleInstances are sometimes a
consequence of multi-parameter type classes with too many parameters. E.g.

    instance Convert Int a
    instance Convert Integer a

which should be better a single-parameter type class on the first
parameter.

FlexibleInstances might indicate too lax instances. E.g.

    instance C (A a) (B a) where

should be better

    isntance (a~b) => C (A a) (B b) where


Sometimes they are a sign of non-composability. E.g.

    instance StringClass String where

should be better

    instance CharClass a => StringClass [a] where

or

    instance (a ~ Char) => StringClass [a] where

depending, on what you need.
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Improving the instances of Data.Functor.{Product,Sum}

Richard Eisenberg-5
In reply to this post by Eric Mertens


On Mar 14, 2020, at 4:14 AM, Eric Mertens <[hidden email]> wrote:

The last thing I'd heard about quantified constraints was that they were buggy and I've been avoiding relying on them. (I should probably review that assumptions at some point.)

Without expressing an opinion about chessai's proposal (which I have not really thought about): quantified constraints are in good shape and ready for prime time. They have limitations (e.g. you can't mention a type family to the right of the =>), but when they are valid, they work well. I'll never swear that a feature is bug-free, but I think it's reasonable to consider using quantified constraints in `base`.

Richard

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Improving the instances of Data.Functor.{Product,Sum}

chessai .
I can second Richard's estimation of QuantifiedConstraints, I have used them a lot in my own code since they were in HEAD. I consider it a sufficiently stable feature to include in base or any library. 

On Sat, Mar 14, 2020, 4:16 AM Richard Eisenberg <[hidden email]> wrote:


On Mar 14, 2020, at 4:14 AM, Eric Mertens <[hidden email]> wrote:

The last thing I'd heard about quantified constraints was that they were buggy and I've been avoiding relying on them. (I should probably review that assumptions at some point.)

Without expressing an opinion about chessai's proposal (which I have not really thought about): quantified constraints are in good shape and ready for prime time. They have limitations (e.g. you can't mention a type family to the right of the =>), but when they are valid, they work well. I'll never swear that a feature is bug-free, but I think it's reasonable to consider using quantified constraints in `base`.

Richard

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Improving the instances of Data.Functor.{Product,Sum}

Oleg Grenrus

QuantifiedConstraints are not buggy, but they are not _complete_
(I do mean that as "buggy" = not sound, properly expressive = complete).

There are at least three issues:

1. Instance definition need UndecidableInstances (in my opinion this is big deal)
2. Instances are not elegant (easy to write, but not elegant).
3. QuantifiedConstraints resists to be abstracted over

See https://gist.github.com/phadej/266d68cf5cc1229c3548b7965f4335f8 for
the standalone code file.

For the reasons below I wouldn't recommend using QuantifiedConstraints.
I very like them, but I'm not convinced the feature is ready for "prime time".
To put into perspective, I think code classes of `singletons` are more ready to
be included in `base` than changing instances of Data.Functor.Sum and .Product.
I do use singletons in my code more than QuantifiedConstraints. :)

I'm very worried how this change will affect libraries like `free` and
`recursion-schemes` and what builds on top of them.
This is not only change to `base`, it strongly guides how downstream
libraries should be written (or changed) as well.

On the other hand, I don't feel strongly about

    instance (Eq (f a), Eq (g a)) => Eq (Product f g a)

Yet, in the light of `free` it is "a step backwards".
See https://hackage.haskell.org/package/free-5/changelog

---

Simple example with `newtype Fix f = Fix (f (Fix f))`

    class Eq1 f where
        liftEq :: (a -> b -> Bool) -> f a -> f b -> Bool
   
    class Eq1 f => Ord1 f where
        liftCompare :: (a -> b -> Ordering) -> f a -> f b -> Ordering

    instance Eq1 f => Eq (Fix f) where
        (==) = eq where eq (Fix x) (Fix y) = liftEq eq x y
   
    instance Ord1 f => Ord (Fix f) where
        compare = cmp where cmp (Fix x) (Fix y) = liftCompare cmp x y

works. It's boilerplate, but it's already written.

However, if we want to use QuantifiedConstraints,
then we

1. need UndecidableInstances
2. and then the code turns out to be less elegant:

instance (forall x. Eq x => Eq (f x)) => Eq (Fix f) where
    (==) = eq where eq (Fix x) (Fix y) = x == y

instance (forall x. Ord x => Ord (f x)) => Ord (Fix f) where
    compare = cmp where cmp (Fix x) (Fix y) = compare x y

fails to compile with

    GHCi, version 8.8.3: https://www.haskell.org/ghc/  :? for help
    [1 of 1] Compiling Main             ( Ord1.hs, interpreted )
   
    Ord1.hs:28:10: error:
        • Could not deduce (Ord x)
            arising from the superclasses of an instance declaration

we need to write Ord instance differently

   instance (forall x. Ord x => Ord (f x), forall x. Eq x => Eq (f x)) => Ord (Fix f) where
       compare = cmp where cmp (Fix x) (Fix y) = compare x y


This _cannot_ be made to work:

    forall x. Ord x => Ord (f x)

doesn't entail

    forall x. Eq x => Eq (f x)

If you try to write defaultLiftEq using liftCompare

    defaultLiftEq :: Ord1 f => (a -> b -> Bool) -> f a -> f b -> Bool
    defaultLiftEq eq x y = EQ == liftCompare _problem_ x y

then you will se a problem.

---

Third issue is that We cannot abstract over QuantifiedConstraints.

Take an example `Dict`. We can use `Dict` for various things.

    data Dict :: (k -> Constraint) -> k -> * where
        Dict :: c a => Dict c a

It nicely uses PolyKinds extension so we can write:

    eqInt :: Dict Eq Int
    eqInt = Dict
   
    eq1List :: Dict Eq1 []
    eq1List = Dict

And we can use Dict to *manually* thread information

    entail :: Dict Ord1 f -> Dict Eq1 f
    entail Dict = Dict

The selling pitch of QuantifiedConstraints, that we could get this for free.
Above Ord (Fix) example however makes me suspicious. Let's try:

    eqQList :: Dict (forall x. Eq x => Eq (f x)) []
    eqQList = undefined

But it doesn't work!

    Ord1.hs:53:28: error:
        • Expected kind ‘(* -> *) -> Constraint’,
            but ‘Eq (f x)’ has kind ‘*’
        • In the first argument of ‘Dict’, namely
            ‘(forall x. Eq x => Eq (f x))’
          In the type signature:
            eqQList :: Dict (forall x. Eq x => Eq (f x)) []
       |
    53 | eqQList :: Dict (forall x. Eq x => Eq (f x)) []
       |
   
    Ord1.hs:53:36: error:
        • Expected a type, but ‘Eq (f x)’ has kind ‘Constraint’
        • In the first argument of ‘Dict’, namely
            ‘(forall x. Eq x => Eq (f x))’
          In the type signature:
            eqQList :: Dict (forall x. Eq x => Eq (f x)) []
       |
    53 | eqQList :: Dict (forall x. Eq x => Eq (f x)) []
       |                                    ^^^^^^^^
   
Then we remember that we have seen that,
we **cannot define** type synonyms for quantified constraints

    type Eq1' f = forall x. Eq x => Eq (f x)

errors with

    Ord1.hs:56:33: error:
        • Expected a type, but ‘Eq (f x)’ has kind ‘Constraint’

Luckily GHC-8.10.1 (which is not released at the moment of writing)
will give us ability to say

    type Eq1' :: (* -> *) -> Constraint
    type Eq1' f = forall x. Eq x => Eq (f x)

This is promising! Let's try to fix eqQList

    eqQList2 :: Dict Eq1' []
    eqQList2 = undefined

But that doesn't work. Type-aliases have to be fully applied!

How in Haskell we fix issues when type-aliases (of classes) need to be partially
evaluated? We defined

    class ... => Example a b c
    instance ... => Example a b c

Third try

    eqQList3 :: Dict Eq1'' f
    eqQList3 = Dict

The type signature is accepted, but the implementation is not

   Ord1.hs:67:12: error:
       • Could not deduce (Eq (f x)) arising from a use of ‘Dict’

At this point I'm clueless.

---

Best regards,
Oleg

P.S. If we would like to take QuantifiedConstraints somewhere into use, then IMO we should start with MonadTrans class. IIRC it's well motivated in the paper. But UndecidableInstances is very unfortunate.

On 14.3.2020 16.10, chessai . wrote:
I can second Richard's estimation of QuantifiedConstraints, I have used them a lot in my own code since they were in HEAD. I consider it a sufficiently stable feature to include in base or any library. 

On Sat, Mar 14, 2020, 4:16 AM Richard Eisenberg <[hidden email]> wrote:


On Mar 14, 2020, at 4:14 AM, Eric Mertens <[hidden email]> wrote:

The last thing I'd heard about quantified constraints was that they were buggy and I've been avoiding relying on them. (I should probably review that assumptions at some point.)

Without expressing an opinion about chessai's proposal (which I have not really thought about): quantified constraints are in good shape and ready for prime time. They have limitations (e.g. you can't mention a type family to the right of the =>), but when they are valid, they work well. I'll never swear that a feature is bug-free, but I think it's reasonable to consider using quantified constraints in `base`.

Richard

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Improving the instances of Data.Functor.{Product,Sum}

Carter Schonwald
as an additional point of data,
is an example of how not trivial a pretty simple use of quantified constraints / related machinery can be!


a good "guiding light" for core libraries in haskell perhaps should be "what choices jointly give the best type inference, composability, generality, performance, and usability" and when we hit a trade off for these parameters, make sure we understand those and have very well understood tradeoffs.

@daniel  for these sorts of instance renovation proposals, its probably best to show case "heres the type  and instance and uses" in each of the K different flavors and what gets better/easier/harder simpler.  I honestly dont do it as often as I should myself!

In this case, putting together a tiny repo with different module doing the various flavors and how they work might be best for grounding this. bonus points if its cabalized so that folks on different lagging rates of ghc versions can poke around :)

(one idea i've been thinking about is how to best make various phases of possibly nontrivial proposals easy to evaluate and compare for impact and benefit, but thats a discussion for another time)

as ever, be well all on this bizarre spring we're all experiencing

-Carter


On Sat, Mar 14, 2020 at 11:44 AM Oleg Grenrus <[hidden email]> wrote:

QuantifiedConstraints are not buggy, but they are not _complete_
(I do mean that as "buggy" = not sound, properly expressive = complete).

There are at least three issues:

1. Instance definition need UndecidableInstances (in my opinion this is big deal)
2. Instances are not elegant (easy to write, but not elegant).
3. QuantifiedConstraints resists to be abstracted over

See https://gist.github.com/phadej/266d68cf5cc1229c3548b7965f4335f8 for
the standalone code file.

For the reasons below I wouldn't recommend using QuantifiedConstraints.
I very like them, but I'm not convinced the feature is ready for "prime time".
To put into perspective, I think code classes of `singletons` are more ready to
be included in `base` than changing instances of Data.Functor.Sum and .Product.
I do use singletons in my code more than QuantifiedConstraints. :)

I'm very worried how this change will affect libraries like `free` and
`recursion-schemes` and what builds on top of them.
This is not only change to `base`, it strongly guides how downstream
libraries should be written (or changed) as well.

On the other hand, I don't feel strongly about

    instance (Eq (f a), Eq (g a)) => Eq (Product f g a)

Yet, in the light of `free` it is "a step backwards".
See https://hackage.haskell.org/package/free-5/changelog

---

Simple example with `newtype Fix f = Fix (f (Fix f))`

    class Eq1 f where
        liftEq :: (a -> b -> Bool) -> f a -> f b -> Bool
   
    class Eq1 f => Ord1 f where
        liftCompare :: (a -> b -> Ordering) -> f a -> f b -> Ordering

    instance Eq1 f => Eq (Fix f) where
        (==) = eq where eq (Fix x) (Fix y) = liftEq eq x y
   
    instance Ord1 f => Ord (Fix f) where
        compare = cmp where cmp (Fix x) (Fix y) = liftCompare cmp x y

works. It's boilerplate, but it's already written.

However, if we want to use QuantifiedConstraints,
then we

1. need UndecidableInstances
2. and then the code turns out to be less elegant:

instance (forall x. Eq x => Eq (f x)) => Eq (Fix f) where
    (==) = eq where eq (Fix x) (Fix y) = x == y

instance (forall x. Ord x => Ord (f x)) => Ord (Fix f) where
    compare = cmp where cmp (Fix x) (Fix y) = compare x y

fails to compile with

    GHCi, version 8.8.3: https://www.haskell.org/ghc/  :? for help
    [1 of 1] Compiling Main             ( Ord1.hs, interpreted )
   
    Ord1.hs:28:10: error:
        • Could not deduce (Ord x)
            arising from the superclasses of an instance declaration

we need to write Ord instance differently

   instance (forall x. Ord x => Ord (f x), forall x. Eq x => Eq (f x)) => Ord (Fix f) where
       compare = cmp where cmp (Fix x) (Fix y) = compare x y


This _cannot_ be made to work:

    forall x. Ord x => Ord (f x)

doesn't entail

    forall x. Eq x => Eq (f x)

If you try to write defaultLiftEq using liftCompare

    defaultLiftEq :: Ord1 f => (a -> b -> Bool) -> f a -> f b -> Bool
    defaultLiftEq eq x y = EQ == liftCompare _problem_ x y

then you will se a problem.

---

Third issue is that We cannot abstract over QuantifiedConstraints.

Take an example `Dict`. We can use `Dict` for various things.

    data Dict :: (k -> Constraint) -> k -> * where
        Dict :: c a => Dict c a

It nicely uses PolyKinds extension so we can write:

    eqInt :: Dict Eq Int
    eqInt = Dict
   
    eq1List :: Dict Eq1 []
    eq1List = Dict

And we can use Dict to *manually* thread information

    entail :: Dict Ord1 f -> Dict Eq1 f
    entail Dict = Dict

The selling pitch of QuantifiedConstraints, that we could get this for free.
Above Ord (Fix) example however makes me suspicious. Let's try:

    eqQList :: Dict (forall x. Eq x => Eq (f x)) []
    eqQList = undefined

But it doesn't work!

    Ord1.hs:53:28: error:
        • Expected kind ‘(* -> *) -> Constraint’,
            but ‘Eq (f x)’ has kind ‘*’
        • In the first argument of ‘Dict’, namely
            ‘(forall x. Eq x => Eq (f x))’
          In the type signature:
            eqQList :: Dict (forall x. Eq x => Eq (f x)) []
       |
    53 | eqQList :: Dict (forall x. Eq x => Eq (f x)) []
       |
   
    Ord1.hs:53:36: error:
        • Expected a type, but ‘Eq (f x)’ has kind ‘Constraint’
        • In the first argument of ‘Dict’, namely
            ‘(forall x. Eq x => Eq (f x))’
          In the type signature:
            eqQList :: Dict (forall x. Eq x => Eq (f x)) []
       |
    53 | eqQList :: Dict (forall x. Eq x => Eq (f x)) []
       |                                    ^^^^^^^^
   
Then we remember that we have seen that,
we **cannot define** type synonyms for quantified constraints

    type Eq1' f = forall x. Eq x => Eq (f x)

errors with

    Ord1.hs:56:33: error:
        • Expected a type, but ‘Eq (f x)’ has kind ‘Constraint’

Luckily GHC-8.10.1 (which is not released at the moment of writing)
will give us ability to say

    type Eq1' :: (* -> *) -> Constraint
    type Eq1' f = forall x. Eq x => Eq (f x)

This is promising! Let's try to fix eqQList

    eqQList2 :: Dict Eq1' []
    eqQList2 = undefined

But that doesn't work. Type-aliases have to be fully applied!

How in Haskell we fix issues when type-aliases (of classes) need to be partially
evaluated? We defined

    class ... => Example a b c
    instance ... => Example a b c

Third try

    eqQList3 :: Dict Eq1'' f
    eqQList3 = Dict

The type signature is accepted, but the implementation is not

   Ord1.hs:67:12: error:
       • Could not deduce (Eq (f x)) arising from a use of ‘Dict’

At this point I'm clueless.

---

Best regards,
Oleg

P.S. If we would like to take QuantifiedConstraints somewhere into use, then IMO we should start with MonadTrans class. IIRC it's well motivated in the paper. But UndecidableInstances is very unfortunate.

On 14.3.2020 16.10, chessai . wrote:
I can second Richard's estimation of QuantifiedConstraints, I have used them a lot in my own code since they were in HEAD. I consider it a sufficiently stable feature to include in base or any library. 

On Sat, Mar 14, 2020, 4:16 AM Richard Eisenberg <[hidden email]> wrote:


On Mar 14, 2020, at 4:14 AM, Eric Mertens <[hidden email]> wrote:

The last thing I'd heard about quantified constraints was that they were buggy and I've been avoiding relying on them. (I should probably review that assumptions at some point.)

Without expressing an opinion about chessai's proposal (which I have not really thought about): quantified constraints are in good shape and ready for prime time. They have limitations (e.g. you can't mention a type family to the right of the =>), but when they are valid, they work well. I'll never swear that a feature is bug-free, but I think it's reasonable to consider using quantified constraints in `base`.

Richard

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Improving the instances of Data.Functor.{Product,Sum}

John Cotton Ericson
Big +1 to fixing these issues.

https://github.com/phadej/some/pull/21 is a PR I'd like to see merged,
but which cannot build because of base shunning flexible instances. We
at Obsidian frequently use `Sum` and `Product` (or when it usually fails
their `Data.Generic` equivalents, `:+:` and `:*:`) with GADTs that are
*not* functors, and anything but the `Flexible*` instances  prevents
that. (Yup, `QuantifiedConstraints` instead of *1 is also no good.)

Do note that none of specific problems with `Flexible*` raised in this
seem to apply in this case (no multi-param type class, no missing `~`,
etc.), only the general wariness. As mentioned, the `Data.Generics` ones
get it the way I want, and I do try to use them accordingly, but if we
can be "right" there why can't we be right here? (And wouldn't it be
nice of one was a newtype or alias of the other...)

If we can all do that, secondarily I would actually like to *keep* the
*1 classes, but give them `QuantifiedConstraints` super-classes:

 > (forall a. Eq (f a)) => Eq1 f

It doesn't look like this has been brought up yet, but the idea is that
one implements a *1 class because of the extra power that the lift*
methods provide----the functionality on the type parameter need not be
canonical---not as a crude hack around the lack of `QuantifiedConstraints`.

I would also advocate writing a `Lift1` for this reason: "shallowly
quoting" a functor of syntax (i.e. `liftLift id`) is quite useful and
very much in the spirit of the lisp quasi-quoting that our quoting and
splicing is based one.

Finally, while the change is breaking, no CPP should be needed and there
is less room for user-error as the new quantified constraint super
classes forces anything which used the old instances to also support the
new instances---you can unthinkingly fix the the type errors and end up
with the right instances for old and new base.

John

P.S. Maybe one might argue that the the new ret-conned use for the *1
classes is much more niche so they belong outside of base. I always like
anything to do with breaking up base, so that's fine with me too. Just
don't say they are altogether useless because of `QuantifiedConstraints`.

On 3/15/20 4:43 PM, Carter Schonwald wrote:

> as an additional point of data,
> https://github.com/ekmett/bytes/pull/49#issuecomment-580924670 and the
> indirectly linked ticket
> https://gitlab.haskell.org/ghc/ghc/issues/17767#note_251123
> is an example of how not trivial a pretty simple use of quantified
> constraints / related machinery can be!
>
>
> a good "guiding light" for core libraries in haskell perhaps should be
> "what choices jointly give the best type inference, composability,
> generality, performance, and usability" and when we hit a trade off
> for these parameters, make sure we understand those and have very well
> understood tradeoffs.
>
> @daniel  for these sorts of instance renovation proposals, its
> probably best to show case "heres the type  and instance and uses" in
> each of the K different flavors and what gets better/easier/harder
> simpler.  I honestly dont do it as often as I should myself!
>
> In this case, putting together a tiny repo with different module doing
> the various flavors and how they work might be best for grounding
> this. bonus points if its cabalized so that folks on different lagging
> rates of ghc versions can poke around :)
>
> (one idea i've been thinking about is how to best make various phases
> of possibly nontrivial proposals easy to evaluate and compare for
> impact and benefit, but thats a discussion for another time)
>
> as ever, be well all on this bizarre spring we're all experiencing
>
> -Carter
>
>
> On Sat, Mar 14, 2020 at 11:44 AM Oleg Grenrus <[hidden email]
> <mailto:[hidden email]>> wrote:
>
>     QuantifiedConstraints are not buggy, but they are not _complete_
>     (I do mean that as "buggy" = not sound, properly expressive =
>     complete).
>
>     There are at least three issues:
>
>     1. Instance definition need UndecidableInstances (in my opinion
>     this is big deal)
>     2. Instances are not elegant (easy to write, but not elegant).
>     3. QuantifiedConstraints resists to be abstracted over
>
>     See
>     https://gist.github.com/phadej/266d68cf5cc1229c3548b7965f4335f8 for
>     the standalone code file.
>
>     For the reasons below I wouldn't recommend using
>     QuantifiedConstraints.
>     I very like them, but I'm not convinced the feature is ready for
>     "prime time".
>     To put into perspective, I think code classes of `singletons` are
>     more ready to
>     be included in `base` than changing instances of Data.Functor.Sum
>     and .Product.
>     I do use singletons in my code more than QuantifiedConstraints. :)
>
>     I'm very worried how this change will affect libraries like `free` and
>     `recursion-schemes` and what builds on top of them.
>     This is not only change to `base`, it strongly guides how downstream
>     libraries should be written (or changed) as well.
>
>     On the other hand, I don't feel strongly about
>
>         instance (Eq (f a), Eq (g a)) => Eq (Product f g a)
>
>     Yet, in the light of `free` it is "a step backwards".
>     See https://hackage.haskell.org/package/free-5/changelog
>
>     ---
>
>     Simple example with `newtype Fix f = Fix (f (Fix f))`
>
>         class Eq1 f where
>             liftEq :: (a -> b -> Bool) -> f a -> f b -> Bool
>
>         class Eq1 f => Ord1 f where
>             liftCompare :: (a -> b -> Ordering) -> f a -> f b -> Ordering
>
>         instance Eq1 f => Eq (Fix f) where
>             (==) = eq where eq (Fix x) (Fix y) = liftEq eq x y
>
>         instance Ord1 f => Ord (Fix f) where
>             compare = cmp where cmp (Fix x) (Fix y) = liftCompare cmp x y
>
>     works. It's boilerplate, but it's already written.
>
>     However, if we want to use QuantifiedConstraints,
>     then we
>
>     1. need UndecidableInstances
>     2. and then the code turns out to be less elegant:
>
>     instance (forall x. Eq x => Eq (f x)) => Eq (Fix f) where
>         (==) = eq where eq (Fix x) (Fix y) = x == y
>
>     instance (forall x. Ord x => Ord (f x)) => Ord (Fix f) where
>         compare = cmp where cmp (Fix x) (Fix y) = compare x y
>
>     fails to compile with
>
>         GHCi, version 8.8.3: https://www.haskell.org/ghc/ :? for help
>         [1 of 1] Compiling Main             ( Ord1.hs, interpreted )
>
>         Ord1.hs:28:10: error:
>             • Could not deduce (Ord x)
>                 arising from the superclasses of an instance declaration
>
>     we need to write Ord instance differently
>
>        instance (forall x. Ord x => Ord (f x), forall x. Eq x => Eq (f
>     x)) => Ord (Fix f) where
>            compare = cmp where cmp (Fix x) (Fix y) = compare x y
>
>
>     This _cannot_ be made to work:
>
>         forall x. Ord x => Ord (f x)
>
>     doesn't entail
>
>         forall x. Eq x => Eq (f x)
>
>     If you try to write defaultLiftEq using liftCompare
>
>         defaultLiftEq :: Ord1 f => (a -> b -> Bool) -> f a -> f b -> Bool
>         defaultLiftEq eq x y = EQ == liftCompare _problem_ x y
>
>     then you will se a problem.
>
>     ---
>
>     Third issue is that We cannot abstract over QuantifiedConstraints.
>
>     Take an example `Dict`. We can use `Dict` for various things.
>
>         data Dict :: (k -> Constraint) -> k -> * where
>             Dict :: c a => Dict c a
>
>     It nicely uses PolyKinds extension so we can write:
>
>         eqInt :: Dict Eq Int
>         eqInt = Dict
>
>         eq1List :: Dict Eq1 []
>         eq1List = Dict
>
>     And we can use Dict to *manually* thread information
>
>         entail :: Dict Ord1 f -> Dict Eq1 f
>         entail Dict = Dict
>
>     The selling pitch of QuantifiedConstraints, that we could get this
>     for free.
>     Above Ord (Fix) example however makes me suspicious. Let's try:
>
>         eqQList :: Dict (forall x. Eq x => Eq (f x)) []
>         eqQList = undefined
>
>     But it doesn't work!
>
>         Ord1.hs:53:28: error:
>             • Expected kind ‘(* -> *) -> Constraint’,
>                 but ‘Eq (f x)’ has kind ‘*’
>             • In the first argument of ‘Dict’, namely
>                 ‘(forall x. Eq x => Eq (f x))’
>               In the type signature:
>                 eqQList :: Dict (forall x. Eq x => Eq (f x)) []
>            |
>         53 | eqQList :: Dict (forall x. Eq x => Eq (f x)) []
>            |
>
>         Ord1.hs:53:36: error:
>             • Expected a type, but ‘Eq (f x)’ has kind ‘Constraint’
>             • In the first argument of ‘Dict’, namely
>                 ‘(forall x. Eq x => Eq (f x))’
>               In the type signature:
>                 eqQList :: Dict (forall x. Eq x => Eq (f x)) []
>            |
>         53 | eqQList :: Dict (forall x. Eq x => Eq (f x)) []
>            |                                    ^^^^^^^^
>
>     Then we remember that we have seen that,
>     we **cannot define** type synonyms for quantified constraints
>
>         type Eq1' f = forall x. Eq x => Eq (f x)
>
>     errors with
>
>         Ord1.hs:56:33: error:
>             • Expected a type, but ‘Eq (f x)’ has kind ‘Constraint’
>
>     Luckily GHC-8.10.1 (which is not released at the moment of writing)
>     will give us ability to say
>
>         type Eq1' :: (* -> *) -> Constraint
>         type Eq1' f = forall x. Eq x => Eq (f x)
>
>     This is promising! Let's try to fix eqQList
>
>         eqQList2 :: Dict Eq1' []
>         eqQList2 = undefined
>
>     But that doesn't work. Type-aliases have to be fully applied!
>
>     How in Haskell we fix issues when type-aliases (of classes) need
>     to be partially
>     evaluated? We defined
>
>         class ... => Example a b c
>         instance ... => Example a b c
>
>     Third try
>
>         eqQList3 :: Dict Eq1'' f
>         eqQList3 = Dict
>
>     The type signature is accepted, but the implementation is not
>
>        Ord1.hs:67:12: error:
>            • Could not deduce (Eq (f x)) arising from a use of ‘Dict’
>
>     At this point I'm clueless.
>
>     ---
>
>     Best regards,
>     Oleg
>
>     P.S. If we would like to take QuantifiedConstraints somewhere into
>     use, then IMO we should start with MonadTrans class. IIRC it's
>     well motivated in the paper. But UndecidableInstances is very
>     unfortunate.
>
>     On 14.3.2020 16.10, chessai . wrote:
>>     I can second Richard's estimation of QuantifiedConstraints, I
>>     have used them a lot in my own code since they were in HEAD. I
>>     consider it a sufficiently stable feature to include in base or
>>     any library.
>>
>>     On Sat, Mar 14, 2020, 4:16 AM Richard Eisenberg <[hidden email]
>>     <mailto:[hidden email]>> wrote:
>>
>>
>>
>>>         On Mar 14, 2020, at 4:14 AM, Eric Mertens
>>>         <[hidden email] <mailto:[hidden email]>> wrote:
>>>
>>>         The last thing I'd heard about quantified constraints was
>>>         that they were buggy and I've been avoiding relying on them.
>>>         (I should probably review that assumptions at some point.)
>>
>>         Without expressing an opinion about chessai's proposal (which
>>         I have not really thought about): quantified constraints are
>>         in good shape and ready for prime time. They have limitations
>>         (e.g. you can't mention a type family to the right of the
>>         =>), but when they are valid, they work well. I'll never
>>         swear that a feature is bug-free, but I think it's reasonable
>>         to consider using quantified constraints in `base`.
>>
>>         Richard
>>
>>
>>     _______________________________________________
>>     Libraries mailing list
>>     [hidden email]  <mailto:[hidden email]>
>>     http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>     _______________________________________________
>     Libraries mailing list
>     [hidden email] <mailto:[hidden email]>
>     http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
>
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Improving the instances of Data.Functor.{Product,Sum}

David Feuer
In reply to this post by Oleg Grenrus
It's been some months, but the last time I messed with quantified constraints I found they didn't work well at all with Coercible.

On Sat, Mar 14, 2020, 11:44 AM Oleg Grenrus <[hidden email]> wrote:

QuantifiedConstraints are not buggy, but they are not _complete_
(I do mean that as "buggy" = not sound, properly expressive = complete).

There are at least three issues:

1. Instance definition need UndecidableInstances (in my opinion this is big deal)
2. Instances are not elegant (easy to write, but not elegant).
3. QuantifiedConstraints resists to be abstracted over

See https://gist.github.com/phadej/266d68cf5cc1229c3548b7965f4335f8 for
the standalone code file.

For the reasons below I wouldn't recommend using QuantifiedConstraints.
I very like them, but I'm not convinced the feature is ready for "prime time".
To put into perspective, I think code classes of `singletons` are more ready to
be included in `base` than changing instances of Data.Functor.Sum and .Product.
I do use singletons in my code more than QuantifiedConstraints. :)

I'm very worried how this change will affect libraries like `free` and
`recursion-schemes` and what builds on top of them.
This is not only change to `base`, it strongly guides how downstream
libraries should be written (or changed) as well.

On the other hand, I don't feel strongly about

    instance (Eq (f a), Eq (g a)) => Eq (Product f g a)

Yet, in the light of `free` it is "a step backwards".
See https://hackage.haskell.org/package/free-5/changelog

---

Simple example with `newtype Fix f = Fix (f (Fix f))`

    class Eq1 f where
        liftEq :: (a -> b -> Bool) -> f a -> f b -> Bool
   
    class Eq1 f => Ord1 f where
        liftCompare :: (a -> b -> Ordering) -> f a -> f b -> Ordering

    instance Eq1 f => Eq (Fix f) where
        (==) = eq where eq (Fix x) (Fix y) = liftEq eq x y
   
    instance Ord1 f => Ord (Fix f) where
        compare = cmp where cmp (Fix x) (Fix y) = liftCompare cmp x y

works. It's boilerplate, but it's already written.

However, if we want to use QuantifiedConstraints,
then we

1. need UndecidableInstances
2. and then the code turns out to be less elegant:

instance (forall x. Eq x => Eq (f x)) => Eq (Fix f) where
    (==) = eq where eq (Fix x) (Fix y) = x == y

instance (forall x. Ord x => Ord (f x)) => Ord (Fix f) where
    compare = cmp where cmp (Fix x) (Fix y) = compare x y

fails to compile with

    GHCi, version 8.8.3: https://www.haskell.org/ghc/  :? for help
    [1 of 1] Compiling Main             ( Ord1.hs, interpreted )
   
    Ord1.hs:28:10: error:
        • Could not deduce (Ord x)
            arising from the superclasses of an instance declaration

we need to write Ord instance differently

   instance (forall x. Ord x => Ord (f x), forall x. Eq x => Eq (f x)) => Ord (Fix f) where
       compare = cmp where cmp (Fix x) (Fix y) = compare x y


This _cannot_ be made to work:

    forall x. Ord x => Ord (f x)

doesn't entail

    forall x. Eq x => Eq (f x)

If you try to write defaultLiftEq using liftCompare

    defaultLiftEq :: Ord1 f => (a -> b -> Bool) -> f a -> f b -> Bool
    defaultLiftEq eq x y = EQ == liftCompare _problem_ x y

then you will se a problem.

---

Third issue is that We cannot abstract over QuantifiedConstraints.

Take an example `Dict`. We can use `Dict` for various things.

    data Dict :: (k -> Constraint) -> k -> * where
        Dict :: c a => Dict c a

It nicely uses PolyKinds extension so we can write:

    eqInt :: Dict Eq Int
    eqInt = Dict
   
    eq1List :: Dict Eq1 []
    eq1List = Dict

And we can use Dict to *manually* thread information

    entail :: Dict Ord1 f -> Dict Eq1 f
    entail Dict = Dict

The selling pitch of QuantifiedConstraints, that we could get this for free.
Above Ord (Fix) example however makes me suspicious. Let's try:

    eqQList :: Dict (forall x. Eq x => Eq (f x)) []
    eqQList = undefined

But it doesn't work!

    Ord1.hs:53:28: error:
        • Expected kind ‘(* -> *) -> Constraint’,
            but ‘Eq (f x)’ has kind ‘*’
        • In the first argument of ‘Dict’, namely
            ‘(forall x. Eq x => Eq (f x))’
          In the type signature:
            eqQList :: Dict (forall x. Eq x => Eq (f x)) []
       |
    53 | eqQList :: Dict (forall x. Eq x => Eq (f x)) []
       |
   
    Ord1.hs:53:36: error:
        • Expected a type, but ‘Eq (f x)’ has kind ‘Constraint’
        • In the first argument of ‘Dict’, namely
            ‘(forall x. Eq x => Eq (f x))’
          In the type signature:
            eqQList :: Dict (forall x. Eq x => Eq (f x)) []
       |
    53 | eqQList :: Dict (forall x. Eq x => Eq (f x)) []
       |                                    ^^^^^^^^
   
Then we remember that we have seen that,
we **cannot define** type synonyms for quantified constraints

    type Eq1' f = forall x. Eq x => Eq (f x)

errors with

    Ord1.hs:56:33: error:
        • Expected a type, but ‘Eq (f x)’ has kind ‘Constraint’

Luckily GHC-8.10.1 (which is not released at the moment of writing)
will give us ability to say

    type Eq1' :: (* -> *) -> Constraint
    type Eq1' f = forall x. Eq x => Eq (f x)

This is promising! Let's try to fix eqQList

    eqQList2 :: Dict Eq1' []
    eqQList2 = undefined

But that doesn't work. Type-aliases have to be fully applied!

How in Haskell we fix issues when type-aliases (of classes) need to be partially
evaluated? We defined

    class ... => Example a b c
    instance ... => Example a b c

Third try

    eqQList3 :: Dict Eq1'' f
    eqQList3 = Dict

The type signature is accepted, but the implementation is not

   Ord1.hs:67:12: error:
       • Could not deduce (Eq (f x)) arising from a use of ‘Dict’

At this point I'm clueless.

---

Best regards,
Oleg

P.S. If we would like to take QuantifiedConstraints somewhere into use, then IMO we should start with MonadTrans class. IIRC it's well motivated in the paper. But UndecidableInstances is very unfortunate.

On 14.3.2020 16.10, chessai . wrote:
I can second Richard's estimation of QuantifiedConstraints, I have used them a lot in my own code since they were in HEAD. I consider it a sufficiently stable feature to include in base or any library. 

On Sat, Mar 14, 2020, 4:16 AM Richard Eisenberg <[hidden email]> wrote:


On Mar 14, 2020, at 4:14 AM, Eric Mertens <[hidden email]> wrote:

The last thing I'd heard about quantified constraints was that they were buggy and I've been avoiding relying on them. (I should probably review that assumptions at some point.)

Without expressing an opinion about chessai's proposal (which I have not really thought about): quantified constraints are in good shape and ready for prime time. They have limitations (e.g. you can't mention a type family to the right of the =>), but when they are valid, they work well. I'll never swear that a feature is bug-free, but I think it's reasonable to consider using quantified constraints in `base`.

Richard

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Improving the instances of Data.Functor.{Product,Sum}

John Cotton Ericson

I think that the problem there is not QuantifiedConstraints, but Coercible (and likewise ~ and ~~) not working well with local constraints of any sort. That's a problem I very much want fixed, but still separate. It should be possible to turn a `Foo => Bar` into a `Dict Foo -> Dict Bar` can get oneself unstuck.

John

On 4/18/20 2:51 PM, David Feuer wrote:
It's been some months, but the last time I messed with quantified constraints I found they didn't work well at all with Coercible.

On Sat, Mar 14, 2020, 11:44 AM Oleg Grenrus <[hidden email]> wrote:

QuantifiedConstraints are not buggy, but they are not _complete_
(I do mean that as "buggy" = not sound, properly expressive = complete).

There are at least three issues:

1. Instance definition need UndecidableInstances (in my opinion this is big deal)
2. Instances are not elegant (easy to write, but not elegant).
3. QuantifiedConstraints resists to be abstracted over

See https://gist.github.com/phadej/266d68cf5cc1229c3548b7965f4335f8 for
the standalone code file.

For the reasons below I wouldn't recommend using QuantifiedConstraints.
I very like them, but I'm not convinced the feature is ready for "prime time".
To put into perspective, I think code classes of `singletons` are more ready to
be included in `base` than changing instances of Data.Functor.Sum and .Product.
I do use singletons in my code more than QuantifiedConstraints. :)

I'm very worried how this change will affect libraries like `free` and
`recursion-schemes` and what builds on top of them.
This is not only change to `base`, it strongly guides how downstream
libraries should be written (or changed) as well.

On the other hand, I don't feel strongly about

    instance (Eq (f a), Eq (g a)) => Eq (Product f g a)

Yet, in the light of `free` it is "a step backwards".
See https://hackage.haskell.org/package/free-5/changelog

---

Simple example with `newtype Fix f = Fix (f (Fix f))`

    class Eq1 f where
        liftEq :: (a -> b -> Bool) -> f a -> f b -> Bool
   
    class Eq1 f => Ord1 f where
        liftCompare :: (a -> b -> Ordering) -> f a -> f b -> Ordering

    instance Eq1 f => Eq (Fix f) where
        (==) = eq where eq (Fix x) (Fix y) = liftEq eq x y
   
    instance Ord1 f => Ord (Fix f) where
        compare = cmp where cmp (Fix x) (Fix y) = liftCompare cmp x y

works. It's boilerplate, but it's already written.

However, if we want to use QuantifiedConstraints,
then we

1. need UndecidableInstances
2. and then the code turns out to be less elegant:

instance (forall x. Eq x => Eq (f x)) => Eq (Fix f) where
    (==) = eq where eq (Fix x) (Fix y) = x == y

instance (forall x. Ord x => Ord (f x)) => Ord (Fix f) where
    compare = cmp where cmp (Fix x) (Fix y) = compare x y

fails to compile with

    GHCi, version 8.8.3: https://www.haskell.org/ghc/  :? for help
    [1 of 1] Compiling Main             ( Ord1.hs, interpreted )
   
    Ord1.hs:28:10: error:
        • Could not deduce (Ord x)
            arising from the superclasses of an instance declaration

we need to write Ord instance differently

   instance (forall x. Ord x => Ord (f x), forall x. Eq x => Eq (f x)) => Ord (Fix f) where
       compare = cmp where cmp (Fix x) (Fix y) = compare x y


This _cannot_ be made to work:

    forall x. Ord x => Ord (f x)

doesn't entail

    forall x. Eq x => Eq (f x)

If you try to write defaultLiftEq using liftCompare

    defaultLiftEq :: Ord1 f => (a -> b -> Bool) -> f a -> f b -> Bool
    defaultLiftEq eq x y = EQ == liftCompare _problem_ x y

then you will se a problem.

---

Third issue is that We cannot abstract over QuantifiedConstraints.

Take an example `Dict`. We can use `Dict` for various things.

    data Dict :: (k -> Constraint) -> k -> * where
        Dict :: c a => Dict c a

It nicely uses PolyKinds extension so we can write:

    eqInt :: Dict Eq Int
    eqInt = Dict
   
    eq1List :: Dict Eq1 []
    eq1List = Dict

And we can use Dict to *manually* thread information

    entail :: Dict Ord1 f -> Dict Eq1 f
    entail Dict = Dict

The selling pitch of QuantifiedConstraints, that we could get this for free.
Above Ord (Fix) example however makes me suspicious. Let's try:

    eqQList :: Dict (forall x. Eq x => Eq (f x)) []
    eqQList = undefined

But it doesn't work!

    Ord1.hs:53:28: error:
        • Expected kind ‘(* -> *) -> Constraint’,
            but ‘Eq (f x)’ has kind ‘*’
        • In the first argument of ‘Dict’, namely
            ‘(forall x. Eq x => Eq (f x))’
          In the type signature:
            eqQList :: Dict (forall x. Eq x => Eq (f x)) []
       |
    53 | eqQList :: Dict (forall x. Eq x => Eq (f x)) []
       |
   
    Ord1.hs:53:36: error:
        • Expected a type, but ‘Eq (f x)’ has kind ‘Constraint’
        • In the first argument of ‘Dict’, namely
            ‘(forall x. Eq x => Eq (f x))’
          In the type signature:
            eqQList :: Dict (forall x. Eq x => Eq (f x)) []
       |
    53 | eqQList :: Dict (forall x. Eq x => Eq (f x)) []
       |                                    ^^^^^^^^
   
Then we remember that we have seen that,
we **cannot define** type synonyms for quantified constraints

    type Eq1' f = forall x. Eq x => Eq (f x)

errors with

    Ord1.hs:56:33: error:
        • Expected a type, but ‘Eq (f x)’ has kind ‘Constraint’

Luckily GHC-8.10.1 (which is not released at the moment of writing)
will give us ability to say

    type Eq1' :: (* -> *) -> Constraint
    type Eq1' f = forall x. Eq x => Eq (f x)

This is promising! Let's try to fix eqQList

    eqQList2 :: Dict Eq1' []
    eqQList2 = undefined

But that doesn't work. Type-aliases have to be fully applied!

How in Haskell we fix issues when type-aliases (of classes) need to be partially
evaluated? We defined

    class ... => Example a b c
    instance ... => Example a b c

Third try

    eqQList3 :: Dict Eq1'' f
    eqQList3 = Dict

The type signature is accepted, but the implementation is not

   Ord1.hs:67:12: error:
       • Could not deduce (Eq (f x)) arising from a use of ‘Dict’

At this point I'm clueless.

---

Best regards,
Oleg

P.S. If we would like to take QuantifiedConstraints somewhere into use, then IMO we should start with MonadTrans class. IIRC it's well motivated in the paper. But UndecidableInstances is very unfortunate.

On 14.3.2020 16.10, chessai . wrote:
I can second Richard's estimation of QuantifiedConstraints, I have used them a lot in my own code since they were in HEAD. I consider it a sufficiently stable feature to include in base or any library. 

On Sat, Mar 14, 2020, 4:16 AM Richard Eisenberg <[hidden email]> wrote:


On Mar 14, 2020, at 4:14 AM, Eric Mertens <[hidden email]> wrote:

The last thing I'd heard about quantified constraints was that they were buggy and I've been avoiding relying on them. (I should probably review that assumptions at some point.)

Without expressing an opinion about chessai's proposal (which I have not really thought about): quantified constraints are in good shape and ready for prime time. They have limitations (e.g. you can't mention a type family to the right of the =>), but when they are valid, they work well. I'll never swear that a feature is bug-free, but I think it's reasonable to consider using quantified constraints in `base`.

Richard

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Improving the instances of Data.Functor.{Product,Sum}

David Feuer
That's definitely part of the problem, but the way QuantifiedConstraints leads to local overlap is also generally troubling.

On Mon, Apr 20, 2020, 9:44 PM John Ericson <[hidden email]> wrote:

I think that the problem there is not QuantifiedConstraints, but Coercible (and likewise ~ and ~~) not working well with local constraints of any sort. That's a problem I very much want fixed, but still separate. It should be possible to turn a `Foo => Bar` into a `Dict Foo -> Dict Bar` can get oneself unstuck.

John

On 4/18/20 2:51 PM, David Feuer wrote:
It's been some months, but the last time I messed with quantified constraints I found they didn't work well at all with Coercible.

On Sat, Mar 14, 2020, 11:44 AM Oleg Grenrus <[hidden email]> wrote:

QuantifiedConstraints are not buggy, but they are not _complete_
(I do mean that as "buggy" = not sound, properly expressive = complete).

There are at least three issues:

1. Instance definition need UndecidableInstances (in my opinion this is big deal)
2. Instances are not elegant (easy to write, but not elegant).
3. QuantifiedConstraints resists to be abstracted over

See https://gist.github.com/phadej/266d68cf5cc1229c3548b7965f4335f8 for
the standalone code file.

For the reasons below I wouldn't recommend using QuantifiedConstraints.
I very like them, but I'm not convinced the feature is ready for "prime time".
To put into perspective, I think code classes of `singletons` are more ready to
be included in `base` than changing instances of Data.Functor.Sum and .Product.
I do use singletons in my code more than QuantifiedConstraints. :)

I'm very worried how this change will affect libraries like `free` and
`recursion-schemes` and what builds on top of them.
This is not only change to `base`, it strongly guides how downstream
libraries should be written (or changed) as well.

On the other hand, I don't feel strongly about

    instance (Eq (f a), Eq (g a)) => Eq (Product f g a)

Yet, in the light of `free` it is "a step backwards".
See https://hackage.haskell.org/package/free-5/changelog

---

Simple example with `newtype Fix f = Fix (f (Fix f))`

    class Eq1 f where
        liftEq :: (a -> b -> Bool) -> f a -> f b -> Bool
   
    class Eq1 f => Ord1 f where
        liftCompare :: (a -> b -> Ordering) -> f a -> f b -> Ordering

    instance Eq1 f => Eq (Fix f) where
        (==) = eq where eq (Fix x) (Fix y) = liftEq eq x y
   
    instance Ord1 f => Ord (Fix f) where
        compare = cmp where cmp (Fix x) (Fix y) = liftCompare cmp x y

works. It's boilerplate, but it's already written.

However, if we want to use QuantifiedConstraints,
then we

1. need UndecidableInstances
2. and then the code turns out to be less elegant:

instance (forall x. Eq x => Eq (f x)) => Eq (Fix f) where
    (==) = eq where eq (Fix x) (Fix y) = x == y

instance (forall x. Ord x => Ord (f x)) => Ord (Fix f) where
    compare = cmp where cmp (Fix x) (Fix y) = compare x y

fails to compile with

    GHCi, version 8.8.3: https://www.haskell.org/ghc/  :? for help
    [1 of 1] Compiling Main             ( Ord1.hs, interpreted )
   
    Ord1.hs:28:10: error:
        • Could not deduce (Ord x)
            arising from the superclasses of an instance declaration

we need to write Ord instance differently

   instance (forall x. Ord x => Ord (f x), forall x. Eq x => Eq (f x)) => Ord (Fix f) where
       compare = cmp where cmp (Fix x) (Fix y) = compare x y


This _cannot_ be made to work:

    forall x. Ord x => Ord (f x)

doesn't entail

    forall x. Eq x => Eq (f x)

If you try to write defaultLiftEq using liftCompare

    defaultLiftEq :: Ord1 f => (a -> b -> Bool) -> f a -> f b -> Bool
    defaultLiftEq eq x y = EQ == liftCompare _problem_ x y

then you will se a problem.

---

Third issue is that We cannot abstract over QuantifiedConstraints.

Take an example `Dict`. We can use `Dict` for various things.

    data Dict :: (k -> Constraint) -> k -> * where
        Dict :: c a => Dict c a

It nicely uses PolyKinds extension so we can write:

    eqInt :: Dict Eq Int
    eqInt = Dict
   
    eq1List :: Dict Eq1 []
    eq1List = Dict

And we can use Dict to *manually* thread information

    entail :: Dict Ord1 f -> Dict Eq1 f
    entail Dict = Dict

The selling pitch of QuantifiedConstraints, that we could get this for free.
Above Ord (Fix) example however makes me suspicious. Let's try:

    eqQList :: Dict (forall x. Eq x => Eq (f x)) []
    eqQList = undefined

But it doesn't work!

    Ord1.hs:53:28: error:
        • Expected kind ‘(* -> *) -> Constraint’,
            but ‘Eq (f x)’ has kind ‘*’
        • In the first argument of ‘Dict’, namely
            ‘(forall x. Eq x => Eq (f x))’
          In the type signature:
            eqQList :: Dict (forall x. Eq x => Eq (f x)) []
       |
    53 | eqQList :: Dict (forall x. Eq x => Eq (f x)) []
       |
   
    Ord1.hs:53:36: error:
        • Expected a type, but ‘Eq (f x)’ has kind ‘Constraint’
        • In the first argument of ‘Dict’, namely
            ‘(forall x. Eq x => Eq (f x))’
          In the type signature:
            eqQList :: Dict (forall x. Eq x => Eq (f x)) []
       |
    53 | eqQList :: Dict (forall x. Eq x => Eq (f x)) []
       |                                    ^^^^^^^^
   
Then we remember that we have seen that,
we **cannot define** type synonyms for quantified constraints

    type Eq1' f = forall x. Eq x => Eq (f x)

errors with

    Ord1.hs:56:33: error:
        • Expected a type, but ‘Eq (f x)’ has kind ‘Constraint’

Luckily GHC-8.10.1 (which is not released at the moment of writing)
will give us ability to say

    type Eq1' :: (* -> *) -> Constraint
    type Eq1' f = forall x. Eq x => Eq (f x)

This is promising! Let's try to fix eqQList

    eqQList2 :: Dict Eq1' []
    eqQList2 = undefined

But that doesn't work. Type-aliases have to be fully applied!

How in Haskell we fix issues when type-aliases (of classes) need to be partially
evaluated? We defined

    class ... => Example a b c
    instance ... => Example a b c

Third try

    eqQList3 :: Dict Eq1'' f
    eqQList3 = Dict

The type signature is accepted, but the implementation is not

   Ord1.hs:67:12: error:
       • Could not deduce (Eq (f x)) arising from a use of ‘Dict’

At this point I'm clueless.

---

Best regards,
Oleg

P.S. If we would like to take QuantifiedConstraints somewhere into use, then IMO we should start with MonadTrans class. IIRC it's well motivated in the paper. But UndecidableInstances is very unfortunate.

On 14.3.2020 16.10, chessai . wrote:
I can second Richard's estimation of QuantifiedConstraints, I have used them a lot in my own code since they were in HEAD. I consider it a sufficiently stable feature to include in base or any library. 

On Sat, Mar 14, 2020, 4:16 AM Richard Eisenberg <[hidden email]> wrote:


On Mar 14, 2020, at 4:14 AM, Eric Mertens <[hidden email]> wrote:

The last thing I'd heard about quantified constraints was that they were buggy and I've been avoiding relying on them. (I should probably review that assumptions at some point.)

Without expressing an opinion about chessai's proposal (which I have not really thought about): quantified constraints are in good shape and ready for prime time. They have limitations (e.g. you can't mention a type family to the right of the =>), but when they are valid, they work well. I'll never swear that a feature is bug-free, but I think it's reasonable to consider using quantified constraints in `base`.

Richard

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Improving the instances of Data.Functor.{Product,Sum}

John Cotton Ericson

Yes there is that. If you (or anyone else is) curious, https://gitlab.haskell.org/ghc/ghc/issues/17295 discusses this a bit. In the last comment I wonder whether `Note [Instance and Given overlap]` is really about quantified vs non-quantified, rather than local and global, and just conflates the two because it dates back to the introduction of OutsideIn when there were no local givens with implication.

On 4/20/20 9:47 PM, David Feuer wrote:
That's definitely part of the problem, but the way QuantifiedConstraints leads to local overlap is also generally troubling.

On Mon, Apr 20, 2020, 9:44 PM John Ericson [hidden email] wrote:

I think that the problem there is not QuantifiedConstraints, but Coercible (and likewise ~ and ~~) not working well with local constraints of any sort. That's a problem I very much want fixed, but still separate. It should be possible to turn a `Foo => Bar` into a `Dict Foo -> Dict Bar` can get oneself unstuck.

John

On 4/18/20 2:51 PM, David Feuer wrote:
It's been some months, but the last time I messed with quantified constraints I found they didn't work well at all with Coercible.

On Sat, Mar 14, 2020, 11:44 AM Oleg Grenrus <[hidden email]> wrote:

QuantifiedConstraints are not buggy, but they are not _complete_
(I do mean that as "buggy" = not sound, properly expressive = complete).

There are at least three issues:

1. Instance definition need UndecidableInstances (in my opinion this is big deal)
2. Instances are not elegant (easy to write, but not elegant).
3. QuantifiedConstraints resists to be abstracted over

See https://gist.github.com/phadej/266d68cf5cc1229c3548b7965f4335f8 for
the standalone code file.

For the reasons below I wouldn't recommend using QuantifiedConstraints.
I very like them, but I'm not convinced the feature is ready for "prime time".
To put into perspective, I think code classes of `singletons` are more ready to
be included in `base` than changing instances of Data.Functor.Sum and .Product.
I do use singletons in my code more than QuantifiedConstraints. :)

I'm very worried how this change will affect libraries like `free` and
`recursion-schemes` and what builds on top of them.
This is not only change to `base`, it strongly guides how downstream
libraries should be written (or changed) as well.

On the other hand, I don't feel strongly about

    instance (Eq (f a), Eq (g a)) => Eq (Product f g a)

Yet, in the light of `free` it is "a step backwards".
See https://hackage.haskell.org/package/free-5/changelog

---

Simple example with `newtype Fix f = Fix (f (Fix f))`

    class Eq1 f where
        liftEq :: (a -> b -> Bool) -> f a -> f b -> Bool
   
    class Eq1 f => Ord1 f where
        liftCompare :: (a -> b -> Ordering) -> f a -> f b -> Ordering

    instance Eq1 f => Eq (Fix f) where
        (==) = eq where eq (Fix x) (Fix y) = liftEq eq x y
   
    instance Ord1 f => Ord (Fix f) where
        compare = cmp where cmp (Fix x) (Fix y) = liftCompare cmp x y

works. It's boilerplate, but it's already written.

However, if we want to use QuantifiedConstraints,
then we

1. need UndecidableInstances
2. and then the code turns out to be less elegant:

instance (forall x. Eq x => Eq (f x)) => Eq (Fix f) where
    (==) = eq where eq (Fix x) (Fix y) = x == y

instance (forall x. Ord x => Ord (f x)) => Ord (Fix f) where
    compare = cmp where cmp (Fix x) (Fix y) = compare x y

fails to compile with

    GHCi, version 8.8.3: https://www.haskell.org/ghc/  :? for help
    [1 of 1] Compiling Main             ( Ord1.hs, interpreted )
   
    Ord1.hs:28:10: error:
        • Could not deduce (Ord x)
            arising from the superclasses of an instance declaration

we need to write Ord instance differently

   instance (forall x. Ord x => Ord (f x), forall x. Eq x => Eq (f x)) => Ord (Fix f) where
       compare = cmp where cmp (Fix x) (Fix y) = compare x y


This _cannot_ be made to work:

    forall x. Ord x => Ord (f x)

doesn't entail

    forall x. Eq x => Eq (f x)

If you try to write defaultLiftEq using liftCompare

    defaultLiftEq :: Ord1 f => (a -> b -> Bool) -> f a -> f b -> Bool
    defaultLiftEq eq x y = EQ == liftCompare _problem_ x y

then you will se a problem.

---

Third issue is that We cannot abstract over QuantifiedConstraints.

Take an example `Dict`. We can use `Dict` for various things.

    data Dict :: (k -> Constraint) -> k -> * where
        Dict :: c a => Dict c a

It nicely uses PolyKinds extension so we can write:

    eqInt :: Dict Eq Int
    eqInt = Dict
   
    eq1List :: Dict Eq1 []
    eq1List = Dict

And we can use Dict to *manually* thread information

    entail :: Dict Ord1 f -> Dict Eq1 f
    entail Dict = Dict

The selling pitch of QuantifiedConstraints, that we could get this for free.
Above Ord (Fix) example however makes me suspicious. Let's try:

    eqQList :: Dict (forall x. Eq x => Eq (f x)) []
    eqQList = undefined

But it doesn't work!

    Ord1.hs:53:28: error:
        • Expected kind ‘(* -> *) -> Constraint’,
            but ‘Eq (f x)’ has kind ‘*’
        • In the first argument of ‘Dict’, namely
            ‘(forall x. Eq x => Eq (f x))’
          In the type signature:
            eqQList :: Dict (forall x. Eq x => Eq (f x)) []
       |
    53 | eqQList :: Dict (forall x. Eq x => Eq (f x)) []
       |
   
    Ord1.hs:53:36: error:
        • Expected a type, but ‘Eq (f x)’ has kind ‘Constraint’
        • In the first argument of ‘Dict’, namely
            ‘(forall x. Eq x => Eq (f x))’
          In the type signature:
            eqQList :: Dict (forall x. Eq x => Eq (f x)) []
       |
    53 | eqQList :: Dict (forall x. Eq x => Eq (f x)) []
       |                                    ^^^^^^^^
   
Then we remember that we have seen that,
we **cannot define** type synonyms for quantified constraints

    type Eq1' f = forall x. Eq x => Eq (f x)

errors with

    Ord1.hs:56:33: error:
        • Expected a type, but ‘Eq (f x)’ has kind ‘Constraint’

Luckily GHC-8.10.1 (which is not released at the moment of writing)
will give us ability to say

    type Eq1' :: (* -> *) -> Constraint
    type Eq1' f = forall x. Eq x => Eq (f x)

This is promising! Let's try to fix eqQList

    eqQList2 :: Dict Eq1' []
    eqQList2 = undefined

But that doesn't work. Type-aliases have to be fully applied!

How in Haskell we fix issues when type-aliases (of classes) need to be partially
evaluated? We defined

    class ... => Example a b c
    instance ... => Example a b c

Third try

    eqQList3 :: Dict Eq1'' f
    eqQList3 = Dict

The type signature is accepted, but the implementation is not

   Ord1.hs:67:12: error:
       • Could not deduce (Eq (f x)) arising from a use of ‘Dict’

At this point I'm clueless.

---

Best regards,
Oleg

P.S. If we would like to take QuantifiedConstraints somewhere into use, then IMO we should start with MonadTrans class. IIRC it's well motivated in the paper. But UndecidableInstances is very unfortunate.

On 14.3.2020 16.10, chessai . wrote:
I can second Richard's estimation of QuantifiedConstraints, I have used them a lot in my own code since they were in HEAD. I consider it a sufficiently stable feature to include in base or any library. 

On Sat, Mar 14, 2020, 4:16 AM Richard Eisenberg <[hidden email]> wrote:


On Mar 14, 2020, at 4:14 AM, Eric Mertens <[hidden email]> wrote:

The last thing I'd heard about quantified constraints was that they were buggy and I've been avoiding relying on them. (I should probably review that assumptions at some point.)

Without expressing an opinion about chessai's proposal (which I have not really thought about): quantified constraints are in good shape and ready for prime time. They have limitations (e.g. you can't mention a type family to the right of the =>), but when they are valid, they work well. I'll never swear that a feature is bug-free, but I think it's reasonable to consider using quantified constraints in `base`.

Richard

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Improving the instances of Data.Functor.{Product,Sum}

David Feuer
In reply to this post by chessai .
I oppose the QuantifiedConstraints version because:

1. It is more complicated than the FlexibleConstraints one.

2. It is strictly less general than the FlexibleConstraints one.

3. There is no apparent benefit to pay for detriments 1 and 2.

On Fri, Mar 13, 2020, 11:59 PM chessai . <[hidden email]> wrote:
Consider the Eq instance for these types. Currently we rely on:

(Eq1 f, Eq1 g, Eq a)

But some potential improvements include changing to:

(Eq (f (g a))) (FlexibleContexts)

or

(forall x. Eq x => Eq (f x), forall x. Eq x => Eq (g x), Eq a)
(QuantifiedConstraints)

There was a discussion sometime last year about the same thing
regarding Semigroup/Monoid instances for `Compose` [1]. Additionally,
the question has been raised again for Data.Functor.{Product,Sum} on
Gitlab [2, 3]. There has been no consensus in either case, but that's
not too worrying as both discussions have been brief. I'm currently
not happy with the {Eq,Ord,Show}{1,2} family of classes, and would
hope to work toward their removal, or at least the shrinking of their
presence in base. Even though the linked proposals are about a single
type, I think it's important that we come up with a decision and stick
with it. Having different APIs for different types here would be
pretty confusing, and some could even say sloppy.

Please let me know your thoughts.

[1]: https://mail.haskell.org/pipermail/libraries/2019-July/029771.html
[2]: https://gitlab.haskell.org/ghc/ghc/issues/17015
[3]: https://gitlab.haskell.org/ghc/ghc/merge_requests/1704
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Improving the instances of Data.Functor.{Product,Sum}

Andrew Martin
I dislike the FlexibleContexts approach because it gives you constraints that do not compose. Consider this minimal example:

    foo :: _ => a -> a -> Bool
    foo x y = Compose (Just (Just x)) == Compose (Just (Just y)) && Compose [Just x] == Compose [Just y]

What do we expect the constraint to be? With the Eq1 machinery or with QuantifiedConstraints, it's `Eq a` (GHC will infer this). However, with FlexibleContexts, it's `(Eq (Compose Maybe Maybe a), Eq (Compose [] Maybe a)`.

On Tue, May 5, 2020 at 12:45 PM David Feuer <[hidden email]> wrote:
I oppose the QuantifiedConstraints version because:

1. It is more complicated than the FlexibleConstraints one.

2. It is strictly less general than the FlexibleConstraints one.

3. There is no apparent benefit to pay for detriments 1 and 2.

On Fri, Mar 13, 2020, 11:59 PM chessai . <[hidden email]> wrote:
Consider the Eq instance for these types. Currently we rely on:

(Eq1 f, Eq1 g, Eq a)

But some potential improvements include changing to:

(Eq (f (g a))) (FlexibleContexts)

or

(forall x. Eq x => Eq (f x), forall x. Eq x => Eq (g x), Eq a)
(QuantifiedConstraints)

There was a discussion sometime last year about the same thing
regarding Semigroup/Monoid instances for `Compose` [1]. Additionally,
the question has been raised again for Data.Functor.{Product,Sum} on
Gitlab [2, 3]. There has been no consensus in either case, but that's
not too worrying as both discussions have been brief. I'm currently
not happy with the {Eq,Ord,Show}{1,2} family of classes, and would
hope to work toward their removal, or at least the shrinking of their
presence in base. Even though the linked proposals are about a single
type, I think it's important that we come up with a decision and stick
with it. Having different APIs for different types here would be
pretty confusing, and some could even say sloppy.

Please let me know your thoughts.

[1]: https://mail.haskell.org/pipermail/libraries/2019-July/029771.html
[2]: https://gitlab.haskell.org/ghc/ghc/issues/17015
[3]: https://gitlab.haskell.org/ghc/ghc/merge_requests/1704
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries


--
-Andrew Thaddeus Martin

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Improving the instances of Data.Functor.{Product,Sum}

David Feuer
Why is that a problem? `Eq a` is still sufficient.

On Tue, May 5, 2020, 1:51 PM Andrew Martin <[hidden email]> wrote:
I dislike the FlexibleContexts approach because it gives you constraints that do not compose. Consider this minimal example:

    foo :: _ => a -> a -> Bool
    foo x y = Compose (Just (Just x)) == Compose (Just (Just y)) && Compose [Just x] == Compose [Just y]

What do we expect the constraint to be? With the Eq1 machinery or with QuantifiedConstraints, it's `Eq a` (GHC will infer this). However, with FlexibleContexts, it's `(Eq (Compose Maybe Maybe a), Eq (Compose [] Maybe a)`.

On Tue, May 5, 2020 at 12:45 PM David Feuer <[hidden email]> wrote:
I oppose the QuantifiedConstraints version because:

1. It is more complicated than the FlexibleConstraints one.

2. It is strictly less general than the FlexibleConstraints one.

3. There is no apparent benefit to pay for detriments 1 and 2.

On Fri, Mar 13, 2020, 11:59 PM chessai . <[hidden email]> wrote:
Consider the Eq instance for these types. Currently we rely on:

(Eq1 f, Eq1 g, Eq a)

But some potential improvements include changing to:

(Eq (f (g a))) (FlexibleContexts)

or

(forall x. Eq x => Eq (f x), forall x. Eq x => Eq (g x), Eq a)
(QuantifiedConstraints)

There was a discussion sometime last year about the same thing
regarding Semigroup/Monoid instances for `Compose` [1]. Additionally,
the question has been raised again for Data.Functor.{Product,Sum} on
Gitlab [2, 3]. There has been no consensus in either case, but that's
not too worrying as both discussions have been brief. I'm currently
not happy with the {Eq,Ord,Show}{1,2} family of classes, and would
hope to work toward their removal, or at least the shrinking of their
presence in base. Even though the linked proposals are about a single
type, I think it's important that we come up with a decision and stick
with it. Having different APIs for different types here would be
pretty confusing, and some could even say sloppy.

Please let me know your thoughts.

[1]: https://mail.haskell.org/pipermail/libraries/2019-July/029771.html
[2]: https://gitlab.haskell.org/ghc/ghc/issues/17015
[3]: https://gitlab.haskell.org/ghc/ghc/merge_requests/1704
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries


--
-Andrew Thaddeus Martin

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Improving the instances of Data.Functor.{Product,Sum}

Andrew Martin
You're right. I botched that. The scenario I meant to describe was:

    foo :: _ => f a -> f a -> Bool
    foo x y = Compose (Just x) == Compose (Just y) && Compose [x] == Compose [y]

The different results are:
* FlexibleContexts approach: `(Eq (Maybe (f a)), Eq [f a])`
* Eq1 typeclass: `(Eq1 f, Eq a)`
* Quantified Constraints: `(forall x. Eq x => Eq (f x), Eq a)`

Only the FlexibleContexts approach mentions Maybe and [] in the constraints.

On Tue, May 5, 2020 at 1:56 PM David Feuer <[hidden email]> wrote:
Why is that a problem? `Eq a` is still sufficient.

On Tue, May 5, 2020, 1:51 PM Andrew Martin <[hidden email]> wrote:
I dislike the FlexibleContexts approach because it gives you constraints that do not compose. Consider this minimal example:

    foo :: _ => a -> a -> Bool
    foo x y = Compose (Just (Just x)) == Compose (Just (Just y)) && Compose [Just x] == Compose [Just y]

What do we expect the constraint to be? With the Eq1 machinery or with QuantifiedConstraints, it's `Eq a` (GHC will infer this). However, with FlexibleContexts, it's `(Eq (Compose Maybe Maybe a), Eq (Compose [] Maybe a)`.

On Tue, May 5, 2020 at 12:45 PM David Feuer <[hidden email]> wrote:
I oppose the QuantifiedConstraints version because:

1. It is more complicated than the FlexibleConstraints one.

2. It is strictly less general than the FlexibleConstraints one.

3. There is no apparent benefit to pay for detriments 1 and 2.

On Fri, Mar 13, 2020, 11:59 PM chessai . <[hidden email]> wrote:
Consider the Eq instance for these types. Currently we rely on:

(Eq1 f, Eq1 g, Eq a)

But some potential improvements include changing to:

(Eq (f (g a))) (FlexibleContexts)

or

(forall x. Eq x => Eq (f x), forall x. Eq x => Eq (g x), Eq a)
(QuantifiedConstraints)

There was a discussion sometime last year about the same thing
regarding Semigroup/Monoid instances for `Compose` [1]. Additionally,
the question has been raised again for Data.Functor.{Product,Sum} on
Gitlab [2, 3]. There has been no consensus in either case, but that's
not too worrying as both discussions have been brief. I'm currently
not happy with the {Eq,Ord,Show}{1,2} family of classes, and would
hope to work toward their removal, or at least the shrinking of their
presence in base. Even though the linked proposals are about a single
type, I think it's important that we come up with a decision and stick
with it. Having different APIs for different types here would be
pretty confusing, and some could even say sloppy.

Please let me know your thoughts.

[1]: https://mail.haskell.org/pipermail/libraries/2019-July/029771.html
[2]: https://gitlab.haskell.org/ghc/ghc/issues/17015
[3]: https://gitlab.haskell.org/ghc/ghc/merge_requests/1704
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries


--
-Andrew Thaddeus Martin


--
-Andrew Thaddeus Martin

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Improving the instances of Data.Functor.{Product,Sum}

David Feuer
Okay, but I still don't see the practical problem.

On Tue, May 5, 2020, 2:05 PM Andrew Martin <[hidden email]> wrote:
You're right. I botched that. The scenario I meant to describe was:

    foo :: _ => f a -> f a -> Bool
    foo x y = Compose (Just x) == Compose (Just y) && Compose [x] == Compose [y]

The different results are:
* FlexibleContexts approach: `(Eq (Maybe (f a)), Eq [f a])`
* Eq1 typeclass: `(Eq1 f, Eq a)`
* Quantified Constraints: `(forall x. Eq x => Eq (f x), Eq a)`

Only the FlexibleContexts approach mentions Maybe and [] in the constraints.

On Tue, May 5, 2020 at 1:56 PM David Feuer <[hidden email]> wrote:
Why is that a problem? `Eq a` is still sufficient.

On Tue, May 5, 2020, 1:51 PM Andrew Martin <[hidden email]> wrote:
I dislike the FlexibleContexts approach because it gives you constraints that do not compose. Consider this minimal example:

    foo :: _ => a -> a -> Bool
    foo x y = Compose (Just (Just x)) == Compose (Just (Just y)) && Compose [Just x] == Compose [Just y]

What do we expect the constraint to be? With the Eq1 machinery or with QuantifiedConstraints, it's `Eq a` (GHC will infer this). However, with FlexibleContexts, it's `(Eq (Compose Maybe Maybe a), Eq (Compose [] Maybe a)`.

On Tue, May 5, 2020 at 12:45 PM David Feuer <[hidden email]> wrote:
I oppose the QuantifiedConstraints version because:

1. It is more complicated than the FlexibleConstraints one.

2. It is strictly less general than the FlexibleConstraints one.

3. There is no apparent benefit to pay for detriments 1 and 2.

On Fri, Mar 13, 2020, 11:59 PM chessai . <[hidden email]> wrote:
Consider the Eq instance for these types. Currently we rely on:

(Eq1 f, Eq1 g, Eq a)

But some potential improvements include changing to:

(Eq (f (g a))) (FlexibleContexts)

or

(forall x. Eq x => Eq (f x), forall x. Eq x => Eq (g x), Eq a)
(QuantifiedConstraints)

There was a discussion sometime last year about the same thing
regarding Semigroup/Monoid instances for `Compose` [1]. Additionally,
the question has been raised again for Data.Functor.{Product,Sum} on
Gitlab [2, 3]. There has been no consensus in either case, but that's
not too worrying as both discussions have been brief. I'm currently
not happy with the {Eq,Ord,Show}{1,2} family of classes, and would
hope to work toward their removal, or at least the shrinking of their
presence in base. Even though the linked proposals are about a single
type, I think it's important that we come up with a decision and stick
with it. Having different APIs for different types here would be
pretty confusing, and some could even say sloppy.

Please let me know your thoughts.

[1]: https://mail.haskell.org/pipermail/libraries/2019-July/029771.html
[2]: https://gitlab.haskell.org/ghc/ghc/issues/17015
[3]: https://gitlab.haskell.org/ghc/ghc/merge_requests/1704
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries


--
-Andrew Thaddeus Martin


--
-Andrew Thaddeus Martin

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Improving the instances of Data.Functor.{Product,Sum}

Carter Schonwald
I think we should pre address any maturity issues or composition/ generality concerns before folding quantified constraint  instances into base 

On Tue, May 5, 2020 at 2:08 PM David Feuer <[hidden email]> wrote:
Okay, but I still don't see the practical problem.

On Tue, May 5, 2020, 2:05 PM Andrew Martin <[hidden email]> wrote:
You're right. I botched that. The scenario I meant to describe was:

    foo :: _ => f a -> f a -> Bool
    foo x y = Compose (Just x) == Compose (Just y) && Compose [x] == Compose [y]

The different results are:
* FlexibleContexts approach: `(Eq (Maybe (f a)), Eq [f a])`
* Eq1 typeclass: `(Eq1 f, Eq a)`
* Quantified Constraints: `(forall x. Eq x => Eq (f x), Eq a)`

Only the FlexibleContexts approach mentions Maybe and [] in the constraints.

On Tue, May 5, 2020 at 1:56 PM David Feuer <[hidden email]> wrote:
Why is that a problem? `Eq a` is still sufficient.

On Tue, May 5, 2020, 1:51 PM Andrew Martin <[hidden email]> wrote:
I dislike the FlexibleContexts approach because it gives you constraints that do not compose. Consider this minimal example:

    foo :: _ => a -> a -> Bool
    foo x y = Compose (Just (Just x)) == Compose (Just (Just y)) && Compose [Just x] == Compose [Just y]

What do we expect the constraint to be? With the Eq1 machinery or with QuantifiedConstraints, it's `Eq a` (GHC will infer this). However, with FlexibleContexts, it's `(Eq (Compose Maybe Maybe a), Eq (Compose [] Maybe a)`.

On Tue, May 5, 2020 at 12:45 PM David Feuer <[hidden email]> wrote:
I oppose the QuantifiedConstraints version because:

1. It is more complicated than the FlexibleConstraints one.

2. It is strictly less general than the FlexibleConstraints one.

3. There is no apparent benefit to pay for detriments 1 and 2.

On Fri, Mar 13, 2020, 11:59 PM chessai . <[hidden email]> wrote:
Consider the Eq instance for these types. Currently we rely on:

(Eq1 f, Eq1 g, Eq a)

But some potential improvements include changing to:

(Eq (f (g a))) (FlexibleContexts)

or

(forall x. Eq x => Eq (f x), forall x. Eq x => Eq (g x), Eq a)
(QuantifiedConstraints)

There was a discussion sometime last year about the same thing
regarding Semigroup/Monoid instances for `Compose` [1]. Additionally,
the question has been raised again for Data.Functor.{Product,Sum} on
Gitlab [2, 3]. There has been no consensus in either case, but that's
not too worrying as both discussions have been brief. I'm currently
not happy with the {Eq,Ord,Show}{1,2} family of classes, and would
hope to work toward their removal, or at least the shrinking of their
presence in base. Even though the linked proposals are about a single
type, I think it's important that we come up with a decision and stick
with it. Having different APIs for different types here would be
pretty confusing, and some could even say sloppy.

Please let me know your thoughts.

[1]: https://mail.haskell.org/pipermail/libraries/2019-July/029771.html
[2]: https://gitlab.haskell.org/ghc/ghc/issues/17015
[3]: https://gitlab.haskell.org/ghc/ghc/merge_requests/1704
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries


--
-Andrew Thaddeus Martin


--
-Andrew Thaddeus Martin
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
12