[Haskell-cafe] type classes and logic

[Sebastian Fischer]

Hi Pat,

> A proof for the  predicate BEING(being) must show that there is an
> inhabited type (a type which has values)

Note that in a lazy language like Haskell every type is inhabited by _| 
_, that is, "bottom" the undefined value.

> 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.

> With at least one instantiation existing (e.g.  BEING(Person) =  
> true) we
> can define a sub-class

You can define subclasses even if no instances exist. And as Daniel  
said, the code

     class BEING human => HUMAN human where

defines a subclass HUMAN of BEING which means that every instance of  
HUMAN must also be a BEING. You can read it as: "a BEING is also a  
HUMAN by the following definitions".

> In general for the HUMAN sub-class to be useful additional constraints
> are added after the where keyword. These are similar in purpose to  
> those
> described in an ordinary class (not a sub-class)

The "additional constraints" are additional functions that need to be  
available.

> What is the logical role of the functions in the classes and
> instances. Are they constraints on the types in predicates?

BEING(Person) tells you that the type Person implements the functions  
declared in the type class BEING.

> Any instantiation that respects types is fine?

That depends whether you ask a compiler or a programmer. The compiler  
is satisfied if you respect the types. But type classes often come  
with additional laws on the operations that programmers have come to  
expect. For example, every implementation of the function == of the Eq  
class should be an equivalence relation and a Monad instance should  
obey the monad laws. Although the compiler does not complain if it  
doesn't, users of such an invalid Monad instance eventually will.

Cheers,
Sebastian


-- 
Underestimating the novelty of the future is a time-honored tradition.
(D.G.)