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

TP 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
> is:
> 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 mailing list