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

【问题标题】：Optimisation with list solution: compiler error使用列表解决方案进行优化：编译器错误
【发布时间】：2020-04-09 16:11:15
【问题描述】：

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

【问题讨论】：

标签： haskell sbv

【解决方案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 类约束。以下是更通用的并且仍然可以编译：

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

编辑

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

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’

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

【讨论】：

【解决方案2】：

来自the documentation for SList：

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

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

【讨论】：