Improving the instances of Data.Functor.{Product,Sum}
John Ericson
john.ericson at obsidian.systems
Tue May 5 16:36:04 UTC 2020
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
> <john.ericson at obsidian.systems> 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 <oleg.grenrus at iki.fi
>> <mailto:oleg.grenrus at iki.fi>> 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
>>> <rae at richarde.dev <mailto:rae at richarde.dev>> wrote:
>>>
>>>
>>>
>>>> On Mar 14, 2020, at 4:14 AM, Eric Mertens
>>>> <emertens at gmail.com <mailto:emertens at gmail.com>> 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
>>> Libraries at haskell.org <mailto:Libraries at haskell.org>
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>> _______________________________________________
>> Libraries mailing list
>> Libraries at haskell.org <mailto:Libraries at haskell.org>
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>
>>
>> _______________________________________________
>> Libraries mailing list
>> Libraries at haskell.org <mailto:Libraries at haskell.org>
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20200505/1130ba06/attachment.html>
More information about the Libraries
mailing list