Holger Siegel holgersiegel74 at yahoo.de
Sat Jan 10 22:00:25 EST 2009

```On Sunday 11 January 2009 01:44:50 Andrew Wagner wrote:
> Nice Idea, though I don't know that I want something that extensive. I was
> more looking for whether there was a better way I could define the
> algebraic data type.

Let's have a look at your definitions from http://hpaste.org/13807#a1 :

> data Sentence = Atomic Atom | Complex Complex

The distinction between atomic expressions and complex expressions seems to be
Thus, I suggest that you move the constructors of type Atom and Complex to
type Sentence.

The only place where type Atom is used is in the following declaration:

> newtype Model = Model [Atom]

But a close look at function true :: Model -> Sentence -> Bool reveals that it
is sufficient to make a model a list of symbols. Therefore, we modify type Model
to

type Model = [Symbol]

If Symbol was an instance of type class Ord, we could even move from lists to
sets:

import qualified Data.Set as Set
type Model = Set.Set Symbol

Then function symbols could also return sets of symbols, allowing for a much
more efficient implementation via Set.union instead of List.nub and List.++:

symbols :: Sentence -> Set.Set Symbol

> data Atom = T | F | Symbol Symbol deriving Eq

In function symbols you need to distinguish between symbols and other values
of type Atom. With your current definition, function symbol must evaluate every
atom to a concrete truthvalue. We can avoid this by defining Atom as

data Atom = Const Bool | Symbol Symbol deriving Eq

> data Symbol = A | B | C | P | Q | R | X | Y | Z | Label String deriving Eq

1) There are two kinds of symbols, but there is no clear distinction between
them. Instead, String-type labels are modelled as one special case of a
symbol.
2) You enumerate characters explicitly. Instead, you could use type Char for
single-character symbols.

If you define symbols by

type Symbol = Either Char String

then you have a clear distinction between single-character symbols and labels,
and you also get the above-mentioned instance of typeclass Ord for free.

> data Complex = Not Sentence
>             | Sentence :/\: Sentence
>             | Sentence :\/: Sentence
>             | Sentence :=>: Sentence
>             | Sentence :<=>: Sentence

There are some opportunities to reduce the number of constructors in this
declaration. Constructor :=>: can easily be replaced by a function

(==>) :: Sentence -> Sentence -> Sentence
a ==> b  = Not a :/\: b

You can even define true, false, negation, conjunction and disjunction in terms
of a newly introduced constructor

Nand [Sentence]

so that

false = Nand []
true = Nand [false]

Operator <=> can also be expressed in terms of Nand, but that would lead to
duplicated work in function symbol and function true. Thus, we keep
constructor :<=>:.

The resulting declarations are

data Sentence = Nand [Sentence]
| Sentence :<=>: Sentence
| Symbol Symbol

type Symbol = Either Char String

type Model = Set.Set Symbol

This will reduce your boilerplate code to a minimum. :)

Regards,
Holger

```