estensione logica proposizionale alla logica modale in Haskell

Question

Ho scritto un certo codice in Haskell per la modellazione logica proposizionale

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

Tuttavia, non v'è alcun modo naturale per estendere questo al modale logica, dal momento che il tipo di dati è chiuso. Pertanto, ho pensato di utilizzare invece le classi. In questo modo, posso aggiungere facilmente nuove funzionalità linguistiche in diversi moduli in seguito. Il problema è che non so esattamente come scriverlo. Vorrei qualcosa di simile al seguente

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 

L'errore è ovviamente nella definizione di Congiunzione. Tuttavia, non è chiaro per me come potrei riscriverlo in modo che funzioni.

Answer 1

Questo dovrebbe funzionare:

data Conjunction f = Conj f f 

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

Tuttavia, non sono sicuro classi di tipo sono lo strumento giusto per ciò che si sta cercando di ottenere.

---

Forse si potrebbe dare un vortice di utilizzare funtori livello di tipo esplicito e ricorrenti su di loro:

-- 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} 

Sì, questo non è molto conveniente in quanto i costruttori quali F,M,Plain ottengono a volte in mezzo. Tuttavia, a differenza delle classi di tipi, puoi utilizzare la corrispondenza dei modelli qui.

---

Come ulteriore opzione, utilizzare un 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