Improving the instances of Data.Functor.{Product,Sum}
David Feuer
david.feuer at gmail.com
Sat Apr 18 18:51:09 UTC 2020
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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20200418/3ed6bfa0/attachment.html>
More information about the Libraries
mailing list