单子的应用

问：

下面的代码用于测试 2-SAT 布尔公式（仅包含 X v Y 形式的子句的公式）的满足性。尽管存在其他算法（相关隐含图的强连接组件，通过SLUR的文字赋值），但该程序通过递归应用解析来实现，直到找到一个空子句，即发现隐含矛盾。我已经注释了代码以解释它是如何工作的（以防万一）

尽管代码可以编译/工作，但我还是忍不住觉得它感觉有点“hacky”，并且可以通过使用 Monads 使其更像 Haskell。

-- Literals are numbered and are identified by their integer number X; -X represents a negated integer 
-- A 2-CNF clause X v Y  is represented by a tuple of a 2 integers (X,Y)  
-- 0 represents a empty space (i.e. a non existing literal). So (X,0) or (0,X) is a unit clause and (0,0) represents an empty clause

isEmptyClause :: (Int,Int) -> Bool
isEmptyClause c = (fst c == 0) && (snd c == 0) -- c denotes a clause. (0,0) is an empty clause

isUnitClause :: (Int,Int) -> Bool
isUnitClause c = not (c `isEmptyClause`) && (fst c ==0 || snd c == 0 || uncurry (==) c ) -- c denotes a clause. A unit clause has one literal. Three cases : (X,0)=(0,X)=(X,X)

isTautological :: (Int,Int) -> Bool
isTautological c = not (c `isEmptyClause`) && (fst c == - snd c) -- c denotes a clause. (X,-X) is a tautological clause as it is always true, thus meaningless

isSamePair :: (Int,Int) -> (Int,Int) -> Bool
isSamePair p p' = fst p == fst p' && snd p==snd p' || fst p==snd p' && snd p==fst p' -- p and p' denote a pair of integers, each in a tuple. NB : 2 cases (X,Y)=(X,Y)=(Y,X)

isIdentical :: (Int,Int) -> (Int,Int) -> Bool
isIdentical c d = c' `isSamePair` d' -- c and d denote clauses to be compared.
                where c' = checkHiddenUnitClause c ; d' = checkHiddenUnitClause d -- making sure that (X,X) => (X,0) for clauses c and d 

containsClause :: [(Int,Int)]-> (Int,Int) -> Bool
containsClause s c = any (isIdentical c) s -- s denotes a set of clauses and c denotes an individual clause

derivedClause :: (Int,Int) -> (Int,Int) -> (Int,Int) -- derived through resolution
derivedClause c c' -- c and c' denote clauses to be potentially resolved. resolution : AvB,-BvC => AvC. Four possible cases
    | fst c /=0 && fst c == - fst c' = (snd c,snd c') -- (X,Y), (-X,Z) => (Y,Z)
    | fst c /=0 &&fst c == - snd c' = (snd c,fst c') -- (X,Y), (Z,-X) => (Y,Z)
    | snd c /=0 && snd c == - fst c' = (fst c,snd c') -- (Y,X), (-X,Z) => (Y,Z)
    | snd c /=0 && snd c == - snd c' = (fst c,fst c') -- (Y,X), (Z,-X) => (Y,Z)
    | otherwise = (1,-1) -- this results in a tautological clause, and is thus harmless/meaningless. will be filtered out

derivedClauses :: (Int,Int) -> [(Int,Int)] -> [(Int,Int)] -- takes a clause and see if there are any resulting derived clauses by applying resolution to a set of clauses
derivedClauses c s = filter (not.isTautological) s' -- Any derivation that results in a tautological clause is filtered out of the derived set
                    where s' = map (derivedClause c) s -- c is a clause and s being a set of existing resulting clauses. the result s' is a derived set of clauses (from applying resolution)

-- Potentially a clause in the original clause set or any subsequently derived clause can be of the form (X,X), however because X v X => X : (X,X) => (X,0). 
-- getting clauses to the form (X,0) or (0,X) is essential if we ever want to find the empty clause (0,0) through resolution. Thus the clause may need to be rewritten as (X,0)
checkHiddenUnitClause :: (Int,Int)-> (Int,Int)
checkHiddenUnitClause c -- c denotes a clause.  
    | not (c `isUnitClause`) = c -- returns just the clause c if it is not a unit clause
    | fst c == 0 = c -- returns (0,X) if the unit clause is of the form (0,X)
    | otherwise = (fst c, 0) -- returns the unit clause in the form (X,0)

-- The following function expands the set of clauses by finding derived clauses (through resolution)
-- This recursive function does so by establishing a stack of existing clauses and a set of of resulting clauses
-- By "popping" the stack, clauses are assessed one by one and matched up against each of the resulting clauses for a possible derivation of a new clause (through resolution) 
-- The newly derived clauses are placed on the clause stack
-- The "popped" clause is added to the set of resulting clauses
-- the recursion terminates and unwinds, when the clause stack is emptied or when an empty clause is found in the clause stack (in which case the function results in an empty set)
expandClauseSet :: ([(Int,Int)],[(Int,Int)]) -> ([(Int,Int)], [(Int,Int)]) -- establishes a clause stack and a seperate set of resulting clauses
expandClauseSet ([],s) = ([], s) -- s is the set of resulting clauses. If the end of the clause stack is reached, the function returns the set of resulting clauses
expandClauseSet (c:cs,s) -- cs is the clause stack and c is the clause popped off the clause stack. s is the set of resulting clauses
    | (c `isEmptyClause`) = ([],[]) -- if an empty clause is found, return an empty clause stack and an empty set of resulting clauses
    | (c `isTautological`) || (s `containsClause` c') = expandClauseSet (cs, s) -- ignore the popped clause if it is tautological or already exists in the set of resulting clauses
    | otherwise = expandClauseSet (cs ++ derivedClauses c' s, c':s) -- add derived clauses to to the claus stack and add the popped clause to the set of resulting clauses
    where c' = checkHiddenUnitClause c -- this is to verify that the popped clauses is not actually a hidden unit clause. if so, modify it to a regular unit clause c'

expandedClauseSet :: [(Int,Int)] -> [(Int,Int)]
expandedClauseSet [] = []
expandedClauseSet s = snd (expandClauseSet (s,[])) -- s denotes a set of clauses

isSatisfiable :: [(Int,Int)] -> Bool
isSatisfiable s = expandedClauseSet s /= [] -- s denotes a set of clauses to be checked for satifiability

我可能会看到这种情况的三个领域，如果可以使用Monads：

1. 如果没有要应用的解析，该函数将返回一个同义子句;这似乎有点黑客。最好返回 Nothing 而不是。这是否意味着我应该用 monad 重写元组的所有实例，或者这应该是一个 Monoid（仍在与 monad tbh 作斗争）？derivedClause(Int,Int)Maybe

2. 每个子句都由一个元组表示，该元组表示子句中的两个文本。这很好，但也许有自己的定义会很好（也许我想要一些其他的字面定义而不是）。我正在尝试获得我自己类型的声明，例如：(Int,Int)Int

   data Clause = Clause {literal ::Int, otherLiteral :: Int)
   

   这在原则上应该有效，对吧？但是，在重构其余代码时，我会遇到很多类型错误。也许我只是错过了什么。这是值得追求的，还是更清楚的方式？另外，我想这与上一点有关，如果不存在的文字或空格可以用而不是数字 0 来表示，那不是更好吗？Nothing

3. 在我看来，递归函数处理其堆栈和结果列表的方式也非常像一个单子（结果列表是状态）。我这样想是对的，还是这把单子带得太远了？expandClauseSetState