[Haskell-cafe] type classes and logic
Patrick Browne
patrick.browne at dit.ie
Fri Aug 27 18:50:46 EDT 2010
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
More information about the Haskell-Cafe
mailing list