[Haskell-cafe] Free theorems for dependent types?

[Eugene Kirpichov]

Or in a language without bottoms.

2009/5/20 David Menendez <dave at zednenem.com>:
> 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)
> B
>
> --
> Dave Menendez <dave at zednenem.com>
> <http://www.eyrie.org/~zednenem/>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>



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