[Haskell-cafe] Free theorems for dependent types?

David Menendez dave at zednenem.com
Wed May 20 13:47:30 EDT 2009

On Sun, May 17, 2009 at 11:52 PM, Ryan Ingram <ryani.spam at 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)

Dave Menendez <dave at zednenem.com>

More information about the Haskell-Cafe mailing list