[Haskell-cafe] type classes and logic

[Patrick Browne]

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

Thanks,
Pat



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:
http://www.haskell.org/haskellwiki/Curry-Howard-Lambek_correspondence

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