擴展命題邏輯模態邏輯在Haskell

Question

我已經寫在Haskell一些代碼用於建模命題邏輯

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

然而，沒有此，延伸到模態邏輯由於數據類型是封閉自然方式。因此，我認爲我應該使用類而不是。這樣，我可以在以後的不同模塊中輕鬆添加新的語言功能。問題是我不完全知道如何編寫它。我想要類似以下的東西

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 

這個錯誤當然是在連詞的定義中。但是，我不清楚如何重寫它，以便它能夠正常工作。

Answer 1

這應該工作：

data Conjunction f = Conj f f 

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

但是，我不知道類型類是你想達到什麼樣的工具。

---

也許你可以給一掄到使用顯式類型級別函子和經常性過他們：

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

是的，這是不是非常方便，因爲構造如F,M,Plain礙事的時候。但是，不像類型類，你可以在這裏使用模式匹配。

---

作爲另一種選擇，使用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