This is something of a followup to a previous post, expanding upon the idea of using types to constrain the set of a program’s reachable states.
This case study deals with implementing propositional logic in Standard ML, the design decisions involved in both representing the data and transforming it, and how types help us prevent errors.
Propositional Logic
Propositional logic, also called zerothorder logic, is a simple classical logic where all logical formulae are either atoms (which are replaced by Boolean values during evaluation), or logical connectives that implement the Boolean operations we’re familiar with, like negation, conjunction, etc.
Definition
A formula in propositional logic is one of:

An atom
P
. Essentially a variable that is assigned a truth value by an interpretation when evaluating the formula. 
A negation
¬P
, which is true wheneverP
is false. 
A conjunction
P ∧ Q
, which is true whenever bothP
andQ
are true. 
A disjunction
P ∨ Q
, which is true whenever at least one ofP
orQ
are true. 
An implication
P > Q
, which is false whenP
is true andQ
is false, and is true otherwise. 
Biconditional implication
P <> Q
, read as “P
if and only ifQ
”, is true when bothP
andQ
have the same truth value.
The last two connectives are not primitive: they are easily translated to simpler formulae:
P > Q = (¬P) ∨ Q
P <> Q = (P > Q) ∧ (Q > P)
Representation
Fred Brooks said representation is the essence of programming, so first we’ll define the structure of propositional formulae.
The fact that two of these logical connectives are not primitive induces a design decision.
One approach would be to leave the implication and the biconditional off the
formula
datatype, and just have two constructors, implication
and iff
,
that expand to their definitions:
type atom = char
datatype formula = Atom of atom
 Negation of formula
 Conjunction of formula * formula
 Disjunction of formula * formula
fun implication (p: formula, q: formula): formula =
Conjunction (Negation p, q)
fun iff (p: formula, q: formula): formula =
Conjunction (implication (p, q), implication (q, p))
This is the simplest approach, in the Kolmogorov sense. The problem is that we lose information. Suppose this is the backend of some sort of interactive logic program: the user types a propositional formula in the REPL and has it echoed back at them. If we exhaustively expand complex connectives to their definitions at construction time, we worsen the output:
> (p > q) <> (r ∨ s)
it = ((¬(¬p ∨ q) ∨ (r ∨ s)) ∧ (¬(r ∨ s) ∨ (¬p ∨ q)))
Simplification
An alternative approach that preserves information is to define a datatype of formulae that includes cases for implication and biconditional implication, and simplify from there:
type atom = char
datatype formula = Atom of atom
 Negation of formula
 Conjunction of formula * formula
 Disjunction of formula * formula
 Implication of formula * formula
 Biconditional of formula * formula
