Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Problem with using Zero as discard in computation expression #28

Closed
jacobstanley opened this issue Oct 14, 2016 · 14 comments
Closed

Problem with using Zero as discard in computation expression #28

jacobstanley opened this issue Oct 14, 2016 · 14 comments

Comments

@jacobstanley
Copy link
Member

jacobstanley commented Oct 14, 2016

If we write something like this:

forAll {
  printfn "%d" 123
  let! x = Gen.range 0 10
  return! x <= 11
}

It will discard every expression, as the printfn line will turn in to Zero.
edit: turns out this is not the case at all

It seems like the solution is to turn it in to the "other" type of computation expression which uses for instead of let!. I prefer the let one personally, but I don't think it matters too much. The for style of computation expression is a lot more flexible, allowing for custom operations like where which we can use instead of the Zero hack.

I'm going to start work on this now and see how I go.

The plan (if I can make it work) is to allow something like this:

forAll {
  printfn "%d" 123
  for x in Gen.int do
  for y in Gen.int do
  where x > 0 && y > 0
  yield x * y > 0
  yield someOtherThing // maybe we can even use yield for multiple asserts?
  assert x * y > 0 // or perhaps a custom operation which is yield in disguise
}
@moodmosaic
Copy link
Member

I think we shouldn't use yield for multiple asserts because, often, multiple asserts tend to lead to this issue.

@jacobstanley
Copy link
Member Author

What I really want is to be able to write where but using the let! style, unfortunately this isn't allowed, you have to choose between for or let!.

I agree that it's a bad style to use multiple asserts interspersed with more actions and generators, but two in a row is no differently logically to one with a && operator.

@moodmosaic
Copy link
Member

but two in a row is no differently logically to one with a &&operator.

True.

@moodmosaic
Copy link
Member

Allowing for custom operations can even end up to having some property-based testing DSL, so this looks appealing, although technically this might not be trivial, as it seems.

@jacobstanley
Copy link
Member Author

Allowing for custom operations can even end up to having some property-based testing DSL

Yeah! I think we could do some cool stuff with this, the classification functions you mentioned here #25 and the counterexample function would work nicely in such a DSL.

@moodmosaic
Copy link
Member

Indeed!

@jacobstanley
Copy link
Member Author

It looks like multiple yields don't work anyway unless you implement Combine, so we're good

@jacobstanley
Copy link
Member Author

Also I managed to get let! syntax working with where, I needed to implement For/Yield but you don't really end up using them explicitly, would like to check out the generated code as the compiler complains every time I try to get rid of them.

So these seem to work:

Property.check <| forAll {
    let! n = Gen.int
    where (n <> 0)
    return 1 / n = 2 / n
}

Property.check <| forAll {
    let! x = Gen.int
    let! y = Gen.int
    where (x > 0 && y > 0)
    return x * y > 0
}

@jacobstanley
Copy link
Member Author

jacobstanley commented Oct 14, 2016

using where has a nasty side-effect, I can observe the compiler transform that tuples up x and y so it can be threaded through the expression:

*** Failed! Falsifiable (after 33 tests and 8 shrinks and 120 discards):
(37963, 56568)

As opposed to using if via the current Zero/discard implementation:

*** Failed! Falsifiable (after 33 tests and 8 shrinks and 120 discards):
37963
56568

This could be problematic with a large number of arguments, needs more investigation to see if we can un-tuple the counterexamples.

It turned out I was wrong by the way:

It will discard every expression, as the printfn line will turn in to Zero.

^ this is not true, it works just fine. So maybe we should stick with what's in master given the tupling issue. Hmm..

@moodmosaic
Copy link
Member

Nice analysis! Since Zero works fine, we could probably close this. Though, I think, we will end up needing some custom operations for #25, and perhaps then we'd have to deal with that tupling issue...

@jacobstanley
Copy link
Member Author

Ok I think I made some progress, I can avoid capturing the tuple by only storing the values when something is bound using Bind (aka let!), and not when it is bound using For (aka for) (which happens under the hood when using custom operations, and also causes the tupling).

I actually tried this approach initially as it makes the most sense, show counterexample for the visible binding, but not for the magic that happens under the hood. But unfortunately I got no output at all when I added the where.

I discovered that this is because of the encoding of Property and Result I was using (forgive me it differs slightly from master, I changed Success to carry a value so it can implement monad):

type Result<'a> =
    | Failure of List<string>
    | Discard
    | Success of 'a

type Property<'a> =
    | Property of Gen<Result<'a>>

I guess at some point we were getting a Success that wiped out the failure (and hence the messages), so I changed it to this:

type Report =
    | Report of List<string>

type Result<'a> =
    | Failure
    | Discard
    | Success of 'a

type Property<'a> =
    | Property of Gen<Report * Result<'a>>

And was sure to append reports together when binding a property, this seemed to fix the issue.

I now get this output:

*** Failed! Falsifiable (after 33 tests and 8 shrinks and 120 discards):
37963
56568

from this:

Property.check <| forAll {
    let! x = Gen.int
    let! y = Gen.int
    where (x > 0 && y > 0)
    return x * y > 0
}

and also from this:

Property.check <| forAll {
    let! x = Gen.int
    let! y = Gen.int
    if x > 0 && y > 0 then
        return x * y > 0
}

So I guess we can choose, or have both, the most important thing is that we can make the DSL stuff work 😄

@moodmosaic
Copy link
Member

I changed Success to carry a value

This seems useful 👍

@moodmosaic
Copy link
Member

where is neat 🎉 – although it makes Gen a bit heavier since it has to carry a tuple 😕 On the other hand, this work makes the DSL stuff possible, and that's awesome.

@jacobstanley
Copy link
Member Author

Resolved by #29

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants