> is not it true that some functors are contravariant?
sure; it's just that if one wants a system where subtypes are subsets, and functions are extensional ( (f, g: A -> B, and for all x from A, f(x) = g(x)) implies f = g), then this one cannot be contravariant (assuming that I have not made a mistake when "proving" that).
> I do not see the importance of substitutability
I think it is quite essential in justifying rules for various mainstream systems of types lambda calculus (e.g. parametric polymorphism of ML and similar systems); although it really becomes explicit, when one enriches a system like that with subtypes.
So here is a logical fork, which depends on whether one likes this class of type systems. If one likes these type systems, then it probably matters that this class of type systems comes from people who think that substitutability is quite key here (although it still does not mean that one has to agree with them, but their arguments should be considered).
Alternatively, one could decide that one does not like this class of type systems, and that inference rules should be different (like I was thinking in the 90-s; now I don't have a firm opinion). Then it's quite likely that substitutability would not be involved.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
timeasmymeasure
no subject
Date: 2011-01-25 01:33 am (UTC)sure; it's just that if one wants a system where subtypes are subsets, and functions are extensional ( (f, g: A -> B, and for all x from A, f(x) = g(x)) implies f = g), then this one cannot be contravariant (assuming that I have not made a mistake when "proving" that).
> I do not see the importance of substitutability
I think it is quite essential in justifying rules for various mainstream systems of types lambda calculus (e.g. parametric polymorphism of ML and similar systems); although it really becomes explicit, when one enriches a system like that with subtypes.
So here is a logical fork, which depends on whether one likes this class of type systems. If one likes these type systems, then it probably matters that this class of type systems comes from people who think that substitutability is quite key here (although it still does not mean that one has to agree with them, but their arguments should be considered).
Alternatively, one could decide that one does not like this class of type systems, and that inference rules should be different (like I was thinking in the 90-s; now I don't have a firm opinion). Then it's quite likely that substitutability would not be involved.