Оптимизация с помощью списка решений: ошибка компилятора - PullRequest
Новая
       25

Оптимизация с помощью списка решений: ошибка компилятора

1 голос
/ 09 апреля 2020

Я пытаюсь решить проблему оптимизации с помощью sbv в Haskell, но получаю ошибку компилятора.

Решением является список значений, и у меня есть функция проверить правильность решения (ограничение) и функцию для вычисления числа, которое нужно минимизировать.

Я получаю эту ошибку компилятора на своем минимальном примере: 

/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

Ответы [ 2 ]

3 голосов
/ 09 апреля 2020

С документация для SList:

Обратите внимание, что список символов c не список символов c элементов то есть, это не тот случай, когда SList a = [a], в отличие от того, что можно ожидать после haskell списков / последовательностей. SList является собственным значением symboli c, возможно произвольной, но конечной длины, и внутренне обрабатывается как одна единица, в отличие от списка элементов фиксированной длины.

Так что если вы собираетесь использовать SList, тогда вам нужно использовать его с обычными Bool с, а не SBool с.

3 голосов
/ 09 апреля 2020

Вы получаете это сообщение об ошибке, потому что нет экземпляра SymVal для 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 также не выполняет проверку типов, поскольку его сигнатура типа имеет ограничение 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’

Что, на мой взгляд, говорит немного больше о фактической проблеме. Это просто говорит о том, что минимальный пример иногда может быть еще более минимальным и, следовательно, более полезным.

...