Order Theory

First, I add Matt Might's partial order type class.

class PartialOrder t where
 (⊑) :: t -> t -> Bool

To make a type a partial order, I need to define ⊑ on a type.

Next, I enumerate the possible sign values and define a type that contains a set of them.

import qualified Data.Set as Set

data Sign = Positive | Negative | Zero deriving (Show, Ord, Eq)
type SignAlternatives = Set.Set Sign

Example:

Set.fromList []) --> fromList []
Set.fromList [Positive, Negative] --> fromList [Positive,Negative]

Finally, I make the SignAlternatives type an instance of the PartialOrder class.

instance PartialOrder SignAlternatives where
   a ⊑ b = b `Set.isSubsetOf` a

Notice that we swap the order of a and b. This is because a ⊑ b means that a is a conservative estimate of b. If a ⊑ b, a can be used to replace b, but there's no gurantee b can replace a.

Examples:

(Set.fromList [Negative]) ⊑ (Set.fromList [Positive, Negative]) -- => False
(Set.fromList [Positive, Negative]) ⊑ (Set.fromList [Negative]) -- => True

Partial orders must be antisymmetric, reflexive, and transitive. The Data.Set.isSubsetOf function is all of these things, so we have a proper partial order.

The final code is below. The required imports and extensions are at the top. We need flexible instances because we're making a concrete type into an instance of a type class.

{-# LANGUAGE FlexibleInstances #-}

import qualified Data.Set as Set

class PartialOrder t where
 (⊑) :: t -> t -> Bool

data Sign = Positive | Negative | Zero deriving (Show, Ord, Eq)
type SignAlternatives = Set.Set Sign

instance PartialOrder SignAlternatives where
   a ⊑ b = b `Set.isSubsetOf` a

Using another of Matt Might's type classes, we can make our partial order a lattice.

First, I add Matt Might's lattice type class.

class PartialOrder t => Lattice t where
 (⊔) :: t -> t -> t
 (⊓) :: t -> t -> t

A lattice is a partial order that defines a meet and join operation, represented by ⊔ and ⊓.

I make SignAlternatives an instance of lattice by implementing meet and join.

instance Lattice SignAlternatives where
 a ⊔ b = a `Set.intersection` b
 a ⊓ b = a `Set.union` b

Using another of Matt Might's type classes, we can make our lattice a bounded lattice. A bounded lattice is a normal lattice, but it has two special values: top and bottom, represented ⊤ by ⊥. I'll edit Matt Might's type class to use the symbols.

class Lattice t => BoundedLattice t where
 (⊥) :: t
 (⊤) :: t

The bottom value, ⊥, is the value is the most conservative estimate; the universal set. Fortunately, our universal set is finite, it only has three items. The top, ⊤, is the the least conservative estimate: an empty set.

(We could have defined a ⊥ value for the partial; no lattice is needed. A bounded partial order is possible.)

instance BoundedLattice SignAlternatives where
  bot = Set.fromList [Positive, Negative, Zero]
  top = Set.empty

Examples:

(⊥) :: SignAlternatives --> fromList []
(⊤) :: SignAlternatives --> fromList [Positive,Negative,Zero]

Really, our lattice doesn't have a top, ⊤. The meaning of an empty set for signs analysis is undefined. The least conservative estimates are {Positive}, {Zero}, and {Negative}. Instead of defining a meaningless top, ⊤, we can just leave it undefined.

instance BoundedLattice SignAlternatives where
  bot = Set.fromList [Positive, Negative, Zero]
  top = error "undefined"

Examples:

(⊤) :: SignAlternatives --> fromList [Positive,Negative,Zero]

The bounded partial order is useful, but I'm not sure about the lattice. Lattices are normally used to combine data from control flow graphs, but here I'm using it for abstract interpretation. I could have stopped at the bounded preorder and written an abstract interpreter.