Improving the instances of Data.Functor.{Product,Sum}
David Feuer
david.feuer at gmail.com
Tue Apr 21 01:47:38 UTC 2020
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> 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> wrote:
>>
>>>
>>>
>>> On Mar 14, 2020, at 4:14 AM, Eric Mertens <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 listLibraries at haskell.orghttp://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>
>> _______________________________________________
>> Libraries mailing list
>> Libraries at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>
>
> _______________________________________________
> Libraries mailing listLibraries at haskell.orghttp://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20200420/d7553f3b/attachment.html>
More information about the Libraries
mailing list