Take a type theory of your choice (perhaps System Fω). Parametric functions are known to be natural transformations in 'Type' category. Yet not every natural transformation in 'Type' is a polymorphic function.
What is the counter-example?
$\begingroup$
$\endgroup$
5
-
1$\begingroup$ What is the $\mathsf{Type}$ category? (Make sure you explain exactly how equality of morphisms is supposed to work, please.) $\endgroup$– Andrej BauerJan 29, 2019 at 7:44
-
$\begingroup$ @AndrejBauer, Thank you for pointing out that choice of equality is relevant, I have not appreciated it. This remark alone is helpful as I see that this is essential in the definition of the natural transformation. I know the standard options are $\beta$ and $\beta\eta$ equalities. Are there others? Can/should we stipulate that isomorphic types are equal even if we can't prove it internally? I can't phantom what would be the effect. If I must choose one I'd like to focus on $\beta\eta$ equality. $\endgroup$– Łukasz LewJan 29, 2019 at 15:28
-
$\begingroup$ This question has 3 votes to be closed, yet no comment explaining why or how it can be improved. The question is important to me and I'm keen to improve it if it is not clear. $\endgroup$– Łukasz LewJan 29, 2019 at 15:31
-
3$\begingroup$ There is a suggestion, namely that you explain what the $\mathrm{Type}$ category is. You have not done so. And please put the explanation in the main text, not the comments. I think you will discover that you do not know what the category is. I would also like to see a reference to the claim that "Parametric functions are known to be natural transformations in $\mathrm{Type}$ category" because it's not clear what that is supposed to mean. $\endgroup$– Andrej BauerJan 29, 2019 at 22:54
-
$\begingroup$ Maybe "Normal Forms and Cut-Free Proofs as Natural Transformations", but it's dinatural, not natural. $\endgroup$– xavierm02Jan 30, 2019 at 14:52
Add a comment
|