Nearest equivalent to Prolog atom or Lisp symbol in Haskell

Question

I'm trying to write a simple program for manipulating expressions in propositional calculus and would like a nice syntax for proposition variables (e.g. 'P or something).

Strings get the job done, but the syntax is misleading in this context and they permit inappropriate operations like ++.

Syntactically, I'd like to be able to write down something that does not "look quoted" visually (something like 'P is okay, though). In terms of the supported operations, I'd like to be able to determine whether two symbols are equal and to convert them into a string matching their name via show. I'd also like these things to be open (ADTs with only nullary constructors are similar in principle to symbols, but require all variants to be declared in advance).

Here's a toy example using strings where something symbol-like would be more appropriate.

type Var = String

data Proposition =
    Primitive Var |
    Negated Proposition |
    Implication Proposition Proposition

instance Show Proposition where
    show (Primitive p) = p
    show (Negated n) = "!" ++ show n
    show (Implication ant cons) = 
        "(" ++ show ant ++ "->" ++ show cons ++ ")"

main = putStrLn $ show $ Implication (Primitive "A") (Primitive "B")

Answer 1

Typically the way this is done in Haskell is by parameterizing over the type of symbols. So your example would become:

data Proposition a = 
    Primitive a |
    Negated (Proposition a) |
    Implication (Proposition a) (Proposition a)

which then leaves it up to the user to decide the best representation their symbols. This has advantages over LISP-like symbols: symbols intended for different purposes will not be mixed up, and data structures involving symbols now admit transformations over all the symbols, which are more useful than you realize. For example, Functor changes between symbol representations, and Monad models substitution.

(=<<) :: (a        ->      Proposition b)      -> Proposition a -> Proposition b
          ^                ^^^^^^^^^^^^^          ^^^^^^^^^^^^^        
substitute each free var   with an expression   in this expression

You can get a form of type-safe openness too:

implyOpen :: Proposition a -> Proposition b -> Proposition (Either a b)
implyOpen p q = Implication (Left <$> p) (Right <$> q)

Another fun trick is using a non-regular recursive type to model variable bindings in a type-safe way.

data Proposition a = 
    ... |
    ForAll (Proposition (Maybe a))

Here we have added one "free variable" to the inner proposition -- Primitive Nothing is the variable being quantified over. It may seem awkward at first, but when you get to coding it's bomb, because the types make it very hard to get it wrong.

bound is an excellent package for modelling expression languages based on this idea (and a few other tricks).