I apologize if the formatting or content of my previous email caused offence.
Hopefully my question is better phrased and presented this time.
Below is my attempt to code the first example from Walder’s Theorems for free! paper[1].
{-# 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'])
I am not sure about what is being proved.
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
[1] homepages.inf.ed.ac.uk/wadler/papers/free/free.ps
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
