在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)

但是,由于数据类型已关闭,因此没有自然的方法将其扩展到Modal Logic.因此,我认为我应该使用类来代替.这样,我可以在以后轻松地在不同的模块中添加新的语言功能.问题是我不知道如何写它.我想要像下面这样的东西

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

错误当然是在Conjunction的定义中.但是,我不清楚如何重写它以使其有效.

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