Wyprowadź zamówienie z ograniczeniami ilościowymi (dla wszystkich a. Zamówienie a => Zamówienie (fa))

10

Dzięki ograniczeniom ilościowym mogę dobrze wyprowadzić Eq (A f)? Jednak gdy próbuję wyliczyć Ord (A f), to się nie udaje. Nie rozumiem, jak stosować ograniczenia ilościowe, gdy klasa ograniczeń ma nadklasę. Jak uzyskać Ord (A f)i inne klasy, które mają nadklasy?

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

PS. Przeanalizowałem również propozycje ghc 0109-ograniczenia ilościowe . Korzystanie z ghc 8.6.5

William Rusnack
źródło

Odpowiedzi:

8

Problem polega na tym, że Eqjest to nadklasa Ord, a ograniczenie (forall a. Ord a => Ord (f a))nie pociąga za sobą ograniczenia nadklasy Eq (A f)wymaganego do zadeklarowania Ord (A f)instancji.

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

  • Potrzebujemy Eq (A f)tzn. Tego (forall a. Eq a => Eq (f a)), co nie wynika z tego, co mamy.

Rozwiązanie: dodaj (forall a. Eq a => Eq (f a))do Ordinstancji.

(Tak naprawdę nie rozumiem, w jaki sposób komunikat o błędzie podany przez GHC odnosi się do problemu).

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

Lub trochę bardziej schludnie:

{-# 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
źródło
Byłem tak blisko deriving instance (forall a. (Eq a, Ord a) => (Eq (f a), Ord (f a))) => Ord (A f). Czy wiesz, dlaczego jest różnica?
William Rusnack
1
To też nie oznacza forall a. Eq a => Eq (f a). (postrzegane pod względem logicznym (A /\ B) => (C /\ D)nie oznacza A => C)
Li-yao Xia
1
W rzeczywistości to, co napisałeś, jest równoważne forall a. Ord a => Ord (f a).
Li-yao Xia
Dziękuję za wyjaśnienie!
William Rusnack