Type classes and the structure of types

A type might have some relevant structure. In fact, multiple types might share the same structure. The notion of a type having a structure is expressed in Haskell by means of type classes. Some type classes are rather banal; the type class Show expresses that a particular type can be turned into a String.1 

class Show a where
  show :: a -> String

This type class definition should be read in the following way:

  • there is a type class called Show
  • if a type a belongs to this class,
  • then there is a function show defined on elements of type a

The type class Bounded expresses that a particular type has two special elements, called the minBound and the maxBound.2 

class Bounded a where
  minBound :: a
  maxBound :: a

A more useful type class, Eq, expresses that we know how to compare two elements of a type to determine whether they are equal. 

class Eq a where
  (==) :: a -> a -> Bool

Not all types can be compared for equality. For example, how should we test whether two functions f and g of some type a -> b are equal?!3 In general we cannot, but, if the type a is structured in a particular way, we can: 

instance (Bounded a, Enum a, Eq b) => Eq (a -> b) where
  f == g = all (\x -> f x == g x) [minBound .. maxBound]

Here we have stated how to compare two functions for equality, PROVIDED THAT we know how to

  1. compare their outputs for equality
  2. enumerate their possible inputs

We state these provisos by listing constraints on the allowable types (to the left of the ). Here, constraining the result type b of the functions to be one where equality is decidable is straightforward. To constrain a so that we can enumerate it, we require that it be bounded, so that we know where to start enumerating from, and that it be enumerable, so that we can do the enumerating.

The expression [minBound..maxBound] makes use of three linguistic idioms associated with typeclasses: the minBound and maxBound are from the Bounded typeclass, and the [..] is from the Enum typeclass. This expression cannot be evaluated on its own, but requires that we specify which type we are intending to use. Another way of thinking about expressions like [minBound..maxBound] is that they are simply linguistic terms, which must be interpreted. They can be interpreted in any type which instantiates both the Enum and the Bounded typeclasses.

In general, we can create terms using operations from multiple diverse typeclasses (as illustrated above with the Enum and Bounded typeclasses). In order to interpret such terms in some type, we need to (independently!) specify how to interpret each typeclass in that type. This permits us to focus on interpreting individual typeclasses, and to automatically obtain a way to interpret their combination. (This is a modular approach to program construction.)

The logic of unanalysed sentences

We start our semantic journey at the beginning. We note that certain sentences are true, and others are false. Instead of defining a new type of things which are sentences, we use the class system to allow us to find 'sentences' in other types. As there are infinitely many sentences, we can arrange them in a list (perhaps in alphabetical order) and refer to them by number (by their position in this list). We say that a type has propositional structure just in case we can find an object in it for each sentence to denote. 

class Prop b where
  p :: Int -> b

We will be interested in writing terms (expressions in Haskell), which we will interpret in various ways via the class system. The term p 7 is a Haskell expression (with type Prop b => b) which we will intuitively understand as representing 'proposition number 7', and which a logician might write \(P_{7}\).

This by itself isn't very interesting; nearly any type could be a meaning space for our propositional terms! It only becomes interesting once we want to do things with propositions. Here are some uninteresting instances of the class Prop. 

instance Prop () where
  p _ = ()
-- p 7 :: () == ()

instance Prop Char where
  p _ = 'a'
-- p 7 :: Char == 'a'

instance Prop Int where
  p i = i
-- p 7 :: Int == 7

More interesting will be the way we would like to combine meaning spaces of propositions. If a and b are two meaning spaces for propositions, then so is their product. 

instance (Prop a,Prop b) => Prop (a,b) where
  p i = (p i, p i)

We are interested fundamentally in the notion of entailment, in which our semantic competence manifests itself in an observable way. We define entailment informally in terms of truth in a situation; a sentence \(\phi\) entails another \(\psi\) just in case in any situation in which \(\phi\) is true, so is \(\psi\). We begin by considering how to define truth in a situation, before turning to entailment.

