Have all the Haskell instances of Applicative typeclass that we get with the Haskell platform been proved to satisfy all the Applicative laws? If yes, where do we find those proofs?
The source code of Control.Applicative does not seem to contain any proof that the applicative laws for various instances do hold. It just mentions that
-- | A functor with application.
--
--Instances should satisfy the following laws:
It then just states the laws in the comments.
I found a similar case for the instances of other typeclasses (Alternative and Monad) too.
Are the users of these libraries supposed to verify these laws by themselves?
But I was wondering whether the rigorous proofs of these laws have been given elsewhere by the developers?
Again, I am aware that a rigorous proof of Applicate (or Monad) laws for IO Monad, which involves talking with outside world, in general, may well be very much complex.
Thanks.