3 added 340 characters in body
source | link

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
source | link

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:

  1. 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
  2. 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:

  1. 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
  2. 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:

  1. 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
  2. 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
source | link

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:

  1. 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
  2. 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