Truth in a Situation

In our intended model of propositions, the meaning of a proposition is something which requires a situation for its evaluation into a boolean domain. We implement this as a function from situations to true or false. 

newtype PropInt = PropInt (PropSit -> Bool)

extractPropInt :: PropInt -> PropSit -> Bool
extractPropInt (PropInt phi) = phi

What should a propositional situation be? It had better be something on the basis of which we can determine whether a sentence is true or false! As we are not analysing the internal structure of propositions, a situation will have to be able to tell us whether or not a proposition is true. 

type PropSit = Int -> Bool

We need to define how exactly our intended model of propostions supports propositional structure. If a proposition denotes a function from situations to truth values, then how are we to compute the truth value of the \(i^{th}\) proposition in a given situation? The answer is to simply ask the situation what the truth value of the \(i^{th}\) proposition is. 

instance Prop PropInt where
  p i = PropInt $ \g -> g i

Defining PropInt as an instance of Prop means that we can interpret terms in the type PropInt.

We can define a function to take a proposition and a situation and to compute the truth of that propositon in that situation. 

isTrueProp (PropInt phi) = phi

Validity

We have shown how propositions can be interpreted in the type of functions from situations to truth values. This gives us a way of determining, for a given situation, whether a sentence is true or false in that situation. Our characterization of validity, however, refers to truth in every situation. How are we to determine whether a sentence is valid? A naive approach is to interpret the sentence as usual, and then to enumerate all possible situations, verifying that the sentence is true in each of them. This is doomed to failure, as there are non-denumerably many possible situations!4 In some cases, the problem of there being infinitely many situations is tamed by the fact that the situations fall into finitely many groups; a situation will either make a given sentence true or false, and what it does on other sentences is completely irrelevant to this fact. Accordingly, we would like to be able to compute which propositional atoms appear in a sentence. We could do this if propositions denote the set of atoms which appear in them. 

--- Determining which propositional atoms appear in a sentence
newtype WhichAtoms =
  WhichAtoms [Int]

extractAtoms :: WhichAtoms -> [Int]
extractAtoms (WhichAtoms atms) = atms

As we want to understand this type as a collection of sets of integers, we give it a monoidal structure, with the multiplication of the monoid set union. 

instance Semigroup WhichAtoms where
  WhichAtoms a1 <> WhichAtoms a2 = WhichAtoms (a1 `union` a2)

instance Monoid WhichAtoms where
  mempty = WhichAtoms []

As our propositions are atomic, without internal structure, the e.g. seventh proposition just has one part; namely, itself. 

instance Prop WhichAtoms where
  p n = WhichAtoms [n]

Given a proposition of the form p i, if we interpret it in the domain of pairs of WhichAtoms and PropInt, we can use the first component to collect the identifiers of the proposition, and using that to create the relevant situations, and then to evaluate the second component on each relevant situation. 

isValidProp phi = all (isTrueProp pI) relevantSituations
  where
    relevantSituations = [charFunc sit | sit <- powerSet atms]
    (WhichAtoms atms, pI) = phi

Entailment is a relation holding between a set of sentences (the premises) and a sentence (the conclusion). We define a data type (called a Sequent) which contains premises and conclusions. 

data Sequent a = Seq [a] a deriving (Eq,Show,Ord)

A sequent is valid, that is, the premises of a sequent entail its conclusion, just in case the conclusion is true in all relevant situations, where a situation is relevant just in case it makes all of the premises sentences true. 

isValidPropSeq (ant `Seq` cons) = all (isTrueProp consProp) relevantSituations
  where
    relevantSituations = filter makesPremisesTrue allSits
    allSits = [charFunc sit | sit <- powerSet allAtoms]
    makesPremisesTrue sit = all (flip isTrueProp sit) premiseProps
    (consAtm,consProp) = cons
    WhichAtoms allAtoms = mconcat (consAtm : premiseAtms)
    (premiseAtms,premiseProps) = unzip ant

