Closed andreasabel closed 1 month ago
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)
.)
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
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
Hi Andreas,
This is essentially a duplicate of https://github.com/LeventErkok/sbv/issues/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.
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.
https://github.com/LeventErkok/sbv/blob/720255d2a843b146d248720036a986917ee62041/Data/SBV/Core/Model.hs#L1322-L1329
(Due to limited expressivity of the Haskell class system, this would probably lead to tons of boilerplate...)
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.
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 (https://github.com/LeventErkok/sbv/issues/706). I'm not sure what the exact design there will be, but I think it's worthy of exploration.
@andreasabel
Hi Andreas,
As of https://github.com/LeventErkok/sbv/commit/9a90e88787e9966616fcea0b1f29cab0d56a9dc4 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 fromInteger
instead 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.
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...)
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.
(This is my first attempt to use
sbv
.)I am hitting an impossible in
sbv-10.10
in the internalsh
function: