Extending propositional logic to modal logic in Haskell

Question

I wrote code in Haskell to model sentence 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 that I should use classes instead. This way, I can easily add new language features to different modules later. The problem is that I don’t know exactly 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 error, of course, is in the definition of the conjunction. However, it is not clear to me how I could rewrite it so that it works.

Answer 1

This should work:

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

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

---

Perhaps you could let the vortex use explicit type-level functions and repeat over them:

 -- functor for plain formulae data FormulaF f = Prop {propName :: String} | Neg f | Conj ff | Disj ff | Impl ff | BiImpl ff -- 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 very convenient, since constructors such as F,M,Plain sometimes interfere. But, unlike type classes, you can use pattern matching here.

---

As another option, use 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