Я написал реализацию Applicative
и VerifiedApplicative
для пары с моноидом:
import Interfaces.Verified
VerifiedMonoid a => Applicative (Pair a) where
(l, f) <*> (r, x) = (l <+> r, f x)
pure x = (neutral, x)
VerifiedMonoid a => VerifiedApplicative (Pair a) where
applicativeMap (l, x) g = sym $ cong {f=(\y => (y, g x))} (monoidNeutralIsNeutralR l)
applicativeIdentity = ?h1
applicativeComposition = ?h2
applicativeHomomorphism = ?h3
applicativeInterchange = ?h4
Хотя она компилируется, если я ослаблю условие на a
в Applicative
экземпляр выглядит следующим образом:
Monoid a => Applicative (Pair a) where
(l, f) <*> (r, x) = (l <+> r, f x)
pure x = (neutral, x)
Я вижу сообщение об ошибке с жалобой на applicativeMap
:
When checking right hand side of Interfaces.Verified.Contravariant.Pair a implementation of Interfaces.Verified.VerifiedApplicative, method applicativeMap with expected type
map g (l, x) = pure g <*> (l, x)
When checking an application of function Prelude.Basics.cong:
Type mismatch between
(<+>) {{constructor of Interfaces.Verified.VerifiedSemigroup#Semigroup a {{constructor of Interfaces.Verified.VerifiedMonoid#VerifiedSemigroup a}}}}
neutral
l =
l (Type of monoidNeutralIsNeutralR l)
and
(<+>) {{constructor of Prelude.Algebra.Monoid#Semigroup ty {{constructor of Interfaces.Verified.VerifiedMonoid#Monoid a}}}} neutral l = l (Expected type)
Specifically:
Type mismatch between
(<+>) {{constructor of Interfaces.Verified.VerifiedSemigroup#Semigroup a {{constructor of Interfaces.Verified.VerifiedMonoid#VerifiedSemigroup a}}}}
neutral
l
and
(<+>) {{constructor of Prelude.Algebra.Monoid#Semigroup ty {{constructor of Interfaces.Verified.VerifiedMonoid#Monoid a}}}}
neutral
l
Так как он показан Semigroup ty
, по-видимому, Semigroup
экземпляр не выводится.Я пытался записать это явно как (Semigroup a, VerifiedMonoid a) => VerifiedApplicative (Pair a)
, но это не помогает.
Также речь идет о проблеме наследования алмазов, начиная с Semigroup => Monoid => VerifiedMonoid
и в то же время Semigroup => VerifiedSemigroup => VerifiedMonoid
.
Есть идеи, как это обойти?Ограничение Applicative
экземпляра только на VerifiedMonoid
немного неудобно.