# Computing truth tables using nested types

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

Xvalue
00
11
• 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:

• Every `Assignment` should have each variable only once
• Every element of `SimpleTable` should have the same set of variables
• Every possible combination of values should be present in the result

We 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 `Fork`s 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.