Generating Num (SBV a) instances "generically"

[andreasabel]

(This is my first attempt to use sbv.)

I am hitting an impossible in sbv-10.10 in the internal sh function:

$ git clone [email protected]:andreasabel/sbv-quarter-circle-puzzle.git
$ cd sbv-*
$ git checkout bug-impossible-sh
$ stack run
...
puzzle-two: SBV.SMT.SMTLib2.cvtExp.sh: impossible happened; can't translate: s5 + s8
CallStack (from HasCallStack):
  error, called at ./Data/SBV/SMT/SMTLib2.hs:1113:18 in sbv-10.10-BssX0E5CD3cIV1ObcQi2gZ:Data.SBV.SMT.SMTLib2

[andreasabel]

It seems like svb chokes on a use of sum: https://github.com/andreasabel/sbv-quarter-circle-puzzle/blob/4a5a629191595e189e7b3df009800f34a9a1e0e0/Main.hs#L117-L118

boardVal :: Integer -> Board -> SBV (Integer, Integer)
boardVal i = sum . concat . map (map (squareVal i))

However, in an other example I have used sum of SInteger.
So maybe the problem is here that I use sum with SBV (Integer, Integer) where I defined + in Num (Integer, Integer) pointwise?
(Officially, this should not be a problem since tuples are well supported, e.g. there is instance (SymVal a, SymVal b) => SymVal (a,b).)

[andreasabel]

Indeed, here is an shrinking to a use of sum:

import Data.SBV

type Val = (Integer, Integer)

instance Num Val where
  fromInteger i       = (i, 0)
  negate (x, y)       = (negate x, negate y)
  (x1, y1) + (x2, y2) = (x1 + x2, y1 + y2)
  (*)    = undefined
  abs    = undefined
  signum = undefined

type SVal = SBV Val

valVec :: Int -> Symbolic [SVal]
valVec n = mapM (\ k -> symbolic ("X" ++ show k)) [0..n-1]

main = satWith z3{ verbose = True } $ do
  v <- valVec 3
  pure $ sum v .== 1

[andreasabel]

This is my final shrinking, to just a use of + on tuples:

import Data.SBV

type Val = (Integer, Integer)

instance Num Val where
  fromInteger i       = (i, 0)
  (x1, y1) + (x2, y2) = (x1 + x2, y1 + y2)
  (*)    = undefined
  abs    = undefined
  negate = undefined
  signum = undefined

main = satWith z3{ verbose = True } $ do
  x :: SBV Val <- symbolic "x"
  y :: SBV Val <- symbolic "y"
  pure $ x + y .== 1

[LeventErkok]

Hi Andreas,

This is essentially a duplicate of #598

The main problem here is once you lift a value to an SBV level like you did with symbolic (which is perfectly fine), you also have to tell SBV how all the instances are lifted too. So, the "proper" way to code this would be:

import Data.SBV
import Data.SBV.Tuple

type Val = (Integer, Integer)

instance Num Val where
  fromInteger i       = (i, 0)
  (x1, y1) + (x2, y2) = (x1 + x2, y1 + y2)
  (*)    = undefined
  abs    = undefined
  negate = undefined
  signum = undefined

instance {-# OVERLAPPING #-} Num (SBV Val) where
  fromInteger i = literal (i, 0)
  v1 + v2       = tuple (v1^._1 + v2^._1, v1^._2 + v2^._2)
  (*)    = undefined
  abs    = undefined
  negate = undefined
  signum = undefined

main = sat $ do
  x :: SBV Val <- symbolic "x"
  y :: SBV Val <- symbolic "y"
  pure $ x + y .== 1

When I run this, I get:

*Main> main
Satisfiable. Model:
  x = (0,0) :: (Integer, Integer)
  y = (1,0) :: (Integer, Integer)

which is what you were expecting in the first place.

Now, I do agree that this is rather "esoteric" and requires a deeper understanding of how SBV lifts values. And perhaps there's a way to simplify the user experience here. I'd love to hear what you think to make it easier to use.

Bottom line: This is an unfortunate consequence of how arbitrary liftings work in SBV, and while I'd like to make it better, it is behaving as designed, as crappy as that design is.

[andreasabel]

Hello Levent,

thank you for your quick answer and the explanation.

Maybe the Num (SBV a) instance is too general? I guess the typical Haskeller trusts in the "if it type-checks, it works" paradigm, so getting a crash due to an invalid operation for a well-typed program is unexpected.

Would it make sense to restrict this instance to the types where it works correctly? E.g. I would have gotten an error "no instance for Num (SBV (Integer, Integer))" then.

sbv/Data/SBV/Core/Model.hs

Lines 1322 to 1329 in 720255d

	-- Num instance for symbolic words.
	instance (Ord a, Num a, SymVal a) => Num (SBV a) where
	fromInteger = literal . fromIntegral
	SBV x + SBV y = SBV (svPlus x y)
	SBV x * SBV y = SBV (svTimes x y)
	SBV x - SBV y = SBV (svMinus x y)
	-- Abs is problematic for floating point, due to -0; case, so we carefully shuttle it down
	-- to the solver to avoid the can of worms. (Alternative would be to do an if-then-else here.)

(Due to limited expressivity of the Haskell class system, this would probably lead to tons of boilerplate...)

[LeventErkok]

Thanks Andreas..

You're absolutely right that Num a => Num (SBV a) is way too general. But it does handle most of the basic types (WordN, IntN, Float, Double, Int, BigFloat..) out of the box, and I don't know how to define it for all the internal types without a lot of boilerplate. Maybe template-haskell can help? If you can pull that off (via template-haskell or not), I'd be thrilled to take a PR.

The other difficulty is that the instance Num Val definition needed to make this work isn't that easy to come up with. (The definition is easy enough, but you have to know exactly how the underlying type is lifted; which is probably too much to ask from an end-user. In fact, the whole point of SBV is that you don't need to know how that is done. But I digress.)

