Derive Ord con restricciones cuantificadas (para a. Ord a => Ord (fa))

10

¿Con restricciones cuantificadas puedo derivar Eq (A f)bien? Sin embargo, cuando intento derivar Ord (A f) falla. No entiendo cómo usar restricciones cuantificadas cuando la clase de restricción tiene una superclase. ¿Cómo obtengo Ord (A f)y otras clases que tienen superclases?

> 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)'

PD. También he examinado las propuestas de ghc 0109-restricciones cuantificadas . Usando ghc 8.6.5

William Rusnack
fuente

Respuestas:

8

El problema es que Eqes una superclase de Ord, y la restricción (forall a. Ord a => Ord (f a))no implica la restricción de superclase Eq (A f)que se requiere para declarar una Ord (A f)instancia.

  • Tenemos (forall a. Ord a => Ord (f a))

  • Necesitamos Eq (A f), es decir, lo (forall a. Eq a => Eq (f a))que no está implícito en lo que tenemos.

Solución: agregar (forall a. Eq a => Eq (f a))a la Ordinstancia.

(Realmente no entiendo cómo el mensaje de error dado por GHC se relaciona con el problema).

{-# 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)

O un poco más ordenado:

{-# 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)
Li-yao Xia
fuente
Estaba tan cerca con deriving instance (forall a. (Eq a, Ord a) => (Eq (f a), Ord (f a))) => Ord (A f). ¿Sabes por qué hay una diferencia?
William Rusnack
1
Eso tampoco implica forall a. Eq a => Eq (f a). (visto en términos de lógica (A /\ B) => (C /\ D)no implica A => C)
Li-yao Xia
1
De hecho, lo que escribiste es equivalente a forall a. Ord a => Ord (f a).
Li-yao Xia
¡Gracias por la explicación!
William Rusnack