Mở rộng logic mệnh đề để modal logic trong Haskell

Question

Tôi đã viết một số mã trong Haskell để mô hình hóa logic mệnh đề

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

Tuy nhiên, không có cách nào tự nhiên để mở rộng này để phương thức logic, vì kiểu dữ liệu được đóng lại. Vì vậy, tôi nghĩ tôi nên sử dụng các lớp học thay thế. Bằng cách đó, tôi có thể dễ dàng thêm các tính năng ngôn ngữ mới trong các mô-đun khác nhau sau này. Vấn đề là tôi không biết chính xác cách viết nó. Tôi muốn một cái gì đó như sau

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 

Sai lầm là tất nhiên trong định nghĩa của Liên từ. Tuy nhiên, không rõ ràng với tôi làm thế nào tôi có thể viết lại nó để nó hoạt động.

Answer 1

này nên làm việc:

data Conjunction f = Conj f f 

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

Tuy nhiên, tôi không phải các lớp học kiểu chắc chắn là công cụ phù hợp với những gì bạn đang cố gắng để đạt được.

---

Có lẽ bạn có thể cung cấp một whirl để sử dụng functors cấp loại rõ ràng và định kỳ qua chúng:

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

Vâng, đây không phải là terribly tiện lợi vì nhà xây dựng như F,M,Plain có được đôi khi trong đường đi. Tuy nhiên, không giống như các loại lớp, bạn có thể sử dụng mẫu khớp tại đây.

---

Như một tùy chọn, sử dụng một 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