We can verify that isValidProp is the special case of isValidPropSeq when the antecedent list is empty: as ant == [], we know that

  1. premiseAtms == [] and premisProps == []
  2. WhichAtoms allAtoms == consAtm
  3. makesPremisesTrue sit == True
  4. relevantSituations == allSits
  5. and allSits is just the set of characteristic functions of all subsets of the consAtm atoms

If we simplify these definitions in the definition of isValidPropSeq accordingly, we obtain: 

isValidPropSeq ([] `Seq` cons) = all (isTrueProp consProp) relevantSituations
  where
    relevantSituations = [charFunc sit | sit <- powerSet allAtoms]
    (WhichAtoms allAtoms,consProp) = cons

which is virtually identical with isValidProp. We can thus simply define isValidProp in terms of isValidPropSeq: 

isValidProp = isValidPropSeq . Seq []

In our current setup, where we are not analysing the internal structure of propositions, there are no valid propositions - for every propositional term, it will be true in some situations and false in others - and the only valid sequents are those where the conclusion is one of the premises. This is deeply unsatisfying (because it does not provide a good model of our behaviour), and we will begin to address it later on.

Helper Functions

Sets and functions from elements to booleans are isomorphic, with the characteristic function of a set \(X\) the function \(f_{X}\) which maps an object to True iff that object is an element of \(X\), and the set \(S_{f}\) corresponding to a function \(f\) containing all and only those objects which \(f\) maps to True. 

charFunc :: Eq a => [a] -> (a -> Bool)
charFunc set o = o `elem` set

powerSet takes a set (represented as a list) and computes all possible subsets thereof. 

powerSet :: [a] -> [[a]]
powerSet [] = [[]]
powerSet (x:xs) = pxs ++ [x:p | p <- pxs]
  where
    pxs = powerSet xs

An alternative definition of powerSet is: 

pS :: [a] -> [[a]]
pS [] = [[]]
pS (x:xs) = foldr (\s ss -> (x:s):s:ss) [] $ pS xs

Adding boolean structure

When we consider the internal structure of sentences, in particular those involving the sentential connectives and, or and not, we see that the truth conditions of these complex sentences are predictable from the atomic sentences they contain and the ways in which these are combined with the connectives.

Boolean Lattices

Here we introduce type classes expressing that a type has a boolean structure.

A type has a lattice structure just in case we can define greatest lower and least upper bound operations. 

class Lattice b where
  glb :: b -> b -> b
  lub :: b -> b -> b

There are numerous types with this structure. For instance, the type Bool is a lattice in this sense. 

instance Lattice Bool where
  glb = (&&)
  lub = (||)

In addition, if a type has lattice structure, than so does the type of functions into that type, with the lattice opperations being defined pointwise. 

instance Lattice b => Lattice (a -> b) where
  f `glb` g = \x -> f x `glb` g x
  f `lub` g = \x -> f x `lub` g x

Similarly, given two types with lattice structure, the type of pairs of those types has it as well. 

instance (Lattice b,Lattice c) => Lattice (b,c) where
  (b1,c1) `glb` (b2,c2) = (b1 `glb` b2, c1 `glb` c2)
  (b1,c1) `lub` (b2,c2) = (b1 `lub` b2, c1 `lub` c2)

Some types with lattice structure have additional structure. A boolean lattice is a lattice with a complement operation, and with designated top and bottom elements. 

class Lattice b => Boolean b where
  top :: b
  bot :: b
  cmp :: b -> b

All of the lattice types we have discussed are also boolean lattices. 

instance Boolean Bool where
  top = True
  bot = False
  cmp = not

instance Boolean b => Boolean (a -> b) where
  top = \x -> top
  bot = \x -> bot
  cmp f = \x -> cmp $ f x

instance (Boolean b,Boolean c) => Boolean (b,c) where
  top = (top,top)
  bot = (bot,bot)
  cmp (b,c) = (cmp b, cmp c)

