rudymatela/speculate

Speculate laws about Haskell functions

speculate's Issues

document what instances must be given

It is not clear what reified instances have to be added. The examples show that Int and Bool are built in, but some other types are not. Which, exactly?

I was assuming that it works for all instances that are known to leancheck, including Test.LeanCheck.Util.Types.Nat, but it does not.

I now assume that it works for all types that have instances of Name.
https://hackage.haskell.org/package/speculate-0.4.2/docs/Test-Speculate.html#t:Name

Does not find Functor Composition Law

Providing fmap, id, and . to Speculate results in

_ :: Int  (holes: Int)
_ :: [Int]  (holes: [Int])
fmap :: (Int -> Int) -> [Int] -> [Int]
id :: Int -> Int
(.) :: (Int -> Int) -> (Int -> Int) -> Int -> Int

             id x == x
      (id . id) x == x
       fmap id xs == xs
fmap (id . id) xs == xs

which misses

fmap f . fmap g == fmap (f . g)

TypeApplications for shorter/nicer code

1. (no code change, but update example) The example has

 , constant "+"   ((+)  :: Int -> Int -> Int)

I think this looks much nicer

{-# language TypeApplications #-}
...
 , constant "+"   ((+)  @Int)

2. (code change) currently, we need a proxy argument

  , instances = [ reifyListable (0::N), ...

the "proxy" role could be made more clear by writing undefined::N, or by Proxy :: Proxy N, but I think this would be best:

  , instances = [ reifyListable @N, ...

This might require AllowAmbiguousTypes.

Test build failure on stackage nightly

Preprocessing test suite 'expr' for speculate-0.2.6..
Building test suite 'expr' for speculate-0.2.6..

<no location info>: warning: [-Wmissing-home-modules]
    These modules are needed for compilation but not listed in your .cabal file's other-modules: Test.Speculate
                                                                                                 Test.Speculate.Args
                                                                                                 Test.Speculate.CondReason
                                                                                                 Test.Speculate.Engine
                                                                                                 Test.Speculate.Expr
                                                                                                 Test.Speculate.Expr.Canon
                                                                                                 Test.Speculate.Expr.Core
                                                                                                 Test.Speculate.Expr.Equate
                                                                                                 Test.Speculate.Expr.Ground
                                                                                                 Test.Speculate.Expr.Instance
                                                                                                 Test.Speculate.Expr.Match
                                                                                                 Test.Speculate.Pretty
                                                                                                 Test.Speculate.Reason
                                                                                                 Test.Speculate.Reason.Order
                                                                                                 Test.Speculate.Report
                                                                                                 Test.Speculate.Sanity
                                                                                                 Test.Speculate.SemiReason
                                                                                                 Test.Speculate.Utils
                                                                                                 Test.Speculate.Utils.Class
                                                                                                 Test.Speculate.Utils.Colour
                                                                                                 Test.Speculate.Utils.Digraph
                                                                                                 Test.Speculate.Utils.List
                                                                                                 Test.Speculate.Utils.Memoize
                                                                                                 Test.Speculate.Utils.Misc
                                                                                                 Test.Speculate.Utils.Ord
                                                                                                 Test.Speculate.Utils.PrettyPrint
                                                                                                 Test.Speculate.Utils.String
                                                                                                 Test.Speculate.Utils.Tiers
                                                                                                 Test.Speculate.Utils.Timeout
                                                                                                 Test.Speculate.Utils.Tuple
                                                                                                 Test.Speculate.Utils.Typeable
[ 1 of 33] Compiling Test.Speculate.Utils.Colour ( src/Test/Speculate/Utils/Colour.hs, dist/build/expr/expr-tmp/Test/Speculate/Utils/Colour.o )
[ 2 of 33] Compiling Test.Speculate.Utils.List ( src/Test/Speculate/Utils/List.hs, dist/build/expr/expr-tmp/Test/Speculate/Utils/List.o )
[ 3 of 33] Compiling Test.Speculate.Utils.Class ( src/Test/Speculate/Utils/Class.hs, dist/build/expr/expr-tmp/Test/Speculate/Utils/Class.o )
[ 4 of 33] Compiling Test.Speculate.Utils.Memoize ( src/Test/Speculate/Utils/Memoize.hs, dist/build/expr/expr-tmp/Test/Speculate/Utils/Memoize.o )
[ 5 of 33] Compiling Test.Speculate.Utils.Ord ( src/Test/Speculate/Utils/Ord.hs, dist/build/expr/expr-tmp/Test/Speculate/Utils/Ord.o )
[ 6 of 33] Compiling Test.Speculate.Utils.PrettyPrint ( src/Test/Speculate/Utils/PrettyPrint.hs, dist/build/expr/expr-tmp/Test/Speculate/Utils/PrettyPrint.o )
[ 7 of 33] Compiling Test.Speculate.Utils.String ( src/Test/Speculate/Utils/String.hs, dist/build/expr/expr-tmp/Test/Speculate/Utils/String.o )
[ 8 of 33] Compiling Test.Speculate.Utils.Misc ( src/Test/Speculate/Utils/Misc.hs, dist/build/expr/expr-tmp/Test/Speculate/Utils/Misc.o )
[ 9 of 33] Compiling Test.Speculate.Utils.Tiers ( src/Test/Speculate/Utils/Tiers.hs, dist/build/expr/expr-tmp/Test/Speculate/Utils/Tiers.o )
[10 of 33] Compiling Test.Speculate.Utils.Timeout ( src/Test/Speculate/Utils/Timeout.hs, dist/build/expr/expr-tmp/Test/Speculate/Utils/Timeout.o )
[11 of 33] Compiling Test.Speculate.Utils.Tuple ( src/Test/Speculate/Utils/Tuple.hs, dist/build/expr/expr-tmp/Test/Speculate/Utils/Tuple.o )
[12 of 33] Compiling Test.Speculate.Utils.Typeable ( src/Test/Speculate/Utils/Typeable.hs, dist/build/expr/expr-tmp/Test/Speculate/Utils/Typeable.o )
[13 of 33] Compiling Test.Speculate.Utils ( src/Test/Speculate/Utils.hs, dist/build/expr/expr-tmp/Test/Speculate/Utils.o )
[14 of 33] Compiling Test.Speculate.Utils.Digraph ( src/Test/Speculate/Utils/Digraph.hs, dist/build/expr/expr-tmp/Test/Speculate/Utils/Digraph.o )
[15 of 33] Compiling Test.Speculate.Expr.Core ( src/Test/Speculate/Expr/Core.hs, dist/build/expr/expr-tmp/Test/Speculate/Expr/Core.o )
[16 of 33] Compiling Test.Speculate.Expr.Match ( src/Test/Speculate/Expr/Match.hs, dist/build/expr/expr-tmp/Test/Speculate/Expr/Match.o )
[17 of 33] Compiling Test.Speculate.Expr.Instance ( src/Test/Speculate/Expr/Instance.hs, dist/build/expr/expr-tmp/Test/Speculate/Expr/Instance.o )
[18 of 33] Compiling Test.Speculate.Expr.Equate ( src/Test/Speculate/Expr/Equate.hs, dist/build/expr/expr-tmp/Test/Speculate/Expr/Equate.o )
[19 of 33] Compiling Test.Speculate.Expr.Ground ( src/Test/Speculate/Expr/Ground.hs, dist/build/expr/expr-tmp/Test/Speculate/Expr/Ground.o )
[20 of 33] Compiling Test.Speculate.Expr.Canon ( src/Test/Speculate/Expr/Canon.hs, dist/build/expr/expr-tmp/Test/Speculate/Expr/Canon.o )
[21 of 33] Compiling Test.Speculate.Expr ( src/Test/Speculate/Expr.hs, dist/build/expr/expr-tmp/Test/Speculate/Expr.o )
[22 of 33] Compiling Test.Speculate.Sanity ( src/Test/Speculate/Sanity.hs, dist/build/expr/expr-tmp/Test/Speculate/Sanity.o )
[23 of 33] Compiling Test.Speculate.Reason.Order ( src/Test/Speculate/Reason/Order.hs, dist/build/expr/expr-tmp/Test/Speculate/Reason/Order.o )
[24 of 33] Compiling Test.Speculate.Reason ( src/Test/Speculate/Reason.hs, dist/build/expr/expr-tmp/Test/Speculate/Reason.o )
[25 of 33] Compiling Test.Speculate.SemiReason ( src/Test/Speculate/SemiReason.hs, dist/build/expr/expr-tmp/Test/Speculate/SemiReason.o )
[26 of 33] Compiling Test.Speculate.CondReason ( src/Test/Speculate/CondReason.hs, dist/build/expr/expr-tmp/Test/Speculate/CondReason.o )
[27 of 33] Compiling Test.Speculate.Pretty ( src/Test/Speculate/Pretty.hs, dist/build/expr/expr-tmp/Test/Speculate/Pretty.o )
[28 of 33] Compiling Test.Speculate.Engine ( src/Test/Speculate/Engine.hs, dist/build/expr/expr-tmp/Test/Speculate/Engine.o )
[29 of 33] Compiling Test.Speculate.Args ( src/Test/Speculate/Args.hs, dist/build/expr/expr-tmp/Test/Speculate/Args.o )
[30 of 33] Compiling Test.Speculate.Report ( src/Test/Speculate/Report.hs, dist/build/expr/expr-tmp/Test/Speculate/Report.o )
[31 of 33] Compiling Test.Speculate   ( src/Test/Speculate.hs, dist/build/expr/expr-tmp/Test/Speculate.o )
[32 of 33] Compiling Test             ( tests/Test.hs, dist/build/expr/expr-tmp/Test.o )
[33 of 33] Compiling Main             ( tests/test-expr.hs, dist/build/expr/expr-tmp/Main.o )

<no location info>: warning: [-Wmissing-home-modules]
    These modules are needed for compilation but not listed in your .cabal file's other-modules: Test.Speculate
                                                                                                 Test.Speculate.Args
                                                                                                 Test.Speculate.CondReason
                                                                                                 Test.Speculate.Engine
                                                                                                 Test.Speculate.Expr
                                                                                                 Test.Speculate.Expr.Canon
                                                                                                 Test.Speculate.Expr.Core
                                                                                                 Test.Speculate.Expr.Equate
                                                                                                 Test.Speculate.Expr.Ground
                                                                                                 Test.Speculate.Expr.Instance
                                                                                                 Test.Speculate.Expr.Match
                                                                                                 Test.Speculate.Pretty
                                                                                                 Test.Speculate.Reason
                                                                                                 Test.Speculate.Reason.Order
                                                                                                 Test.Speculate.Report
                                                                                                 Test.Speculate.Sanity
                                                                                                 Test.Speculate.SemiReason
                                                                                                 Test.Speculate.Utils
                                                                                                 Test.Speculate.Utils.Class
                                                                                                 Test.Speculate.Utils.Colour
                                                                                                 Test.Speculate.Utils.Digraph
                                                                                                 Test.Speculate.Utils.List
                                                                                                 Test.Speculate.Utils.Memoize
                                                                                                 Test.Speculate.Utils.Misc
                                                                                                 Test.Speculate.Utils.Ord
                                                                                                 Test.Speculate.Utils.PrettyPrint
                                                                                                 Test.Speculate.Utils.String
                                                                                                 Test.Speculate.Utils.Tiers
                                                                                                 Test.Speculate.Utils.Timeout
                                                                                                 Test.Speculate.Utils.Tuple
                                                                                                 Test.Speculate.Utils.Typeable
Linking dist/build/expr/expr ...
> /tmp/stackage-build14/speculate-0.2.6$ dist/build/expr/expr
*** Failed tests:[114]

This looks strange. I'll look into it too.

Incorrect equations when size limit is increased.

@barrucadu reports an issue when applying Speculate to DejaFu:

• speculate -t20000 -s5: doesn't find any equalities, only conditional equations.

• speculate -t20000 -s6: finds these equalities:

                          isBlock ta == isBlock ta'
    (isBarrier a == isCommit a crid) == (False == synchronises a crid)
  

  (isBarrier a == synchronises a crid) == (False == isCommit a crid)
  ...

Property 1 is wrong. Something gets weird with ThreadActions ("ta") when the size is increased, even though the number of tests remains the same.

Provide module for treating functions as test values.

Code is repeated across the fun and monad examples. The repeated functionality should be provided by a module.

Maybe:

• Test.Speculate.Function with:
• Test.Speculate.Function.T100 and;
• Test.Speculate.Function.T1000.

Do newtypes need special handling?

I am using speculate to try to discover laws about Patterns in tidalcycles (https://hackage.haskell.org/package/tidal-1.7.1)

Since Pattern a is a data type similar to a function, I am using a newtype wrapper for which I implemented Listable, Eq and Show.

import qualified Sound.Tidal.Context as T

instance Listable a => Listable (T.TPat a) where
  tiers =
    cons1 T.TPat_Seq
      \/ cons2 (\x y -> T.TPat_Elongate ((abs x + 1) % 1) y)
      \/ cons2 T.TPat_Atom

newtype MyPattern a = MyPattern {pat :: T.Pattern a}

instance (T.Enumerable a, T.Parseable a, Listable a) => Listable (MyPattern a) where
  list = map (MyPattern . T.toPat) list -- [T.TPat a] here

instance Eq a => Eq (MyPattern a) where
  MyPattern p1 == MyPattern p2 = T.queryArc p1 (T.Arc 0 1) == T.queryArc p2 (T.Arc 0 1)

instance Show a => Show (MyPattern a) where
  show (MyPattern p) = show $ T.queryArc p (T.Arc 0 1)

when I run speculate as following:

main :: IO ()
main = do
  speculate
    args
      { constants =
          [ constant "fast" (fast :: MyPattern Rational -> MyPattern Int -> MyPattern Int),
            constant "slow" (slow :: MyPattern Rational -> MyPattern Int -> MyPattern Int)
          ]
      }

I get the following Warnings:

Warning: no Listable instance for MyPattern Int, variables of this type will not be considered
Warning: no Listable instance for MyPattern (Ratio Integer), variables of this type will not be considered
Warning: no Eq instance for MyPattern Int, equations of this type will not be considered
Warning: no Eq instance for MyPattern (Ratio Integer), equations of this type will not be considered
Warning: no Ord instance for MyPattern Int, inequations of this type will not be considered
Warning: no Ord instance for MyPattern (Ratio Integer), inequations of this type will not be considered

Are these Warnigns due to the newtype, or am I missing something completely different?

stackage nightly - speculate-0.4.14 - test build fails

Building test suite 'expr' for speculate-0.4.14..
       [3 of 3] Compiling Main [Test.Speculate.Expr package changed]

       /home/curators/work/unpack-dir/unpacked/speculate-0.4.14-a8408cae222a1f8c74752f8e9630227bd3653010805e5b3e275f1d022d2baab2/test/expr.hs:42:29: error: [GHC-87543]
           Ambiguous occurrence ‘ff2’.
           It could refer to
              either ‘Test.ff2’,
                     imported from ‘Test’ at test/expr.hs:2:1-11
                     (and originally defined in ‘Data.Express.Fixtures’),
                  or ‘Main.ff2’, defined at test/expr.hs:62:1.
          |
       42 |   , unification (hh5 yy zz (ff2 ii ii) (ff2 jj jj) kk) (hh5 (ff2 xx xx) (ff2 yy yy) jj kk zz)
          |

Basic `Listable` instances for composite types

Hi, I'm just trying out the tool for the first time, and I'm confused as to why it isn't working for a simple example. Here's the example code:

module Dominoes (chain, initState, isCyclic, search, insert, remove, State, Domino) where

import Data.Map (Map)
import Data.Tuple (swap)

import qualified Data.List as L
import qualified Data.Map as M
import qualified Data.Maybe as MB

type Domino = (Int, Int)
type State = ([Domino], Map Int [Int])

chain :: [Domino] -> Maybe [Domino]
chain = search . initState

initState :: [Domino] -> State
initState = foldr insert ([], M.empty)

isCyclic :: [Domino] -> Bool
isCyclic []  = True
isCyclic [(a, b)] = a == b
isCyclic ((a, _) : ds) = a == (snd . last $ ds)

search :: State -> Maybe [Domino]
search ([], _) = Just []
search (ds, m) = L.find isCyclic . MB.mapMaybe (go (ds, m)) $ ds ++ map swap ds
  where
    go :: State -> Domino -> Maybe [Domino]
    go state d = (d :) <$> search (remove d state)

insert :: Domino -> State -> State
insert (a, b) (ds, m) = ((a, b) : ds, M.insertWith (++) b [a] . M.insertWith (++) a [b] $ m)

remove :: Domino -> State -> State
remove (a, b) (ds, m) = (L.delete (a, b) ds, M.alter (fmap (L.delete b)) a . M.alter (fmap (L.delete a)) b $ m)

import Test.Speculate (speculate, constant, constants, instances, args, reifyInstances, showConstant, Name (..))

import Data.Map (Map)
import qualified Data.Map as M

import Dominoes (chain, insert, remove, State, Domino)

instance Name (Map a b) where
  name m = "map"

main :: IO ()
main = speculate args
  { instances = [ reifyInstances (undefined :: [(Int, Int)])
                , reifyInstances (undefined :: Map Int [Int])
                , reifyInstances (undefined :: State)
                ]
  , constants =
    [ showConstant (([], M.empty) :: State)
    , constant "insert" (insert :: Domino -> State -> State)
    ]
  }

/home/mal/pkgs/exercism/haskell/dominoes/Experiments.hs:14:19: error:
    • No instance for (leancheck-0.9.12:Test.LeanCheck.Core.Listable
                         (Map Int [Int]))
        arising from a use of ‘reifyInstances’
    • In the expression: reifyInstances (undefined :: Map Int [Int])
      In the ‘instances’ field of a record
      In the first argument of ‘speculate’, namely
        ‘args
           {instances = [reifyInstances (undefined :: [(Int, Int)]),
                         reifyInstances (undefined :: Map Int [Int]),
                         reifyInstances (undefined :: State)],
            constants = [showConstant (([], M.empty) :: State),
                         constant "insert" (insert :: Domino -> State -> State)]}’
   |
14 |                 , reifyInstances (undefined :: Map Int [Int])
   |                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Progress 1/2

Any idea why it's saying there's no Eq instance for these types? I would expect the Listable instance to be inferrable. 🤷🏻‍♀️

Okay, I didn't realize I should be using reifyInstances, but I've run into a problem with Map which I'm unsure about. Any tips?

Speculate on DejaFu: `speculate: could not find Listable Thread D1 D1`

The attached file (Main.hs.txt) applies Speculate to DejaFu. When it is run, Speculate reports an error:

speculate: could not find Listable Thread D1 D1
CallStack (from HasCallStack):
  error, called at src/Test/Speculate/Expr/Instance.hs:194:27 in speculate-0.2.9-...

See full log here.

That definitely seems like a bug.

Thanks to @barrucadu for discovering this.

Grading functions

Would this be helpful in finding an optimized function for a or giving insight to nonlinear grading function?

output of theorems should be lazy, but is not, because of alignment

For larger values of maxSize, I have to wait a looong time to see anything, in the output of speculate.

I was hoping that theorems are printed as they are discovered. But I think they are all held until the end - for computing the alignment. (report calls prettyEquations calls table which wants to see all words)

A work-around (I guess) is to call finalEquations directly, but then I have to copy code out of report.

Assuming the above is true (the lazy list of theorems is available),
perhaps Args can get an attribute that says whether to print them at once (but un-aligned), or in the end (and aligned).