Wojciech,
I apreciate that the example only satisifies rather than proves the theorem.
Wadler
says “it is possible to conclude that r satisifies the following theorem”
"r must work on lists of X for any types X".
So does evaluation demonstrate type
level satisfiability?
Thanks,
Pat
Hello Patrick.
I've read the paper just a few days ago and that particular example
was presented to show the general idea in a concrete setting - nothing
more. The general idea here is that if r is a polymorphic function on
lists, then it doesn't matter whether you apply the map function
before or after applying the r itself.
Hope that helps,
Wojciech
2012/2/27 Patrick Browne <patrick.browne@dit.ie>:
> Hi,
> Below is my attempt to code the first example from Walder’s Theorems for
> free! paper.
>
> I am not sure about what is being proved.
>
> Using the notation from the paper does the proof establish a property of
> map, r, composition or the relationship between all three?
>
>
>
> {-# LANGUAGE ExistentialQuantification #-}
>
> import Data.Char
>
> r :: forall a . [a] -> [a]
>
> r = reverse
>
> g :: Char -> Int
>
> g = ord
>
>
>
> (map g . r $ ['a','b','c']) == (r . map g $ ['a','b','c'])
>
>
>
> Regards,
>
> Pat
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>