Re: [Haskell-cafe] Free theorems for dependent types?

Or in a language without bottoms. 2009/5/20 David Menendez :

On Sun, May 17, 2009 at 11:52 PM, Ryan Ingram 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 http://www.eyrie.org/~zednenem/ _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- Eugene Kirpichov Web IR developer, market.yandex.ru