Accounting for parametricity in property testing - Haskell

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

Asad Saeeduddin

Does it make any sense to use trivial (i.e. constant/nonvarying) generators for types that functions/classes under test are parametric with respect to?

Asad Saeeduddin

the type system already guarantees the function can't screw up by examining the values of those types, so you can basically put unit in there and still discover any bugs there are to find, no?

Georgi Lyubenov // googleson78

is there something prompting you to suspect otherwise?

Asad Saeeduddin

Just my inexperience with property based testing :)

Asad Saeeduddin

most of the "xyz-classes" collections of laws I've seen online use something like an integer for types that the class is parametric wrt

Asad Saeeduddin

e.g. if testing the functor laws for (a -> b) -> f a -> f b, they'll use integers for a and b. what I'm wondering is if its' safe for me to be stupider and just use (). will i still uncover whatever bugs there are to be found?

Georgi Lyubenov // googleson78

well.. I would still use something with more than one value

Georgi Lyubenov // googleson78

if you want to check fmap f . fmap g $ xs == fmap (f . g) xs you would need to use some f, and if that f is also Identity it would matter

Georgi Lyubenov // googleson78

because Identity () has only one (not containing bottom) value, so it will always be == to itself

Asad Saeeduddin

the fmap implementation never analyzes the a or b, that's guaranteed by the type system. so why would it matter whether I have a Bool or a ()?

Asad Saeeduddin

right. and there is actually only one way to write the fmap function for Identity just based on the types I think

Asad Saeeduddin
forall a b. (a -> b) -> Identity a -> Identity b

If you erase the newtype, that's:

forall a b. (a -> b) -> a -> b

I don't think it's possible to screw that up and still typecheck

Georgi Lyubenov // googleson78

so you wouldn't be testing it for Identity anyway

Georgi Lyubenov // googleson78

but I think this argument can be transferred to something more complex, e.g. Maybe?

Asad Saeeduddin

hmm. with Maybe can't I just return Nothing for the Just case and screw up?

Asad Saeeduddin

if I have that bad implementation, and I'm only ever using ()s for the type parameter to Maybe, i think I'd still catch it

Asad Saeeduddin

Like I said, I actually don't know whether this generalizes, that's why i'm asking. It just sounds like something that might make sense.

Georgi Lyubenov // googleson78

I'd also wager on "it doesn't matter", I'm just trying to "play devil's advocate"

Asad Saeeduddin

yes, that's exactly what i'm looking for, thanks

Asad Saeeduddin

e.g. does something go wrong if we apply this principle to Traversable? Is Identity the only applicative I need to test with?

Georgi Lyubenov // googleson78
listToMaybe :: [a] -> Maybe a

for this using [()] -> Maybe () will never be able to catch that this implementation is "wrong":

listToMaybe [] = Nothing
listToMaybe [x] = Just x
listToMaybe (_:y:_) = Just y
Georgi Lyubenov // googleson78

whereas [Integer] -> Maybe Integer has a chance of doing so

Asad Saeeduddin

like, what's the law we're testing?

Georgi Lyubenov // googleson78

wrong in the sense that it doesn't do the same thing as Data.Maybe.listToMaybe:

  1. if the list is empty, return Nothing
  2. if it isn't, return the first element
Asad Saeeduddin

so the law requires an Eq constraint on a?

Asad Saeeduddin

hmm ok. I guess that's a good counterexample.

Asad Saeeduddin

i'm having some trouble figuring out how to write the law

Asad Saeeduddin

listToMaybe [] = Nothing is law 0

Georgi Lyubenov // googleson78

that's the problem with the example - the law is the implementation itself, basically

Asad Saeeduddin

listToMaybe (x : xs) = Just x

Asad Saeeduddin

i guess that's the second one?

Asad Saeeduddin

this gives us a counterexample for the fmap thing as well I believe

Asad Saeeduddin

for fmap :: (a -> b) -> [a] -> [b] I mean

Georgi Lyubenov // googleson78
fmap _ [] = []
fmap f [x] = [x]
fmap f [x, y] = [f y, f x]
fmap f xs = map f xs
Asad Saeeduddin

