[Haskell-cafe] how to factorize propagation of a function over a data type
paratribulations at free.fr
Tue Dec 3 02:30:11 UTC 2013
Andras Slemmer wrote:
> The reason you need the typeclass constraint is not in the use of 'f' but
> rather in the use of propagate and what you pass in to it (foo1/foo2
> here). If you leave away the typeclass constraint what you're left with
> propagate' Bar -> (forall a. a->a) -> Bar
> The implementation of this function is the same as before, however your
> use of propagate' is restricted:
> forall a. a->a is a very "strict" type, in fact the only inhabitant of
> this type is 'id' (and bottom, but disregard that here), which means the
> only way to call propagate is to pass in 'id'. Try it yourself!
Indeed I have tried, it works as you say.
> 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!
Interesting. I have tried to google on the topic, but I find mainly research
articles. For example:
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.
More information about the Haskell-Cafe