This allows us to write terms like top `glb` (top `lub` bot), with type Boolean b => b.

Truth in a Situation

We would like to show that our intended model of propositions, the type PropInt, supports boolean structure (interpreting and as the lattice glb, or as lub, and not as the boolean cmp). Because PropInt is morally a type which maps to a known boolean type (Bool), this can be done pointwise (modulo the type constructor PropInt).5 

instance Lattice PropInt where
  PropInt i `glb` PropInt j = PropInt (i `glb` j)
  PropInt i `lub` PropInt j = PropInt (i `lub` j)
instance Boolean PropInt where
  top = PropInt top
  bot = PropInt bot
  cmp (PropInt i) = PropInt (cmp i)

This is all we need to do! As we have previously defined the function isTrueProp to map a PropInt and a situation to a truth value, any way of delivering a PropInt to this function is acceptable. By showing how PropInt has a boolean structure, we are able to interpret expressions with boolean connectives as being of type PropInt. The sentence "Either (True and P0) or not P1" (in more canonical logical syntax: \((\top \wedge P_{0}) \vee \neg P_{1}\)) can be written in Haskell as the term (top `glb` p 0) `lub` cmp (p 1). This term has type (Boolean a,Prop a) => a, which we should read as saying:

any type which can interpret booleans and Prop can interpret this term

Validity

Our validity checker (isValidProp) worked by interpreting a term both in the domain of WhichAtoms and in the domain of PropInt. We have seen how to interpret booleans in PropInt, now we need only show how to interpret booleans in WhichAtoms.6 

instance Lattice WhichAtoms where
  -- Not really a Lattice: the ordering (if any) is wonky
  -- should be: p ∧ q ≤ p ≤ p ∨ q
  WhichAtoms p `glb` WhichAtoms q = WhichAtoms (p `union` q)
  WhichAtoms p `lub` WhichAtoms q = WhichAtoms (p `union` q)

instance Boolean WhichAtoms where
  -- not really a boolean algebra: doesn't satisfy 0≠1, which would anyways require the ordering to collapse
  top = WhichAtoms []
  bot = WhichAtoms []
  cmp wp = wp

Footnotes:

1

Note that the built-in class Show has additional operations, expressing that a type has even more structure than is shown here.

2

These special elements needn't be distinct; the type () is bounded, with minBound and maxBound the same element, ().

3

It is not even clear what this should mean! A useful notion is extensional equality, which means that they give the same results on the same inputs, irrespective of how they compute these results.

4

A situation, as a function from Ints to truth values, is isomorphic to a set of Ints. It is a famous result (of Georg Cantor) that there are strictly more sets of integers than there are integers! Assume (for a contradiction) that there were not more sets of integers than integers. Then we could enumerate the sets of integers (line them up in an infinite list), such that each set of integers is at some finite position in the list. For each position in the list, we can ask: is the number of that position an element of the list at that position? We construct a new set of numbers, consisting of those numbers where the set at that position does not contain that number. Now this is a perfectly legitimate set of numbers, call it X, and so it must be (by hypothesis) in the list at some position, call it x. Now, is \(x \in X\)? If so, then x is an element of the list at its position, and so by the definition of X, \(x \notin X\). If not, then x is not an element of the list at its position, and so by the definition of X, \(x \in X\). Both of these are contradictory, and so we reject our assumption that there are no more sets of numbers than numbers.

5

What does it mean to say that PropInt "is morally a type which…"? This is a funny (albeit standard) way to say that PropInt is the same as something else, modulo some irrelevant notational differences. In Haskell, newtypes are new types for the purposes of the type checker, but the compiler represents them exactly the same as the type that they are built over.

6

We are 'cheating', as WhichAtoms is not actually boolean. Luckily (?), Haskell is not rich enough to discriminate between domains which are correctly interpreted as boolean lattices, and those which merely allow for an ad hoc implementation of the required operations.

Author: Greg Kobele

Created: 2019-06-29 Sat 15:59

Validate