2 Dec
2013
2 Dec
'13
4:58 p.m.
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