CODEWITHSUNDEEP
haskell
Sergey Sosnin
Sergey Sosnin

Reputation: 1413

"ExistentialQuantification" and Eq instance

When I tried to use ExistentialQuantification I faced with a problem

Let's suppose you have a type

data T s = forall s. (Show s,Eq s) => T (String,s)

I want to write an instance Eq for this type, say:

instance Eq (T a) where
    (T (name,value)) == (T (name',value'))  | (name /= name') = False
                                            | otherwise = value == value'

but it fails:

Could not deduce (s1 ~ s)
from the context (Show s, Eq s)

Another instance declaration 

instance Eq a => Eq (T a) where

results the same error:

   Could not deduce (s1 ~ s)
    from the context (Eq a)

Upvotes: 1

Views: 218

Answers (2)

augustss
augustss

Reputation: 23014

To expand on my comment, here's how you can do it

{-# LANGUAGE ExistentialQuantification #-}
module E where
import Data.Typeable

data T = forall s. (Show s, Eq s, Typeable s) => T String s

instance Eq T where
    T name value == T name' value' = name == name' && maybe False (== value') (cast value)

This assumes that if the types in the existential are different then the values should not compare equal.

Upvotes: 4

J. Abrahamson
J. Abrahamson

Reputation: 74344

Each time you "open" an existential data type you expose a piece of data whose type has been forgotten. To handle this, Haskell must establish a type for this data from nothing and therefore it produces a completely unique, fresh type variable.

This means that if you open two different existentials then the fresh types will not coincide no matter what you do. This is the meaning of the error messages you received.

This is also, of course, the correct behavior. For instance, all we need to use your T constructor are instances of Show and Eq. Both Int and String satisfy this so the following are both valid values

data T = forall s. (Show s,Eq s) => T (String,s)

x, y :: T
x = T ("string", "string")
y = T ("int", 3)

but we cannot expect that the Eq instance for either String or Int is sufficient to compare 3 == "string" as your instance Eq T attempts to do.

So how can this be resolved? We need an notion of equality which works regardless of the type of the data being stored inside of T. To do so we can establish a projection, e.g.

data T = forall s . T String s (s -> (String, Int))

where the third parameter to T is a function which produces both the values shown representation and an integer hash value which we'll use for equality

instance Eq T where
  T nm1 s1 f1 = T nm2 s2 f2 = 
    nm1 == nm2 && snd (f1 s1) == snd (f2 s2)

Now this works but the representation raises an issue—if the only thing we can do with our anonymously-typed value is apply it to its copatriot anonymously-typed function... then why not just do that in the first place?

data T = T String String Int

t :: Show s => String -> s -> (s -> Int) -> T
t nm s f = T nm (show s) (f s)

Upvotes: 2

Related Questions