使用量化约束导出Ord(forall a.Ord a => Ord (f a)) [英] Derive Ord with Quantified Constraints (forall a. Ord a => Ord (f a))

问题描述

通过量化约束，我可以很好地推导出 Eq (A f) 吗?但是，当我尝试推导 Ord (A f) 时，它失败了.当约束类具有超类时，我不明白如何使用量化约束.如何派生 Ord (A f) 和其他具有超类的类?

With quantified constraints I can derive Eq (A f) just fine? However, when I try to derive Ord (A f) it fails. I do not understand how to use quantified constraints when the constraint class has a superclass. How do I derive Ord (A f) and other classes that have superclasses?

> newtype A f = A (f Int)
> deriving instance (forall a. Eq a => Eq (f a)) => Eq (A f)
> deriving instance (forall a. Ord a => Ord (f a)) => Ord (A f)
<interactive>:3:1: error:
    • Could not deduce (Ord a)
        arising from the superclasses of an instance declaration
      from the context: forall a. Ord a => Ord (f a)
        bound by the instance declaration at <interactive>:3:1-61
      or from: Eq a bound by a quantified context at <interactive>:1:1
      Possible fix: add (Ord a) to the context of a quantified context
    • In the instance declaration for 'Ord (A f)'

附注.我还检查了 ghc 提案 0109-量化约束.使用 ghc 8.6.5

PS. I have also examined ghc proposals 0109-quantified-constraints. Using ghc 8.6.5

推荐答案

问题是Eq是Ord的超类，约束(foralla. Ord a => Ord (fa)) 不包含声明Ord (A f)Eq (A f)> 实例.

The problem is that Eq is a superclass of Ord, and the constraint (forall a. Ord a => Ord (f a)) does not entail the superclass constraint Eq (A f) that's required to declare an Ord (A f) instance.

• 我们有 (forall a.Ord a => Ord (f a))

我们需要Eq (A f)，即(forall a.Eq a => Eq (fa))，这不是由我们所拥有的.

We need Eq (A f), i.e., (forall a. Eq a => Eq (f a)), which is not implied by what we have.

解决方案:在Ord实例中添加(forall a.Eq a => Eq (f a)).

Solution: add (forall a. Eq a => Eq (f a)) to the Ord instance.

(我实际上不明白 GHC 给出的错误消息与问题有何关联.)

(I don't actually understand how the error message given by GHC relates to the problem.)

{-# LANGUAGE QuantifiedConstraints, StandaloneDeriving, UndecidableInstances, FlexibleContexts #-}

newtype A f = A (f Int)
deriving instance (forall a. Eq a => Eq (f a)) => Eq (A f)
deriving instance (forall a. Eq a => Eq (f a), forall a. Ord a => Ord (f a)) => Ord (A f)

或者更整洁一点:

{-# LANGUAGE ConstraintKinds, RankNTypes, KindSignatures, QuantifiedConstraints, StandaloneDeriving, UndecidableInstances, FlexibleContexts #-}

import Data.Kind (Constraint)

type Eq1 f = (forall a. Eq a => Eq (f a) :: Constraint)
type Ord1 f = (forall a. Ord a => Ord (f a) :: Constraint)  -- I also wanted to put Eq1 in here but was getting some impredicativity errors...

-----

newtype A f = A (f Int)
deriving instance Eq1 f => Eq (A f)
deriving instance (Eq1 f, Ord1 f) => Ord (A f)

这篇关于使用量化约束导出Ord(forall a.Ord a => Ord (f a))的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！