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
On Friday 27 August 2010 14:54:53, Patrick Browne wrote:
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
No, it's the other way round. Every HUMAN is also a BEING, hence HUMAN(t) => BEING(t) Admittedly, the notation for subclasses in Haskell is backwards. The corresponding situation for Java interfaces (which are roughly analogous to type classes) would be interface BEING{ ... } interface HUMAN extends BEING{ ... }
Daniel Fischer wrote:
class BEING human => HUMAN human where Sub-classing is logical implication BEING(human) => HUMAN(human) All types t that make BEING(t) = true also make HUMAN(t)=true
No, it's the other way round. Every HUMAN is also a BEING, hence
HUMAN(t) => BEING(t)
Could I say that HUMAN is a subset of BEING? Sebastian Fischer wrote:
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".
Thanks for pointing out my error But I am still not sure of the interpretation of logical implication wrt to sub-classes. Lets simplify the representation and just regard the classes in the example as propositions (instead of predicates). I am not sure if this simplification still makes the example valid. Below is a reasonable interpretation of propositional logical implication. a) If I wear a raincoat then I stay dry (sufficient condition) wareRaincoat => stayDry b) I will stay dry only if I ware a raincoat(necessary condition) stayDry => wareRaincoat In the light of the above examples how should I interpret the class-to-subclass relation as logical implication? Is it a) If BEING then HUMAN (sufficient condition): BEING => HUMAN b) HUMAN is true only if BEING (necessary condition): HUMAN => BEING c) Neither? Thanks, 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
Daniel Fischer wrote:
class BEING human => HUMAN human where Sub-classing is logical implication BEING(human) => HUMAN(human) All types t that make BEING(t) = true also make HUMAN(t)=true
No, it's the other way round. Every HUMAN is also a BEING, hence
HUMAN(t) => BEING(t)
Could I say that HUMAN is a subset of BEING?
That depends on whether predicates are sets.. But yes, every instance of HUMAN is also an instance of BEING, hence, the set of HUMAN instances is a subset of the set of BEING instances.
In the light of the above examples how should I interpret the class-to-subclass relation as logical implication? Is it a) If BEING then HUMAN (sufficient condition): BEING => HUMAN b) HUMAN is true only if BEING (necessary condition): HUMAN => BEING c) Neither?
b). Every HUMAN is a BEING. Cheers, Sebastian -- Underestimating the novelty of the future is a time-honored tradition. (D.G.)
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 On 8/28/10 06:17 , Patrick Browne wrote:
In the light of the above examples how should I interpret the class-to-subclass relation as logical implication? Is it a) If BEING then HUMAN (sufficient condition): BEING => HUMAN b) HUMAN is true only if BEING (necessary condition): HUMAN => BEING c) Neither?
(b). But there's an additional wrinkle: what it really says is "A HUMAN is (...). Oh, and it's a BEING too." Which is to say, Haskell doesn't look at BEING until *after* it's decided something is a HUMAN. (Technically speaking, constraints are not used when selecting an instance; they're applied after the fact, and if the selected instance doesn't conform then it throws a type error.) - -- brandon s. allbery [linux,solaris,freebsd,perl] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH -----BEGIN PGP SIGNATURE----- Version: GnuPG v2.0.10 (Darwin) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/ iEYEARECAAYFAkx5KOcACgkQIn7hlCsL25UWyQCfTblcgeEfwOci9KE7leVs07aN VT4AoJAwHqXoD6nbD+TZVRlAWj3N99SM =jA0B -----END PGP SIGNATURE-----
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.)
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
participants (4)
-
Brandon S Allbery KF8NH -
Daniel Fischer -
Patrick Browne -
Sebastian Fischer