I'm open to enhancements here. Ideas/explorations/Pull-Requests are most welcome.

[LeventErkok]

I think we can close this ticket. I captured the exploration of removal of the Num a => Num (SBV a) instance in a separate ticket (#706). I'm not sure what the exact design there will be, but I think it's worthy of exploration.

[LeventErkok]

@andreasabel

Hi Andreas,

As of 9a90e88 the following program now gives a type error:

import Data.SBV

type Val = (Integer, Integer)

instance Num Val where
  fromInteger i       = (i, 0)
  (x1, y1) + (x2, y2) = (x1 + x2, y1 + y2)
  (*)    = undefined
  abs    = undefined
  negate = undefined
  signum = undefined

main = sat $ do
  x :: SBV Val <- symbolic "x"
  y :: SBV Val <- symbolic "y"
  pure $ x + y .== 1

yielding:

a.hs:29:12: error: [GHC-39999]
    • No instance for ‘Num (SBV Val)’ arising from a use of ‘+’
    • In the first argument of ‘(.==)’, namely ‘x + y’
      In the second argument of ‘($)’, namely ‘x + y .== 1’
      In a stmt of a 'do' block: pure $ x + y .== 1
   |
29 |   pure $ x + y .== 1
   |            ^

This is indeed better; thanks for noting that the general Num a => Num (SBV a) instance was way too general.

To "fix" this, one needs to write:

import Data.SBV.Tuple

instance Num (SBV Val) where
  fromInteger i = literal (i, 0)
  v1 + v2       = let (x1, y1) = untuple v1
                      (x2, y2) = untuple v2
                  in tuple (x1+x2, y1+y2)
  (*)    = undefined
  abs    = undefined
  negate = undefined
  signum = undefined

And the program will work as expected.

I'm curious if we can make this "easier." Clearly the Num Val instance and Num (SBV Val) instances "mimic" each other, though it definitely does need some internal knowledge of how SBV lifts values internally. (The use of Data.SBV.Tuple in this particular case; via untuple/tuple round-trip.)

I played around with the iso-deriving mechanism you mentioned, thought about generic-haskell, and even (though I'd like to avoid) use of TH. But I wasn't able to come up with a satisfying solution that makes writing these sorts of Num (SBV Val) instances easier.

You're an expert in generic programming; is there a solution to "mimic" a given instance (i.e., Num Val here) and create a related instance (i.e., Num (SBV Val) here). Clearly, this can't all be done by SBV itself: Your Num instance might've put 5 in fromIntegerinstead of 0 as the second component; or did some other stuff.) But it also feels like some automation can be provided. What sort of facilities I should look at? Perhaps some combination of TH and iso-deriving? I'd appreciate hearing your thoughts about this.

[andreasabel]

Thanks for further digging into this issue @LeventErkok.

You're an expert in generic programming;

You are flattering me. :-)
When it comes to Haskell, I unfortunately have zero experience with generic programming.
(When it comes to theory, I could lecture how to use hand-rolled universes to get generic programming for "free" with dependent types, but this is hardly helpful here...)

[LeventErkok]

Yeah, I was thinking about it myself and there doesn't seem to be an easy way to do this to lift an "existing" instance. Maybe via template-haskell, but I don't think the complexity is worth it.