# Order Theory

In this post, I define a signs analysis lattice as an instance of Matt Might's Haskell type classes. Signs analysis is a form of static analysis that can determine the sign (`+`

, `-`

, `0`

) of an expression. Lattices are common data structures in control flow analysis. Khedker, Sanyal, and Karkare's *Data Flow Analysis Theory and Practice* gives examples of them in use.

## Partial Order

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

## Lattice

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

## Bounded Lattice

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]

## End

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.