20 May
2009
20 May
'09
5:47 p.m.
On Sun, May 17, 2009 at 11:52 PM, Ryan Ingram
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