Improving the instances of Data.Functor.{Product,Sum}
John Ericson
john.ericson at obsidian.systems
Tue Apr 21 01:44:50 UTC 2020
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
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20200420/e7b84ccd/attachment.html>
More information about the Libraries
mailing list