nick8325 / quickspec

Equational laws for free
BSD 3-Clause "New" or "Revised" License
247 stars 24 forks source link

Seemingly contradictory laws #39

Closed isovector closed 4 years ago

isovector commented 4 years ago

I'm running quickspec and getting what appear to be contradictory laws. After pruning some of the output, I'm left with:

== Functions ==                  
      set :: Component Jar a -> a -> Setter Jar
     both :: Setter Jar -> Setter Jar -> Setter Jar

== Laws ==
  1. both s s2 = both s2 s         
  2. both s s = s
  -- elided, but no other laws regarding set
 15. both (set c x) (set c x) = both (set c y) (set c x)

If I understand this correctly, law 2 says we should be able to compress 15 down to:

 15*. set c x = both (set c y) (set c x)

Which states now that both is right-biased with respect to set. But law 1 says that both is commutative! From which we can derive something crazy:

  15**. set c x = set c y

This is true if set ignores its second argument, but it doesn't:

> let system = snd $ createEntity (Entity $ build @Jar Nothing Nothing Nothing Nothing Nothing) newSystem

> setEntity (Id 0) (set #jackes 9) system
Jar {jar = fromList [], jazz = fromList [], jim = fromList [], jackes = fromList [(0,9)], boop = fromList []}/1

> setEntity (Id 0) (set #jackes 10) system
Jar {jar = fromList [], jazz = fromList [], jim = fromList [], jackes = fromList [(0,10)], boop = fromList []}/1

Am I reading this wrong? Is this a bug in QuickSpec? Or maybe a bug in my observations? Any advice would be greatly appreciated.

isovector commented 4 years ago

Sorry -- stupid user error. My generator for Setter Jar wasn't ever generating set terms. Nice win for QuickSpec finding that :)