0

我正在尝试用SBV解决算术问题。

例如

solution :: SymbolicT IO ()
solution =  do 
    [x, y] <- sFloats ["x", "y"]
    constrain $ x + y .<= 2

Main> s1 = sat solution
Main> s2 = isSatisfiable solution
Main> s1
Satisfiable. Model:
 x = -1.2030502e-17 :: Float
 z = -2.2888208e-37 :: Float
Main> :t s1
s1 :: IO SatResult
Main> s2
True
Main> :t s2
s2 :: IO Bool

虽然我可以做有用的事情，但我更容易使用纯值（SatResult 或 Bool）而不是 IO monad。

根据文档

sat :: Provable a => a -> IO SatResult
constrain :: SolverContext m => SBool -> m ()
sFloats :: [String] -> Symbolic [SFloat] 
type Symbolic = SymbolicT IO

鉴于我使用的函数类型，我理解为什么我总是使用 IO monad。

但是查看函数的通用版本，例如 sFloats。

sFloats :: MonadSymbolic m => [String] -> m [SFloat]

根据函数的类型，我可以使用与 IO 不同的 monad。这给了我希望，我们将获得一个更有用的 monad，例如 Identity monad。

不幸的是，查看示例总是可以解决 IO monad 中的问题，所以我找不到任何适合我的示例。此外，我没有太多使用 monad 的经验。

最后我的问题是：

在用 SBV 解决此类问题时，有什么方法可以避免 IO monad？

提前致谢

4

2 回答 2

2

SBV 调用您选择的 SMT 求解器（很可能是 z3，但也可以使用其他求解器），并将结果返回给您。这意味着它IO在引擎盖下执行，因此您不能在 IO monad 之外。您可以使用创建自定义 monad MonadSymbolic，但这不会让您摆脱IOmonad：因为调用 SMT 求解器，IO您将始终处于 IO.

（而且我强烈警告不要使用unsafePerformIO其中一条评论中的建议。这确实是一个坏主意；您可以在其他地方找到更多关于此的信息，为什么不应该这样做。）

请注意，这与 Haskell 中任何其他基于 IO 的计算没有什么不同：您在“包装内”执行 IO，但是一旦获得结果，您就可以在“纯“ 环境。

这是一个简单的例子：

import Data.SBV
import Data.SBV.Control

example :: IO ()
example =  runSMT $ do
    [x, y] <- sFloats ["x", "y"]
    constrain $ x + y .<= 2

    query $ do cs <- checkSat
               case cs of
                 Unsat -> io $ putStrLn "Unsatisfiable"
                 Sat   -> do xv <- getValue x
                             yv <- getValue y

                             let result = use xv yv

                             io $ putStrLn $ "Result: " ++ show result

                 _   -> error $ "Solver said: " ++ show cs

-- Use the results from the solver, in a purely functional way
use :: Float -> Float -> Float
use x y = x + y

现在你可以说：

*Main> example
Result: -Infinity

该函数example具有 type IO ()，因为它确实涉及调用求解器并获取结果。但是，一旦您提取了这些结果（通过调用getValue），您就可以将它们传递给use具有非常简单的纯函数类型的函数。因此，您将“包装器”保留在 monad 中，但实际处理、值的使用等仍保留在纯世界中。

或者，您也可以提取值并从那里继续：

import Data.SBV
import Data.SBV.Control

example :: IO (Maybe (Float, Float))
example =  runSMT $ do
    [x, y] <- sFloats ["x", "y"]
    constrain $ x + y .<= 2

    query $ do cs <- checkSat
               case cs of
                 Unsat -> pure Nothing
                 Sat   -> do xv <- getValue x
                             yv <- getValue y

                             pure $ Just (xv, yv)

                 _   -> error $ "Solver said: " ++ show cs

现在你可以说：

*Main> Just (a, b) <- example
*Main> a
-Infinity
*Main> b
4.0302105e-21

长话短说：不要回避 IO 单子。它的存在是有充分理由的。进入它，得到你的结果，然后你的程序的其余部分可以保持纯粹的功能，或者你可能发现自己的任何其他 monad。

请注意，这些都不是真正特定于 SBV 的。这是如何使用具有副作用的函数的常用 Haskell 范例。（例如，任何时候您使用readFile读取文件的内容来进一步处理它。）不要试图“摆脱 IO”。相反，只需使用它。

于 2021-09-26T18:43:54.530 回答
0

根据函数的类型，我可以使用与 IO 不同的 monad。

在你希望的意义上，没有有意义的不同。此类的每个实例都将是IO. 对不起！

是时候制定一个涉及理解和合作的计划了IO。

于 2021-09-26T16:58:04.450 回答