On Sun, May 17, 2009 at 11:52 PM, Ryan Ingram <ryani.s...@gmail.com> wrote: > Free theorem's are theorems about functions that rely only on parametricity. > > For example, consider any function f with the type > forall a. a -> a > > >From its type, I can tell you directly that this theorem holds: > forall g :: A -> B, x :: A, > f (g x) = g (f x) > > (Note that the f on the left is B -> B, the f on the right is A -> A).
Note also that the theorem only holds in a strict language (i.e., not Haskell). data A = A deriving Show data B = B deriving Show f :: a -> a f = const undefined g :: A -> B g = const B *Main> f (g A) *** Exception: Prelude.undefined *Main> g (f A) B -- Dave Menendez <d...@zednenem.com> <http://www.eyrie.org/~zednenem/> _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
