juan_gandhi: (Default)
[personal profile] juan_gandhi
It's a known puzzle from the depths of object-oriented teaching: is Circle a subclass or Ellipse. From school we know it is; but as we read in books, for programmers, it is not. How come? Oh, "Liskov principle". They use Liskov principle to scare kids.

Actually we know that a circle is an ellipse with both axes being the same length.

But in programming, an ellipse is something different. It is at least stretchable. And it is also moveable. Somehow it is not rotatable, but we can skip it for simplicity.

An ellipse in programming is (almost) always horizontal; it can be moved (by changing coordinates of its center) and it can be stretched/compressed by changing its height and width. Sure a stretchable ellipse is neither an ellipse nor a circle, not even a stretchable circle. A stretchable circle stretches equally in all directions.

That's it, no? Questions? Objections?

Date: 2011-01-24 10:05 pm (UTC)
From: [identity profile] anhinga-anhinga.livejournal.com
People who advocate type systems with contravariance typically appeal to substitutability -- which is essentially what "proper inheritance" is about.

These people also claim that they are very "categorical", even extending Curry-Howard isomorphism to cartesian closed categories (http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#Curry.E2.80.93Howard.E2.80.93Lambek_correspondence).

This does not mean that they are right, but this is smth to keep in mind... (I tended to dislike contravariance when I was thinking about functional programming in the 1990-s, in particular, because I thought it was a bad idea to mimic object inheritance, and because of other reasons [one is that this results in "non-extensionality" [multiple points representing the same function from A to B in the models], but I did not like categorical models in software either back then. So, basically, if you come up with a viewpoint which would be categorical, but would decouple these things [proper inheritance and contravariance], it would be something different from mainstream [and might be better, but you would have to argue explicitly against the mainstream viewpoint here].)

Date: 2011-01-24 10:56 pm (UTC)
From: [identity profile] ivan-gandhi.livejournal.com
Actually, I do not think I have a ready solution for disambiguating two categories, one with all functions, another with just inheritance.

I do not see the importance of substitutability, but is not it true that some functors are contravariant?

Date: 2011-01-25 01:33 am (UTC)
From: [identity profile] anhinga-anhinga.livejournal.com
> 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.

Date: 2011-01-25 06:58 am (UTC)
From: [identity profile] anhinga-anhinga.livejournal.com
> 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.

After refreshing it in my memory, the canonical way to think about it in the mainstream school of thought is as follows. One considers a universal set D of all untyped lambda-terms (or of their equivalence classes). Types are just some subsets of D. When a lambda-term belongs to the subset X, we say that this term is of type X. Subtypes are subsets. A term f is said to be of type A->B, if whenever term x is of type A, term f(x) is of type B. Here we have contravariance and substitutability, and they are the same thing (easy to see), but we don't have extensionality (because the terms can be equivalent on the inputs from A, but can behave quite differently, when the inputs are outside of A).

Also, the resulting type systems are quite horrible (IMO) in two ways. On one hand, they are strongly normalizable, and lambda-terms without normal form are never typable, so the recursion and Turing-completeness have to be added by ad-hoc methods. On another hand, the inference is usually too strong, so, for example, one can write a pathological sequence of well-typed programs in ML, such that the size of their types is exponential of the size of the program as a directed acyclic graph (and doubly exponential as a linear output) and hence the compiling time is also exponential. And this "compiler bug" is built-in as a design feature right in the heart of ML and languages with the similar type systems (it does not really occur in practice, one has to work to create this pathology, but it's an ugly property of the type system and of the language).

Profile

juan_gandhi: (Default)
Juan-Carlos Gandhi

June 2025

S M T W T F S
1 2345 6 7
8 9 10 11 121314
15161718 1920 21
222324252627 28
29 30     

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 3rd, 2025 08:51 am
Powered by Dreamwidth Studios