hmm, i'm not sure we can actually write that second case

Asad Saeeduddin

yeah, exactly. so that one would be fine if we were looking at ()s all the time

TheMatten

Isn't it that for such type of testing, we want "counting" generator? We don't really care about the content, we care about it's uniqueness and position in resulting value (you can only move value around and apply arguments to it if it's polymorphic, can't you?). Simply spitting out unique values would uncover "moving around" immediately, while random generator could potentially need more runs in case it "accidentally" generates same values in multiple places.

Asad Saeeduddin

very interesting. ok, so now that you've invalidated that hypothesis, how about the "dual" hypothesis: does using a generator that never produces the same thing twice for those type parameters work?

Asad Saeeduddin

@TheMatten you beat me to it!

Georgi Lyubenov // googleson78

(using Const () for testing Traversables should also exhibit the same flaw, I think)

Georgi Lyubenov // googleson78

then you can't test the property of "being a function"

Georgi Lyubenov // googleson78

because you'll never encounter the same x twice

Georgi Lyubenov // googleson78

granted, that is a very weird thing to test

TheMatten

unsafePerformIO stuff may need more than property testing :sweat_smile:

Georgi Lyubenov // googleson78

not only for actual functions:

if you've implemented Map k v as [(k, v)] under the hood, you may want a property that for all Maps, for each k there is at most one v

Sandy Maguire

this thread is too long for me to work through, so at the risk of repeating something already said

Sandy Maguire

no, you still want randomness!

Sandy Maguire

maybe i am implementing a set and property testing it

Sandy Maguire

probably i want a law that says insert a (insert b s) == insert b (insert a s)

Sandy Maguire

everything here is polymorphic! but if i have (badly) implemented insert in such a way that it only works once. in this case, a constant generator will say "yup, everything is fine!"

Sandy Maguire

there is a trivial model where you map everything to (); using a constant generator can't differentiate your model from that one

Asad Saeeduddin

@Sandy Maguire What about the non random generator that always generates distinct values discussed above (e.g. natural numbers 0..infinity)?

Asad Saeeduddin

would that fail to detect an unlawful implementation in your set example?

Sandy Maguire

then you don't get automatic testing of crazy values

Sandy Maguire

maybe my code only works up to 100 or something?

Asad Saeeduddin

Your code doesn't have the opportunity to only work up to 100

Asad Saeeduddin

because it is parametric

Sandy Maguire

well, i guess true if you don't have any constraints

Sandy Maguire

but constraints can do arbitrarily crazy things :)

Asad Saeeduddin

If it isn't parametric in the relevant type then it's not relevant to what we're talking about

Sandy Maguire

if you're talking fully forall a. a -> ... then yeah, sure, it's fine

Sandy Maguire

except if your code doesn't work now if you get two of the same value?

Asad Saeeduddin

I don't quite understand that last bit

Sandy Maguire

trying hard to construct an example

Sandy Maguire

maybe it can't be done without an Eq

Asad Saeeduddin

except if your code doesn't work now if you get two of the same value?

I'm talking about this bit. I don't quite understand what this means.

Sandy Maguire

okay well let's assume i have an eq on a

Sandy Maguire

i have a bad impl:

f a b | a == b = error "uh oh"
      | otherwise = pure 5
Sandy Maguire

maybe this can't exist without an eq constraint, so maybe you're fine

Sandy Maguire

let's assume you're right that parametricity solves this problem for us! even then, you're also going to want to test code that is concrete, where a deterministic generator can always be detected, and then hide functionality or w/e

James King

Seems like this is the weakness of not having dependent or refinement types to serve as proofs. Property tests generate values so that we can assert invariants on the domain and codomain of our functions which types alone are not able to express, no?

James King

They're not proofs but they give us some amount of certainty that for a sampling of the domain our invariant holds.

James King

I think polymorphism alone is not sufficient to describe such properties otherwise we would be able to prove a functor is valid in Haskell alone, wouldn't we?