在解决SBV算法问题时如何避免IO单点

Question

我正试图用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不同的单点操作。这给了我希望，我们将达到一个更有用的单一，例如身份单。

不幸的是，查看示例总是解决IO monad中的问题，因此我找不到任何对me.Besides有用的示例，这些示例我没有使用monad的丰富经验。

最后，我的问题是：

在使用SBV解决这样的问题时，有什么方法可以避免IO单点吗？

提前感谢

Answer 1

SBV调用您选择的SMT解决程序(很可能是z3，但其他也可用)，并将结果返回给您。这意味着它在幕后执行IO，因此您不能在IO monad之外。您可以使用MonadSymbolic创建自定义monad，但这不会使您脱离IO monad:因为对SMT解决程序的调用是IO，所以您将始终处于IO中。

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

请注意，这与Haskell中任何其他基于IO的计算没有什么不同:您执行IO“in - the -包装”，但是一旦得到了结果，就可以在“纯”环境中对它们做任何您想做的事情。

下面是一个简单的例子：

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有IO ()类型，因为它确实涉及调用求解器并获得结果。但是，一旦提取出这些结果(通过对getValue的调用)，就可以将它们传递给函数use，该函数具有非常简单的纯函数类型。因此，您将“包装器”保存在单子中，但是实际的处理、使用--值等，仍然停留在纯世界中。

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

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单。它的存在有一个很好的理由。进入它，得到你的结果，然后你的其他程序可以保持纯功能，或任何其他你可能发现自己在其中。

请注意，所有这些都不是SBV特有的。这是常见的Haskell范式，说明如何使用副作用函数。(例如，只要您使用readFile读取文件的内容，就可以进一步处理它。)不要试图“摆脱IO”。相反，只需使用它。

Answer 2

根据函数的类型，我可以使用与IO不同的单点操作。

从你所希望的意义上来说，没有意义的不同。这个类的每个实例都将是IO的一些转换版本。抱歉的!

是时候制定一个包含理解和使用IO的计划了。