This post contains Haskell snippets which after concatenation should result in a working Haskell program. Thus, here is a preamble with some language features and libraries we are going to use here:
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE FlexibleInstances #-}
module Main where
import Data.Foldable (toList)
import Data.Map (Map)
import qualified Data.Map as Map
Consider the following problem: given a boolean formula with variables, construct its truth table. Formulas are defined as the following datatype:
data F
= Var String
| F :&: F
| F :|: F
| Not F
| Const Bool
deriving (Show)
This problem is fairly straightforward to solve in two stages: first, traverse the formula in order to find all free variables, then evaluate the formula for each possible assignment of these variables.
However, since we already using Haskell why not complicate our lives even more and try to evaluate the truth table in a single traversal of the formula? The idea of the algorithm is simple enough: we can compute truth tables of subexpressions inductively:
For a constant, return a table of one row with that constant in value column.
For a variable X, return
| X | value |
|---|---|
| 0 | 0 |
| 1 | 1 |
For binary expressions, compute truth tables of subexpressions and then join the resulting tables by common columns, applying the corresponding function in value column.
Here is a question though, how do we represent the type of such a table in Haskell? A simple solution would look like that:
type Assignment = [(String, Bool)]
type SimpleTable = [(Assignment, Bool)]
But, as I've said before, this post is not about simple solutions. This representation particularly, does not enforce a lot of properties we want to be true, such as:
Assignment should have each variable only onceSimpleTable should have the same set of variablesWe can enforce last two of these using a nested type representation of truth table:
data Truth a
= Value a
| Fork String (Truth (a, a))
deriving (Show)
Nested types are somewhat mysterious and thus you might want to squint at it a bit to convince yourself that each value of Truth a contains exactly n strings and 2n values of type a. You can even prove it formally using an induction on number of Forks in the value.
First of all, let's learn how to convert value of this datatype to a regular truth table. This will be useful for printing the data, since automatically generated Show instance is not really human-readable.
The following code for conversion required some experimentation on my part which got me thinking about whether there is a good methodology for writing functions on nested types: while I find implementing recursive function on regular recursive datatypes fairly straightforward, functions on nested types I've written so far usually require some ad-hoc polymorphism, and it's not clear how to search which typeclasses one should use.
Anyway, while I can't explain how to come up with the following code, I can at least show another function that turned out to be useful as an inspiration: turns out, it's easy to implement a Foldable instance for Truth datatype:
instance Foldable Truth where
foldMap f = \case
Value v -> f v
Fork _ v -> foldMap (uncurry mappend . fork f) v
Note that this function essentially ignores all the String tags. We can write another foldMap-like function that does not ignore them, and use it in order to build the simple representation of truth table:
truthFold :: Monoid b => (a -> b) -> (Bool -> String -> b -> b) -> Truth a -> b
truthFold f1 f2 = \case
Value v -> f1 v
Fork s t -> truthFold (uncurry mappend . pointwise (f2 False s . f1, f2 True s . f1)) f2 t
trueTable :: Truth Bool -> SimpleTable
trueTable = truthFold (\b -> [([], b)]) (\k v ls -> map (onFirst ((v, k) :)) ls)
In the snippet above, we use a couple of helper functions which are all probably available in Control.Arrow, but I've found it easier to implement these myself rather than trying to remember which combination of squiggly lines corresponds to which function:
pointwise (f1, f2) (x, y) = (f1 x, f2 y)
fork f (x, y) = (f x, f y)
join (f1, f2) x = (f1 x, f2 x)
onFirst f (x, y) = (f x, y)
Now, on to the truth table construction part. Similarly how implementing Foldable turned out to be useful in order to get the function we need, it turned out that implementing Functor and Applicative turned out to be extremely useful when building the evaluation function. Here are the instances:
instance Functor Truth where
fmap f = \case
Value x -> Value (f x)
Fork t v -> Fork t $ fmap (fork f) v
instance Applicative Truth where
pure = Value
tf <*> tv = case (tf, tv) of
(Value f, Value v) -> Value (f v)
(Value f, Fork t v) -> Fork t $ fmap (fork f) v
(Fork t f, Value v) -> Fork t $ fmap (fork ($ v)) f
(Fork t1 f, Fork t2 v) -> case compare t1 t2 of
EQ -> Fork t1 (pointwise <$> f <*> v)
LT -> Fork t1 (join <$> f <*> tv)
GT -> Fork t2 (fork <$> tf <*> v)
While Functor instance is fairly straightforward, I have a couple of comments about Applicative instance. <*> operator does actually end up implementing the joining, and in order to make it somewhat efficient and avoid reshuffling the tags, we assume that the tags (String part of the Fork constructor) are in sorted order and maintain that sorted property while joining the tables.
Now that we have the join operation, time to implement the actual evaluator. For this, we would need a typeclass for "boolean-like" types, e.g. types we can lift boolean functions to. Observe:
class Boolean a where
liftBool :: (Bool -> Bool) -> a -> a
liftBool2 :: (Bool -> Bool -> Bool) -> a -> a -> a
instance Boolean Bool where
liftBool = id
liftBool2 = id
instance Boolean a => Boolean (a, a) where
liftBool f (x, y) = (liftBool f x, liftBool f y)
liftBool2 f (x, y) (z, w) = (liftBool2 f x z, liftBool2 f y w)
instance Boolean a => Boolean (Truth a) where
liftBool f = \case
Value v -> Value (liftBool f v)
Fork s inner -> Fork s (liftBool f inner)
liftBool2 f t1 t2 = liftBool2 f <$> t1 <*> t2
The final implementation then is a straightforward usage of that typeclass:
eval :: F -> Truth Bool
eval = \case
Const b -> Value b
Var v -> Fork v (Value (False, True))
Not f -> liftBool not (eval f)
f1 :&: f2 -> liftBool2 (&&) (eval f1) (eval f2)
f1 :|: f2 -> liftBool2 (||) (eval f1) (eval f2)
The implementation probably does not need this extra class, and can just use some traversals instead, but that's the code I ended up having for now.