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