how to universally quantify Reified Type Class instance when scraping your type class in haskell?-CodePudding

Studying the infamous blog post scrap your type classes, for the sake of learning, but in particular to understand the meaning of forall in type class instance declaration as stated here Explicit universal quantification (forall)

As well as in type signatures, you can also use an explicit forall in an instance declaration:

instance forall a. Eq a => Eq [a] where ...

This is generally in the backdrop of me refining my understanding of forall in haskell, where among other i have learned how to be careful of its scope.

Hence to make things explicit I have been trying to reproduce the scrap your type classes appraoch for the following use case:

data  DatumType a b = Datum a b deriving Show

instance forall a b . (Eq a, Eq b) => Eq (DatumType a b) where
  (==) (Datum x y) (Datum z e) =  x == z && y == e

renaming Eq as Same, i.e. but declared as

data Same a = Same {
  (===) :: a -> a -> Bool
}

However I get stuck here as I do not see how to write the instance with the forall a b

SameDatumTypeab :: ???
SameDatumTypeab =  Same {
 -- ???
}

Could any one help with this ? is this even possible ?

CodePudding user response：

Nothing you couldn't have come up with some trial and error...

sameDatumTypeab :: ∀ a b . (Eq a, Eq b) => Same (DatumType a b)
sameDatumTypeab = Same {
   (===) = \(Datum x y) (Datum z e) -> x==z && y==e
 }

As usual, the forall is optional (variables that appear are implicitly universal-quantified at the outermost level), i.e. you can simply write

sameDatumTypeab :: (Eq a, Eq b) => Same (DatumType a b)
sameDatumTypeab = Same $ \(Datum x y) (Datum z e) -> x==z && y==e

But actually that's kind of missing the point of Scrap Your Classes, because I'm now using the Eq class though I'm not instantiating it. To make it fully class-free, we want to also convert the (Eq a, Eq b) constraint:

sameDatumTypeab :: Same a -> Same b -> Same (DatumType a b)
sameDatumTypeab (Same eqa) (Same eqb)
   = Same $ \(Datum x y) (Datum z e) -> eqa x z && eqb y e

FTR, the typeclass instance also doesn't need to be explicitly quantified

instance (Eq a, Eq b) => Eq (DatumType a b) where
  Datum x y == Datum z e = x == z && y == e