[Haskell-cafe] type classes and logic

[Patrick Browne]

Hi,
I am trying to understand type classes and sub-classes in purely logical
terms From the literature I gather that:
 1)a type class is a predicate over types (using type variables)
 2)type sub-classing is a logical implication between these predicates.

But I feel that 1) and 2) does not give enough detail and I am missing
the logical significance of the function definitions in the class and
their implementations in the instances. This following example outlines
my current (mis?)understanding:

data Person = Person Name deriving Show
data Employee = Employee Name Position deriving Show

class BEING being where

The class BEING is logically a predicate with type variable being(i.e.
BEING(being))
BEING(being) is true for types that are members of the BEING type class.
Any types that instantiate the type class BEING will have all the BEING
class functions defined on them.
Such a type is a member of the type-class BEING
Actual function signatures and/or default implementations omitted


A proof for the  predicate BEING(being) must show that there is an
inhabited type (a type which has values)
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

instance BEING Person where

All the functions from the class BEING must be defined for the type Person
It is required the functions in the instance respect the types from the
class and type from the instantiated parameter.
t is required that when the functions are run they produce values of the
required type.
Implementations omitted



With at least one instantiation existing (e.g.  BEING(Person) = true) we
can define a sub-class
In the sub-class definition we can assume BEING(human) to be true (type
variable name does not matter)
And based on that assumption we can write a logical implication
BEING(human)  => HUMAN(human)

class BEING human  => HUMAN human where

At this point there is no additional functionality is defined for the
subclass HUMAN
Sub-classing is logical implication BEING(human)  => HUMAN(human)
All types t that make BEING(t) = true also make HUMAN(t)=true
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)


Another example from Bird[1.Intro. to Functional Prog. using Haskell]
class Enum a where
 toEnum :: a -> Int
 fromEnum :: Int -> a

A type is declared an instance of the class Enum by giving definitions
toEnum and fromEnum, functions that convert between elements of the type
a and the type Int. In instance declarations fromEnum should be a left
inverse to toEnum That is for all x fromEnum(toEnum x) = x. This
requirement cannot be expressed in Haskell




My questions are:
a) Is the above *logical view* of type classes correct?

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

c) Apart from signature matching between class-to-instance is there any
logical relation between the functions in a class and the functions in
an instances. From Birds[1] example I suspect that while the types are
subject to logical rules of 1) and 2) the actual functions in the
instance do not have to obey any logical laws. Any instantiation that
respects types is fine?

Regards,
Pat


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