What we want now is to have a simplification function which takes a formula and
removes nonprimitive logical connectives until only the primitive ones
remain. The problem with having a function simplify :: formula > formula
is
that we can’t be certain, at compile time, that the function actually removes
the superfluous connectives.
In dynamically typed languages, a common error when recurring down a
heterogeneous tree is forgetting to go deep enough: you forget to recur down the
subterms of a particular case, and the output of your transformation has
leftovers. The problem with these errors is they require extensive testing in
order to be discovered. As a motivating example, here’s an incorrect
implementation of simplify
in Common Lisp:
(defun simplify (formula)
(if (atom formula)
formula
(destructuringbind (f &rest args)
formula
(case f
(:~ `(:~ ,(simplify (first args))))
(:conj `(:conj ,(simplify (first args)) ,(simplify (second args))))
(:disj `(:disj ,(simplify (first args)) ,(simplify (second args))))
(:impl `(:disj (:~ ,(simplify (first args)))
,(simplify (second args))))
(:iff `(:conj (:implication ,(simplify (first args))
,(simplify (second args)))
(:implication ,(simplify (second args))
,(simplify (first args)))))))))
And here’s the error:
* (simplify '(:iff a b))
(:CONJ (:IMPLICATION A B) (:IMPLICATION B A))
We are left with unexpanded connectives, and it’s easy to see how this would cause errors further down the line, in code that assumes those connectives aren’t there.
The converse of this error is a style of defensive programming – typical of dynamicallytyped languages – where to prevent this type of error we add unnecessary recursion, usually in the tail position, to ensure, by brute force, that we’ve exhaustively expanded all subterms and there’s nothing left to transform.
A function simplify :: formula > formula
wouldn’t protect us from this
failure mode. To demonstrate, here’s the Standard ML version of the above
simplify
function:
fun simple (Atom a) = Atom a
 simple (Negation p) = Negation (simple p)
 simple (Conjunction (p, q)) = Conjunction (simple p, simple q)
 simple (Disjunction (p, q)) = Disjunction (simple p, simple q)
 simple (Implication (p, q)) = Disjunction (Negation (simple p), simple q)
 simple (Biconditional (p, q)) = Conjunction (Implication (simple p, simple q),
Implication (simple q, simple p))
The function typechecks, and is wrong in the same way as the above:
 simple (Biconditional (Atom #"a", Atom #"b"));
val it = Conjunction (Implication (Atom #,Atom #),Implication (Atom #,Atom #))
: formula
Reduced Formulae
To solve this problem, we define a new datatype of reduced or primitive formulae, that is, those which lack implication and biconditional implication. A function from the type of formulae to the type of reduced formulae prevents this whole category of errors:
(* Connective elimination *)
datatype rformula = RAtom of atom
 RNegation of rformula
 RConjunction of rformula * rformula
 RDisjunction of rformula * rformula
fun simplify (Atom a) = RAtom a
 simplify (Negation p) = RNegation (simplify p)
 simplify (Conjunction (p, q)) = RConjunction (simplify p, simplify q)
 simplify (Disjunction (p, q)) = RDisjunction (simplify p, simplify q)
 simplify (Implication (p, q)) = RDisjunction (RNegation (simplify p), simplify q)
 simplify (Biconditional (p, q)) = RConjunction (simplify (Implication (p, q)),
simplify (Implication (q, p)))
Normal Forms
Translating a formula into a normal form by carrying out equivalencepreserving transformations can simplify computation and theorem proving. The following two sections describe a way to transform primitive propositional formulae into Negation Normal Form, as a stepping stone to translating them into Conjunctive Normal Form.
Negation Normal Form
In Negation Normal Form, a negation can only be applied to an atom, so we add another type definition, that of formulae that are in NNF:
datatype nnf = NAtom of atom
 NNegation of atom
 NConjunction of nnf * nnf
 NDisjunction of nnf * nnf
Defining a new datatype for such a small change can seem overkill: the only
delta from rformula
is a negation is now only applied to an atom rather than
an arbitrary formula. It’s admittedly a small step, but it’s nevertheless
shrinking the space of possible formulae, and we know it preserves validity.
To convert an arbitrary formula to Negation Normal Form, we have to apply the following two rules:
 A negation of a conjunction is a disjunction of negations.
 A negation of a disjunction is a conjunctin of negations.
Implemented as follows:
fun nnf (RAtom a) = NAtom a
 nnf (RNegation (RAtom a)) = NNegation a
 nnf (RNegation (RNegation f)) = nnf f
 nnf (RNegation (RConjunction (p, q))) = nnf (RDisjunction (RNegation p, RNegation q))
 nnf (RNegation (RDisjunction (p, q))) = nnf (RConjunction (RNegation p, RNegation q))
 nnf (RConjunction (p, q)) = NConjunction(nnf p, nnf q)
 nnf (RDisjunction (p, q)) = NDisjunction(nnf p, nnf q)
Conjunctive Normal Form
In Conjunctive Normal Form, every formula is in the form of a conjunction of clauses, a clause being a disjunction of literals, and a literal being either an atom or its negation.
First, the types:
datatype cnf_literal = CNFAtom of atom
 CNFNegation of atom
type cnf_clause = cnf_literal list
type cnf = cnf_clause list
And, finally, the function to convert NNF to CNF:
fun cnf (NAtom a) = [[CNFAtom a]]
 cnf (NNegation a) = [[CNFNegation a]]
 cnf (NConjunction (p, q)) = cnf p @ cnf q
 cnf (NDisjunction (p, q)) = List.concat (List.map (fn b' => List.map (fn a' => a' @ b')
(cnf p))
(cnf q))
The first two cases are obvious, the third requires a little thinking, but the fourth case sticks out like a sore thumb. It is easily rewritten:
fun cartesian a b =
List.concat (List.map (fn b' => List.map (fn a' => a' @ b')
a)
b)
fun cnf (NAtom a) = [[CNFAtom a]]
 cnf (NNegation a) = [[CNFNegation a]]
 cnf (NConjunction (p, q)) = cnf p @ cnf q
 cnf (NDisjunction (p, q)) = cartesian (cnf p) (cnf q)
The distributive property is just a special case of the Cartesian product.
Conclusion
Use strong, static types. Use as many intermediate representations as needed to constrain the set of program states. Replace functions that raise exceptions on “impossible” cases with functions that process these intermediate representations.