Extending propositional logic to modal logic in Haskell

Question

I have written some code in Haskell for modeling propositional logic

data Formula = Prop {propName :: String} 
            | Neg Formula 
            | Conj Formula Formula 
            | Disj Formula Formula
            | Impl Formula Formula 
            | BiImpl Formula Formula 
    deriving (Eq,Ord)

However, there is no natural way to extend this to Modal Logic, since the data type is closed. Therefore, I thought I should use classes instead. That way, I can easily add new language features in different modules later on. The problem is that I don't exactly know how to write it. I would like something like the following

type PropValue = (String,Bool) -- for example ("p",True) states that proposition p is true
type Valuation = [PropValue]    

class Formula a where
    evaluate :: a -> Valuation -> Bool

data Proposition = Prop String

instance Formula Proposition where
    evaluate (Prop s) val = (s,True) `elem` val 

data Conjunction = Conj Formula Formula -- illegal syntax

instance Formula Conjunction where
    evaluate (Conj φ ψ) v = evaluate φ v && evaluate ψ v

The mistake is of course in the definition of Conjunction. However, it is unclear to me how I could rewrite it so that it works.

At

If you like reading, you may find this helpful. – Buenabuenaventura

Answer 1

This should work:

data Conjunction f = Conj f f

instance Formula f => Formula (Conjunction f) where
    evaluate (Conj φ ψ) v = evaluate φ v && evaluate ψ v

However, I am not sure type classes are the right tool for what you are trying to achieve.

---

Maybe you could give a whirl to using explicit type level functors and recurring over them:

-- functor for plain formulae
data FormulaF f = Prop {propName :: String} 
            | Neg f
            | Conj f f
            | Disj f f
            | Impl f f
            | BiImpl f f

-- plain formula
newtype Formula = F {unF :: FormulaF Formula}

-- functor adding a modality
data ModalF f = Plain f
             | MyModality f
-- modal formula
newtype Modal = M {unM :: ModalF Modal}

Yes, this is not terribly convenient since constructors such as F,M,Plain get sometimes in the way. But, unlike type classes, you can use pattern matching here.

---

As another option, use a GADT:

data Plain
data Mod
data Formula t where
   Prop {propName :: String} :: Formula t
   Neg  :: Formula t -> Formula t
   Conj :: Formula t -> Formula t -> Formula t
   Disj :: Formula t -> Formula t -> Formula t
   Impl :: Formula t -> Formula t -> Formula t
   BiImpl :: Formula t -> Formula t -> Formula t
   MyModality :: Formula Mod -> Formula Mod 

type PlainFormula = Formula Plain
type ModalFormula = Formula Mod

Gros

Thank you, your first solution seems to work. However, I will look into your other solutions as well, since I believe that data type contexts will be deprecated in the near future, see #7439100. GADT doesn't seem to be the solution I need, since I want to be able to define different operators in different modules. For example, the Conj and Disj operator in PropLogic.hs, the Box operator in ModalLogic.hs and the ForAll quantifier in PredLogic.hs. – At

@Anonymous data type context are indeed to be avoided, but I did not use them (nor you did). These contexts are those as in data (Ord a) => Set a = .... The contexts appearing in class or instance are not data type contexts and are not going away. – Gros