1

我正在尝试在 Haskell 中使用sbv解决优化问题，但出现编译器错误。

解决方案是一个值列表，我有一个检查解决方案是否有效（约束）的函数，以及一个计算最小化数字的函数。

我在我的最小示例中收到此编译器错误：

/home/t/sbvExample/Main.hs:28:5: error:
    • No instance for (S.SymVal S.SBool)
        arising from a use of ‘Sl.length’
    • In the expression: Sl.length xs
      In an equation for ‘toNum’: toNum xs = Sl.length xs
   |
28 |     Sl.length xs
   |     ^^^^^^^^^^^^

这是代码：

{-# LANGUAGE ScopedTypeVariables #-} 
module Main (main) where

import qualified Data.SBV.List as Sl
import qualified Data.SBV as S


main :: IO ()
main = do
    result <- S.optimize S.Lexicographic help
    print result


help :: S.SymbolicT IO ()
help = do
    xs :: S.SList S.SBool <- S.sList "xs"
    S.constrain $ isValid xs
    S.minimize "goal" $ toNum xs


isValid :: S.SList S.SBool -> S.SBool
isValid xs =
    Sl.length xs S..> 0


toNum :: S.SList S.SBool -> S.SInteger
toNum xs =
    Sl.length xs

所以在这个愚蠢的最小示例中，我希望一个包含一个项目的列表。

为方便起见，我将其放在 Github 上，因此使用以下命令构建它：

git clone https://github.com/8n8/sbvExample
cd sbvExample
stack build
4

2 回答 2

3

从文档中SList：

请注意，符号列表不是符号项的列表，也就是说，情况并非如此，这SList a = [a]与人们在 haskell 列表/序列之后所期望的不同。AnSList是它自己的符号值，可能具有任意但有限的长度，并且在内部作为一个单元处理，而不是固定长度的项目列表。

因此，如果您要使用 an SList，那么您需要将其与常规Bools 一起使用，而不是SBools。

于 2020-04-09T16:50:49.707 回答
3

您收到此错误消息是因为没有 SymVal for 的实例SBool，只有 for Bool，并且S.length需要 aS.SList的SymVal值：

length :: SymVal a => SList a -> SInteger

您可以通过更改toNum并isValid接受 yS.SList Bool并将类型更改为xs来解决此问题S.SList Bool：

help :: S.SymbolicT IO ()
help = do
    xs :: S.SList Bool <- S.sList "xs"
    S.constrain $ isValid xs
    S.minimize "goal" $ toNum xs

isValid :: S.SList Bool -> S.SBool
isValid xs =
    Sl.length xs S..> 0

toNum :: S.SList Bool -> S.SInteger
toNum xs =
    Sl.length xs

您的isValidandtoNum函数也过于专业化，因为它们只需要一个SymVal类约束。以下是更通用的并且仍然可以编译：

isValid :: S.SymVal a => S.SList a -> S.SBool
toNum :: S.SymVal a => S.SList a -> S.SInteger

编辑

如果不是因为toNum没有进行类型检查，您还会看到它S.sList也没有进行类型检查，因为它的类型签名SymVal对返回的类型参数有一个约束S.SList：

sList :: SymVal a => String -> Symbolic (SList a)

删除isValidand toNum，只保留S.sList构造函数：

help = do
    xs :: S.SList S.SBool <- S.sList "xs"
    return ()

抛出此错误：

• No instance for (S.SymVal S.SBool)
    arising from a use of ‘S.sList’

在我看来，这更多地说明了实际问题。它只是表明，一个最小的例子有时可能更小，因此更有帮助。

于 2020-04-09T16:42:36.567 回答