使用列表解决方案进行优化：编译器错误

Question

我正在尝试在 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

Answer 1

您收到此错误消息是因为 there is no instance of SymVal for SBool，仅适用于 Bool，而 S.length 需要 S.SList 的 SymVal 值：

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

您可以通过更改 toNum 和 isValid 以接受 y S.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

您的 isValid 和 toNum 函数也过于专业化，因为它们只需要 SymVal class 约束。下面是更通用的，仍然可以编译：

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)

删除isValid和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’

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

Answer 2

来自the documentation for SList：

Note that a symbolic list is not a list of symbolic items, that is, it is not the case that SList a = [a], unlike what one might expect following haskell lists/sequences. An SList is a symbolic value of its own, of possibly arbitrary but finite length, and internally processed as one unit as opposed to a fixed-length list of items.

因此，如果您要使用 SList，则需要将其与常规 Bool 一起使用，而不是 SBool。

使用列表解决方案进行优化：编译器错误

Optimisation with list solution: compiler error

haskell

sbv