3 added 340 characters in body edited Feb 19 '14 at 20:41 user39685 One approach is to write test cases. The fundamental limitation of this approach is that you're verifying the behavior in a finite number of cases (good luck exhaustively testing a function with 8 parameters!), and so passing tests can't guarantee anything but that the tests pass. Another approach is to use mathematical reasoning, i.e. a proof, based on the actual definition (instead of on the behavior in a limited number of cases). The idea here is that a mathematical proof may be more effective; however, this depends on how amenable your program is to mathematical proof. One approach is to write test cases. Another approach is to use mathematical reasoning, i.e. a proof. The idea here is that a mathematical proof may be more effective; however, this depends on how amenable your program is to mathematical proof. One approach is to write test cases. The fundamental limitation of this approach is that you're verifying the behavior in a finite number of cases (good luck exhaustively testing a function with 8 parameters!), and so passing tests can't guarantee anything but that the tests pass. Another approach is to use mathematical reasoning, i.e. a proof, based on the actual definition (instead of on the behavior in a limited number of cases). The idea here is that a mathematical proof may be more effective; however, this depends on how amenable your program is to mathematical proof. 2 added 1 characters in body edited Feb 19 '14 at 20:26 user39685 I don't exactly understand what the otherlinked answer means by "achieve modularity through mathematical laws", but I think I have an idea of what is meant. Check out Functor: The Functor class is defined like this: `````` class Functor f where fmap :: (a -> b) -> f a -> f b `````` It doesn't come with test cases, but rather, with a couple of laws that must be satisfied. All instances of Functor should obey: `````` fmap id = id fmap (p . q) = (fmap p) . (fmap q) `````` Now let's say you implement `Functor` (source): ``````instance Functor Maybe where fmap _ Nothing = Nothing fmap f (Just a) = Just (f a) `````` The problem is to verify that your implementation satisfies the laws. How do you go about doing that? One approach is to write test cases. Another approach is to use mathematical reasoning, i.e. a proof. The idea here is that a mathematical proof may be more effective; however, this depends on how amenable your program is to mathematical proof. I can't guide you through an actual formal proof that the above `Functor` instance satisfies the laws, but I'll try and give an outline of what the proof might look like: `fmap id = id` if we have `Nothing` `fmap id Nothing` = `Nothing` by part 1 of the implementation `id Nothing` = `Nothing` by the definition of `id` if we have `Just x` `fmap id (Just x)` = `Just (id x)` = `Just x` by part 2 of the implementation, then by the definition of `id` `fmap (p . q) = (fmap p) . (fmap q)` if we have `Nothing` `fmap (p . q) Nothing` = `Nothing` by part 1 `(fmap p) . (fmap q) \$ Nothing` = `(fmap p) \$ Nothing` = `Nothing` by two applications of part 1 if we have `Just x` `fmap (p . q) (Just x)` = `Just ((p . q) x)` = `Just (p (q x))` by part 2, then by the definition of `.` `(fmap p) . (fmap q) \$ (Just x)` = `(fmap p) \$ (Just (q x))` = `Just (p (q x))` by two applications of part two I don't exactly understand what the other answer means by "achieve modularity through mathematical laws", but I think I have an idea of what is meant. Check out Functor: The Functor class is defined like this: `````` class Functor f where fmap :: (a -> b) -> f a -> f b `````` It doesn't come with test cases, but rather, with a couple of laws that must be satisfied. All instances of Functor should obey: `````` fmap id = id fmap (p . q) = (fmap p) . (fmap q) `````` Now let's say you implement `Functor` (source): ``````instance Functor Maybe where fmap _ Nothing = Nothing fmap f (Just a) = Just (f a) `````` The problem is to verify that your implementation satisfies the laws. How do you go about doing that? One approach is to write test cases. Another approach is to use mathematical reasoning, i.e. a proof. The idea here is that a mathematical proof may be more effective; however, this depends on how amenable your program is to mathematical proof. I can't guide you through an actual formal proof that the above `Functor` instance satisfies the laws, but I'll try and give an outline of what the proof might look like: `fmap id = id` if we have `Nothing` `fmap id Nothing` = `Nothing` by part 1 of the implementation `id Nothing` = `Nothing` by the definition of `id` if we have `Just x` `fmap id (Just x)` = `Just (id x)` = `Just x` by part 2 of the implementation, then by the definition of `id` `fmap (p . q) = (fmap p) . (fmap q)` if we have `Nothing` `fmap (p . q) Nothing` = `Nothing` by part 1 `(fmap p) . (fmap q) \$ Nothing` = `(fmap p) \$ Nothing` = `Nothing` by two applications of part 1 if we have `Just x` `fmap (p . q) (Just x)` = `Just ((p . q) x)` = `Just (p (q x))` by part 2, then by the definition of `.` `(fmap p) . (fmap q) \$ (Just x)` = `(fmap p) \$ (Just (q x))` = `Just (p (q x))` by two applications of part two I don't exactly understand what the linked answer means by "achieve modularity through mathematical laws", but I think I have an idea of what is meant. Check out Functor: The Functor class is defined like this: `````` class Functor f where fmap :: (a -> b) -> f a -> f b `````` It doesn't come with test cases, but rather, with a couple of laws that must be satisfied. All instances of Functor should obey: `````` fmap id = id fmap (p . q) = (fmap p) . (fmap q) `````` Now let's say you implement `Functor` (source): ``````instance Functor Maybe where fmap _ Nothing = Nothing fmap f (Just a) = Just (f a) `````` The problem is to verify that your implementation satisfies the laws. How do you go about doing that? One approach is to write test cases. Another approach is to use mathematical reasoning, i.e. a proof. The idea here is that a mathematical proof may be more effective; however, this depends on how amenable your program is to mathematical proof. I can't guide you through an actual formal proof that the above `Functor` instance satisfies the laws, but I'll try and give an outline of what the proof might look like: `fmap id = id` if we have `Nothing` `fmap id Nothing` = `Nothing` by part 1 of the implementation `id Nothing` = `Nothing` by the definition of `id` if we have `Just x` `fmap id (Just x)` = `Just (id x)` = `Just x` by part 2 of the implementation, then by the definition of `id` `fmap (p . q) = (fmap p) . (fmap q)` if we have `Nothing` `fmap (p . q) Nothing` = `Nothing` by part 1 `(fmap p) . (fmap q) \$ Nothing` = `(fmap p) \$ Nothing` = `Nothing` by two applications of part 1 if we have `Just x` `fmap (p . q) (Just x)` = `Just ((p . q) x)` = `Just (p (q x))` by part 2, then by the definition of `.` `(fmap p) . (fmap q) \$ (Just x)` = `(fmap p) \$ (Just (q x))` = `Just (p (q x))` by two applications of part two 1 answered Feb 19 '14 at 20:20 user39685 I don't exactly understand what the other answer means by "achieve modularity through mathematical laws", but I think I have an idea of what is meant. Check out Functor: The Functor class is defined like this: `````` class Functor f where fmap :: (a -> b) -> f a -> f b `````` It doesn't come with test cases, but rather, with a couple of laws that must be satisfied. All instances of Functor should obey: `````` fmap id = id fmap (p . q) = (fmap p) . (fmap q) `````` Now let's say you implement `Functor` (source): ``````instance Functor Maybe where fmap _ Nothing = Nothing fmap f (Just a) = Just (f a) `````` The problem is to verify that your implementation satisfies the laws. How do you go about doing that? One approach is to write test cases. Another approach is to use mathematical reasoning, i.e. a proof. The idea here is that a mathematical proof may be more effective; however, this depends on how amenable your program is to mathematical proof. I can't guide you through an actual formal proof that the above `Functor` instance satisfies the laws, but I'll try and give an outline of what the proof might look like: `fmap id = id` if we have `Nothing` `fmap id Nothing` = `Nothing` by part 1 of the implementation `id Nothing` = `Nothing` by the definition of `id` if we have `Just x` `fmap id (Just x)` = `Just (id x)` = `Just x` by part 2 of the implementation, then by the definition of `id` `fmap (p . q) = (fmap p) . (fmap q)` if we have `Nothing` `fmap (p . q) Nothing` = `Nothing` by part 1 `(fmap p) . (fmap q) \$ Nothing` = `(fmap p) \$ Nothing` = `Nothing` by two applications of part 1 if we have `Just x` `fmap (p . q) (Just x)` = `Just ((p . q) x)` = `Just (p (q x))` by part 2, then by the definition of `.` `(fmap p) . (fmap q) \$ (Just x)` = `(fmap p) \$ (Just (q x))` = `Just (p (q x))` by two applications of part two