TheSeamau5 / elm-check

Property Based Testing in Elm
70 stars 20 forks source link

About the name "Arbitrary" #2

Closed evancz closed 9 years ago

evancz commented 9 years ago

I initially had a pretty hard time figuring out what was going on with QuickCheck in Haskell. I think that was partly because Arbitrary and Shrink were very weird for me. Now that you have emailed about getting shrinking working, it makes more sense: you want to get a minimal bad example. That's cool.

I think the name Arbitrary really detracts from that. I don't want an Arbitrary Int. I feel like having Random.Generator and Test.Generator helps guide me towards what's happening here for real. Normally I just generate a random thing. For a test generator, I want to generate a random thing and be able to shrink it down to a minimal example. So what do you think of calling it a Test.Generator Int?

TheSeamau5 commented 9 years ago

This was my initial thought so I'd like to share my train of thought and get your feedback.

So, just as a reminder for this thread:

type alias Arbitrary a = 
  { generator : Random.Generator a 
  , shrinker : Shrinker a
  }

where

type alias Shrinker a = a -> List a

First of all, I thought, "if I call it Check.Generator or Test.Generator, it might tend to confusion where people think it's Random.Generator. It is... sorta... But you can't pass a Random.Generator to the new elm-check functions".

Secondly, Arbitrary objects do not compose in the same ways as Random.Generator objects. You can insert your favorite category theory terms here but Random.Generator supports the following operations:

map : (a -> b) -> Random.Generator a -> Random.Generator b
flatMap : (a -> Random.Generator b) -> Random.Generator a
andMap : Generator (a -> b) -> Generator a -> Generator b
... -- and so on, see my elm-random-extra for more of these

Arbitrary on the other hand doesn't have these sorts of combinators. Instead it has stuff like

convert : (a -> b) -> (b -> a) -> Arbitrary a -> Arbitrary b

and so these things don't combine as well because shrinkers (functions from a to List a), don't support those nice operations.

Now, maybe I'm worrying about something that shouldn't be a worry.

So, instead, here's an example of how you would make your own Arbitrary (or whatever you wanna call it) in elm-check:

type alias Vector =
  { x : Float
  , y : Float
  , z : Float
  }

vector : Arbitrary Vector
vector =
  let
      shrinker {x,y,z} =
        Vector
          `List.map`    shrink float x
          `List.andMap` shrink float y
          `List.andMap` shrink float z

      generator =
        Vector
          `Random.map`    random float
          `Random.andMap` random float
          `Random.andMap` random float
  in
      arbitrary generator shrinker

So, a question that comes up to me is what best terminology to use given that I expect the user's code to look something like this.

