Conditions on list comprehension using Haskell and SBV

Question

I want to write a Haskell list comprehension with a condition on symbolic expressions (SBV). I reproduced the problem with the following small example.

import Data.SBV

allUs :: [SInteger] 
allUs = [0,1,2]  

f :: SInteger -> SBool 
f 0 = sTrue
f 1 = sFalse
f 2 = sTrue

someUs :: [SInteger] 
someUs = [u | u <- allUs, f u == sTrue]

with show someUs, this gives the following error

*** Data.SBV: Comparing symbolic values using Haskell's Eq class!
***
*** Received:    0 :: SInteger  == 0 :: SInteger
*** Instead use: 0 :: SInteger .== 0 :: SInteger
***
*** The Eq instance for symbolic values are necessiated only because
*** of the Bits class requirement. You must use symbolic equality
*** operators instead. (And complain to Haskell folks that they
*** remove the 'Eq' superclass from 'Bits'!.)

CallStack (from HasCallStack):
  error, called at ./Data/SBV/Core/Symbolic.hs:1009:23 in sbv-8.8.5-IR852OLMhURGkbvysaJG5x:Data.SBV.Core.Symbolic

Changing the condition into f u .== sTrue also gives an error

<interactive>:8:27: error:
    • Couldn't match type ‘SBV Bool’ with ‘Bool’
      Expected type: Bool
        Actual type: SBool
    • In the expression: f u .== sTrue
      In a stmt of a list comprehension: f u .== sTrue
      In the expression: [u | u <- allUs, f u .== sTrue]

How to get around this problem?

Answer 1

Neither your f nor your someUs are symbolically computable as written. Ideally, these should be type-errors, rejected out-of-hand. This is due to the fact that symbolic values cannot be instances of the Eq class: Why? Because determining equality of symbolic values requires a call to the underlying solver; so the result cannot be Bool; it should really be SBool. But Haskell doesn't allow generalized guards in pattern-matching to allow for that possibility. (And there are good reasons for that too, so it's not really Haskell's fault here. It's just that the two styles of programming don't work well all that great together.)

You can ask why SBV makes symbolic values an instance of the Eq class. The only reason why it's an instance of Eq is what the error message is telling you: Because we want them to be instances of the Bits class; which has Eq as a superclass requirement. But that's a whole another discussion.

Based on this, how can you write your functions in SBV? Here's how you'd code f in the symbolic style:

f :: SInteger -> SBool
f i = ite (i .== 0) sTrue
    $ ite (i .== 1) sFalse
    $ ite (i .== 2) sTrue
    $               sFalse   -- arbitrarily filled to make the function total

Ugly, but this is the only way to write it unless you want to play some quasi-quoting tricks.

Regarding someUs: This isn't something you can directly write symbolically either: This is known as a spine-concrete list. And there's no way for SBV to know how long your resulting list would be without actually running the solver on individual elements. In general you cannot do filter like functions on a spine-concrete list with symbolic elements.

The solution is to use what's known as a symbolic list and a bounded-list abstraction. This isn't very satisfactory, but is the best you can do to avoid termination problems:

{-# LANGUAGE OverloadedLists #-}

import Data.SBV
import Data.SBV.List
import Data.SBV.Tools.BoundedList

f :: SInteger -> SBool
f i = ite (i .== 0) sTrue
    $ ite (i .== 1) sFalse
    $ ite (i .== 2) sTrue
    $               sFalse   -- arbitrarily filled to make the function total

allUs :: SList Integer
allUs = [0,1,2]

someUs :: SList Integer
someUs = bfilter 10 f allUs

When I run this, I get:

*Main> someUs
[0,2] :: [SInteger]

But you'll ask what's that number 10 in the call to bfilter? Well, the idea is that all lists are assumed to have some sort of an upper bound on their length, and the Data.SBV.Tools.BoundedList exports a bunch of methods to deal with them easily; all taking a bound parameter. So long as the inputs are at most this length long, they'll work correctly. There's no guarantee as to what happens if your list is longer than the bound given. (In general it'll chop off your lists at the bound, but you should not rely on that behavior.)

There's a worked-out example of uses of such lists in coordination with BMC (bounded-model-checking) at https://hackage.haskell.org/package/sbv-8.12/docs/Documentation-SBV-Examples-Lists-BoundedMutex.html

To sum up, dealing with lists in a symbolic context comes with some costs in modeling and how much you can do, due to restrictions in Haskell (where Bool is a fixed type instead of a class), and underlying solvers, which cannot deal with recursively defined functions all that well. The latter is mainly due to the fact that such proofs require induction, and SMT-solvers cannot do induction out-of-the-box. But if you follow the rules of the game using BMC like ideas, you can handle practical instances of the problem up to reasonable bounds.

Answer 2

(.==) takes two instances of EqSymbolic, returning an SBool. Inside a list comprehension, conditionals are implemented using the guard function.

Here's what it looks like:

guard :: Alternative f => Bool -> f ()
guard False = empty
guard True = pure ()

For lists, empty is [], and pure () returns a singleton list [()]. Any member of the list that evaluates to False will return an empty list instead of a unit item, excluding it from computations down the chain.

[True, False, True] >>= guard
= concatMap guard [True, False, True]
= concat $ map guard [True, False, True]
= concat $ [[()], [], [()]]
= [(), ()]

The second branch is then excluded when the context is flattened, so it's "pruned" from the computation.

It seems like you have two problems here - when you pattern match in f, you're doing a comparison using the Eq class. That's where the SBV error is coming from. Since your values are close together, you could use select, which takes a list of items, a default, an expression which evaluates to an index, and attempt to take the indexth item from that list.

You could rewrite f as

f :: SInteger -> SBool
f = select [sTrue, sFalse, sTrue] sFalse

The second problem is that guards explicitly look for Bool, but (.==) still returns an SBool. Looking at Data.SBV, you should be able to coerce that into a regular Bool using unliteral, which attempts to unwrap an SBV value into an equivalent Haskell one.

fromSBool :: SBool -> Bool
fromSBool = fromMaybe False . unliteral

someUs :: [SInteger]
someUs = [u | u <- allUs, fromSBool (f u)]
-- [0 :: SInteger, 2 :: SInteger]