[Haskell-cafe] type classes and logic

Patrick Browne patrick.browne at dit.ie
Fri Aug 27 18:50:46 EDT 2010

Thanks for your very useful reply.
Does the EQ example below not talk about inhabited types as proofs.


Sebastian Fischer wrote:
>>> If we find a value for a type that is a proof that a type exists (it is
>>> inhabited) that is a member of the class

>> I don't understand the above statement. The "inhabitedness" of a type
>> does not tell us anything about which classes it belongs to. Instance
>> declarations do.

The EQ example following is from:

A type class in Haskell is a proposition about a type.

class Eq a where
    (==) :: a -> a -> Bool
    (/=) :: a -> a -> Bool

means, logically, there is a type a for which the type a -> a -> Bool is
inhabited, or, from a it can be proved that a -> a -> Bool (the class
promises two different proofs for this, having names == and /=). This
proposition is of existential nature. A proof for this proposition (that
there is a type that conforms to the specification) is (obviously) a set
of proofs of the advertised proposition (an implementation), by an
instance declaration:

instance Eq Bool where
    True  == True  = True
    False == False = True
    _     == _     = False

(/=) a b = not (a == b)

This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie

More information about the Haskell-Cafe mailing list