Or in a language without bottoms. 2009/5/20 David Menendez <[email protected]>: > On Sun, May 17, 2009 at 11:52 PM, Ryan Ingram <[email protected]> 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 <[email protected]> > <http://www.eyrie.org/~zednenem/> > _______________________________________________ > Haskell-Cafe mailing list > [email protected] > http://www.haskell.org/mailman/listinfo/haskell-cafe >
-- Eugene Kirpichov Web IR developer, market.yandex.ru _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