(oh, and for the record, I don't like the word Arbitrary. It says nothing I totally agree with you.)

evancz commented 9 years ago

That convert type is pretty odd! Looking at the last example, is it true that Shrinker is an applicative functor, but not a monad? If it is an applicative functor, is it true that Arbitrary is an applicative functor?

To make these questions more concrete, can you do something like this:

vector : Arbitrary Vector
vector =
    Vector
        `Arbitrary.map`    float
        `Arbitrary.andMap` float
        `Arbitrary.andMap` float

float : Arbitrary Float

edit: I think I see the weird part. The shrinker code is using List.map not Shrink.map. Is it good to expose the underlying type of Shrinker instead of hiding it?

evancz commented 9 years ago

Anyway, the point is about Arbitrary being a dumb name. How about some of these that go for the idea of exploring some infinite space:

I think my favorite is seeker for some reason, but I can see a bunch of them working. Maybe this is a good direction to go?

evancz commented 9 years ago

Actually, maybe Explorer is my favorite. I like the idea of Indiana Jones scouring all the infinite possibilities to find a hidden treasure and bring it home in perfect condition.

Explorer also has a heroic/accessible sound to it. Contrast this with Auditor and Reviewer which sound boring, and Investigator Inquisitor Inquirer which are kind of scary words that are hard to spell.

Scout kind of has the same feeling of exploration, but I feel like the analogy is a bit too thin to be most helpful.

evancz commented 9 years ago

To go a bit further with the explorer thing, maybe there could be functions like this:

disprove : Explorer a -> (a -> Bool) -> Challenge
prove : Explorer a -> (a -> Bool) -> Challenge

challenge =
    disprove int (\n -> length [1..n] == n)

int : Explorer Int

Now testing is a matter of trying to complete a bunch of challenges in a certain number of tries.

And if you want to take the explorer analogy further, a Challenge could be called a Quest. Or maybe prove/disprove could be example/counterexample or findExample/findCounterexample.

TheSeamau5 commented 9 years ago

Hmmm... I like the terms disprove and prove. I like the notion of being in the business of finding a counter-example. I think that's more telling of what the library is about.

So, there's this property-based testing library in JS by Douglas Crockford called JSCheck. You can see the docs here: http://www.jscheck.org/

The terminology used there is "Claim". Like you make a claim and then you try to disprove it. That would be the analog to your "Challenge" or the current "Property".

He also has these generator constructors which he calls "Classifiers". So, it's like saying, you "classify" this as an integer, or you classify this as a string, or whatever.

It doesn't have shrinking, but it's about the only property-based testing framework that diverges in terminology from Haskell's QuickCheck.

So, this could be one option.

As for the options your propose, I like the idea of conveying the notion of searching to the user. Like, there's a search space of values and elm-check is trying to exhaust that search space to find the most minimal value that'll disprove your claim. (I think I really like the "disprove" and "claim" terminology)

TheSeamau5 commented 9 years ago

As for the functor stuff... nope. Shrinkers are neither monoids, nor monads, nor functors, nor none of that unfortunately.

Like, if we take map as an example.

If you're in a covariant setting, you'd have something like this:

map : (a -> b) -> Box a -> Box b

If you're in a contravariant setting, you'd get something like:

redirect : (b -> a) -> Box a -> Box b

This is like, you have to go both ways in order to achieve the transition. Cuz a shrinker is a function from a to List a.

Say you try to implement map.

map : (a -> b) -> (a -> List a) -> (b -> List b)
map f shrinkerOnA b = 

It's like, I have a "b" and I want a "List of b's" but I know how to go from "a" to "List of a". So, you're like, ok it's contravariant

map : (b -> a) -> (a -> List a) -> (b -> List b)
map f shrinkerOnA b = 
   shrinkerOnA (f b) -- LIst a

Now you're stuck with a list of a's and you wanna go from a's to b's. So, that's why the type of "convert" is weird. Sorry.

Now, that said, you could "make" it a functor if you just throw away the shrinker.

There's a default noShrink shrinker

noShrink : a -> List b
noShrink _ = []

You could use that... but then you'd lose shrinking.... convert on the other-hand allows you to piggy back off of pre-existing shrinkers. Like the char shrinker is just the int shrinker. The string shrinker is just the list shrinker (same for array).

TheSeamau5 commented 9 years ago

Oh, and about the part of using List.map, I just spelled it out for illustration. elm-shrink re-exports it so you can say Shrink.map

TheSeamau5 commented 9 years ago

So, if I take ideas from the other issue and some of the terminology from JSCheck, I get this basic API:

-- Assuming that b is Equatable
claim : String -> (a -> b) -> (a -> b) -> Specifier a -> Claim
check : Claim -> Int -> Seed -> TestResult  

Which would be used as follows :

reverse_list_claim : Claim
reverse_list_claim = 
  claim "Reversing a list twice yields the original list"
  (List.reverse >> List.reverse)
  identity
  (list int) 

check reverse_list_claim 1000 (Random.initialSeed 203928)

From here I can add all sorts of functions to make it easier to work with like:

quickCheck : Claim -> TestResult

continuousCheck : Claim -> Int -> Task error TestResult
-- or continuousCheck : Claim -> Int -> Address TestResult -> Task error ThreadID

claimTrue : String -> (a -> Bool) -> Specifier a -> Claim
claimFalse : String -> (a -> Bool) -> Specifier a -> Claim

suite : String -> List Claim -> Claim
TheSeamau5 commented 9 years ago

Now, given the ability to have two functions for which the results are expected to be equal, we can get a result with "expected" vs "actual".

Currently, this is how it looks:

my_claim =
  claim2 "Append then reverse is equivalent to reverse then append"
    (\l1 l2 -> List.reverse (l1 ++ l2))
    (\l1 l2 -> List.reverse l1 ++ List.reverse l2)
    (list int) (list int)

Yields :

Unit 
  (Err 
    { actual = "[0,1]"
    , expected = "[1,0]"
    , failingInput = "([1],[0])"
    , name = "Append then reverse is equivalent to reverse then append"
    , numberOfShrinks = 8
    , numberOfTests = 1
    , seed = 
      { next = <function>
      , range = <function>
      , split = <function>
      , state = State 1662217419 1109022573 
      }
    , unshrunk = 
      { actual = "[-33,0,-18,28,17,46,3,-36,19]"
      , expected = "[3,-36,19,-33,0,-18,28,17,46]"
      , failingInput = "([19,-36,3],[46,17,28,-18,0,-33])" 
      } 
    }
  )

Where the first function is considered the "actual" and the second is consider the "expected". I think that this additional info make it easier to diagnose the problem.

evancz commented 9 years ago

This seems really simple and clear, I like it :)

