[Haskell-cafe] how to factorize propagation of a function over a data type

Tom Ellis tom-lists-haskell-cafe-2013 at jaguarpaw.co.uk
Mon Dec 2 21:58:49 UTC 2013


On Mon, Dec 02, 2013 at 10:30:11PM -0400, TP wrote:
> Andras Slemmer wrote:
> > Related note: there is a proof that in fact the only inhabitant of (forall
> > a. a -> a) is 'id' and it is the consequence of the "parametricity"
> > property. It is a very neat result I suggest you look it up!
> 
> Are there textbooks where a proof of this fact could be found? I'm an 
> autodidact (who also benefits from help of guys like you), I don't know what 
> lectures on type theory at university level could look like.

I guess the most accessible reference might be Wadler 1989 "Theorems for
Free".

    http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.9875

Tom


More information about the Haskell-Cafe mailing list