[Haskell-cafe] Free theorems for dependent types?
ekirpichov at gmail.com
Wed May 20 13:49:40 EDT 2009
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)
> Dave Menendez <dave at zednenem.com>
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
Web IR developer, market.yandex.ru
More information about the Haskell-Cafe