I dislike the name Specifier pretty strongly. What does that mean? I mean, even in normal english, when would you say that? Overall, I don't think it gives a good hint about what is happening. Otherwise, I really like the simplicity of the API and the naming choices!

TheSeamau5 commented 9 years ago

Thanks.

Arghh... naming is truly one of the hardest problems in computer science...

I like Claim and the idea of "checking claims"... as for those things that bundle a generator and a shrinker....

Thing is I can't find a good analogy for those things. I mean, they "define" or "represent" or "encompass" a space or set of values and a means of searching through that space.

TheSeamau5 commented 9 years ago

@evancz how about this:

type alias Investigator a = 
  { generator : Generator a
  , refiner : Refiner a 
  } 

Where shrinking becomes "refining"... cuz you're "refining the search space"...

As an example, this is how the concept would be explained:

An investigator of ints is able to generate ints in order to attempt to disprove a claim by finding a counterexample. If the investigator manages to find such a counterexample, he/she is then able to refine this counterexample into a more minimal or refined version which will be more representatitve of the failure and thus making it easier to debug.

I'm just worried that this is going too nuts with the analogies

evancz commented 9 years ago

I like it! Investigating a claim! :)

I'm not sure about refine vs shrink. Shrink is maybe more literal, but I think they both work well. I'd go with the gut feeling on that one.

TheSeamau5 commented 9 years ago

Ok, cool! So, my gut tells me to go with shrinking cuz if anyone needs to figure out how to write shrinking strategies, worst case they can search for other quick check implementations and they probably have some docs lying around.

Here's how the API's going to look like now with these changes:

claim : String -> (a -> b) -> (a -> b) -> Investigator a -> Claim
check : Claim -> Int -> Seed -> Evidence

suite : String -> List Claim -> Claim
quickCheck : Claim -> Evidence
claimTrue : String -> (a -> Bool) -> Investigator a -> Claim
claimFalse : String -> (a -> Bool) -> Investigator a -> Claim

And the main types:

type alias Investigator a =
  { generator : Generator a
  , shrinker  : Shrinker a
  }

type Claim
  = Claim (Int -> Seed -> Evidence)
  | Suite String (List Claim)

type Evidence
  = Unit UnitEvidence
  | Multiple String (List Evidence)

type alias UnitEvidence =
  Result FailureOptions SuccessOptions

type alias SuccessOptions =
  { name : String
  , seed : Seed
  , numberOfChecks : Int
  }

type alias FailureOptions =
  { name : String
  , counterExample : String
  , actual    : String
  , expected  : String
  , original  :
    { counterExample  : String
    , actual        : String
    , expected      : String
    }
  , seed : Seed
  , numberOfChecks   : Int
  , numberOfShrinks : Int
  }

Unlike with the previous version of elm-check, I'm making the types available to the user because it's then much easier to then just manipulate the results however you need to.

TheSeamau5 commented 9 years ago

Ok, done, I chose Investigator. It works well. Thanks a lot @evancz for your help.