Есть много вещей, которые могут происходить здесь, я сомневаюсь, что что-либо включает введение классов типов.(Необычная вещь, которая может появиться здесь, - это ГАДТ.) Следующее очень простое;он просто предназначен для того, чтобы заставить вас говорить то, что вы хотите, более четко ...
Вот полиморфный тип, подобный тому, который был у вас изначально.Поскольку он полиморфный, вы можете использовать что угодно для представления атомарных формул.
data Formula a = Atom a
| Negation (Formula a)
| Conjunction (Formula a) (Formula a) deriving (Show, Eq, Ord)
Вот функция, которая извлекает все подформулы:
subformulas (Atom a) = [Atom a]
subformulas (Negation p) = Negation p : subformulas p
subformulas (Conjunction p q) = Conjunction p q : (subformulas p ++ subformulas q)
Вот тип, который следует использовать, если вы нене размышляю над многими атомными утверждениями:
data Atoms = P | Q | R | S | T | U | V deriving (Show, Eq, Ord)
Вот несколько случайных помощников:
k p q = Conjunction p q
n p = Negation p
p = Atom P
q = Atom Q
r = Atom R
s = Atom S
x --> y = n $ k x (n y) -- note lame syntax highlighting
-- Main> ((p --> q) --> q)
-- Negation (Conjunction (Negation (Conjunction (Atom P) (Negation (Atom Q)))) (Negation (Atom Q)))
-- Main> subformulas ((p --> q) --> q)
-- [Negation (Conjunction (Negation (Conjunction (Atom P) (Negation (Atom Q)))) (Negation (Atom Q))),
-- Conjunction (Negation (Conjunction (Atom P) (Negation (Atom Q)))) (Negation (Atom Q)),
-- Negation (Conjunction (Atom P) (Negation (Atom Q))),
-- Conjunction (Atom P) (Negation (Atom Q)),Atom P,
-- Negation (Atom Q),Atom Q,Negation (Atom Q),Atom Q]
Позволяет создавать булевы атомы !:
t = Atom True
f = Atom False
-- Main> t --> f
-- Main> subformulas ( t --> f)
-- [Negation (Conjunction (Atom True) (Negation (Atom False))),
-- Conjunction (Atom True) (Negation (Atom False)),
-- Atom True,Negation (Atom False),Atom False]
Почему бы непростая функция оценки?
eval :: Formula Bool -> Bool
eval (Atom p) = p
eval (Negation p) = not (eval p)
eval (Conjunction p q) = eval p && eval q
несколько случайных результатов:
-- Main> eval (t --> f )
-- False
-- Main> map eval $ subformulas (t --> f)
-- [False,True,True,True,False]
Добавлено позже: обратите внимание, что Formula
- это Functor
с очевидным примером, который может быть выведенGHC, если вы добавите Functor к производному предложению и языковой прагме {-#LANGUAGE DeriveFunctor#-}
.Тогда вы можете использовать любую функцию f :: a -> Bool
в качестве присваивания значений истинности:
-- *Main> let f p = p == P || p == R
-- *Main> fmap f (p --> q)
-- Negation (Conjunction (Atom True) (Negation (Atom False)))
-- *Main> eval it
-- False
-- *Main> fmap f ((p --> q) --> r)
-- Negation (Conjunction (Negation (Conjunction (Atom True) (Negation (Atom False)))) (Negation (Atom True)))
-- *Main> eval it
-- True