You Need Subtyping
blog.polybdenum.com
blog.polybdenum.com
That's... not true? The language can just have an implicit conversion rule for convenience.
> properties like nullability that don’t affect memory layout
That's not true either? It might not affect memory layout because all your objects are boxed or you have niche value optimisation you can use to tag nulls, but make an unboxed integer nullable and you'll definitely see your memory layout be affected.
the presence of an implicit conversion rule `T -> T?` amounts to the observation that `T <: T?`, where <: is the subtyping relation
> make an unboxed integer nullable ...
I don't think any language allows this, in any case disallowing nullability for unboxed types amounts to the observation that `P !<: P?`, where !<: is "does not subtype"
I believe (unless I have misunderstood you) that both your examples are subsumed (heh) by subtyping
Not necessarily, because you might consider it acceptable for the implicit conversion to change the memory layout in this sense.
> I don't think any languages allow this
Plenty do, e.g. Rust's Option works that way.
> in any case disallowing nullability for unboxed types amounts to the observation that `P !<: P?`, where !<: is "does not subtype"
Saying the same thing with fancier words doesn't explain anything. The point is you can't simply treat non-nullable as a subtype of nullable in general, because this case exists.
But surely, you can still use subtyping in other cases -- when it is already unboxed -- right?
Like so: `T <: T?` for all boxed `T`.
Well, maybe. But you have to actually have to do the legwork of figuring out which cases are subtypes and which aren't - unboxed was the first case that comes to mind, there might be others. Restating the same thing using symbols doesn't help make anything clearer, it just gets in the way.
Does the actual data layout impact the observation?
If you have A, something that accepts B, and you consider it implicitly possible for an A to be a B with either no change or an implicit change... that seems to amount to considering As to be Bs when necessary.
The fact that an A can be implicitly converted to a B in this context does not mean that an A should always be implicitly converted to B. (In this case B is effectively a pointer/reference to A; implicitly forming that reference is a useful convenience feature in some contexts, but I don't think treating A as a subtype of reference to A in the general case is a good idea)
I don't know what to make of context here; if you're referring to whether you have a pointer to a type as context, I think it makes more sense to consider that part of the type (i.e. a pointer a A is a subtype of a pointer to B, while A is not a subtype of B)
So you assert that numbers and strings are the same type because PHP and Javascript will implicitly convert back and forth? That any C++ implicit constructor creates a subtyping relationship?
> I don't think any language allows this
Rust, Swift, Zig, just off the top of my head. C# too, value types is where and why it first introduced explicit nullability (back in C# 2.0).
If you can provide (valid!) methods `T -> U` and `U -> T` for two types, why wouldn't `T = U` hold? (Atleast for types where `=` makes sense)
This is the definition I am using:
> S is a subtype of T, written S <: T, if a value of type S can safely be used in any context where a value of type T is expected.
from Pierce's "Software Foundations"
Of course, you may not want to make `String <: Number` and `Number <: String` (and thus `String = Number`), because there is no sensible way to do so; but this is an issue with the way PHP/JS handles subtyping, not with the notion of subtyping itself and certainly does not apply to the example of nullable types.
Unfortunately, I am not familiar enough with C++ to comment on the other question, sorry!
That's the semantics of those languages.
For example since Vec can Deref to Slice, you can syntactically run Slice methods on a Vec; meaning Vec is a subtype of Slice.
[0] https://doc.rust-lang.org/std/ops/trait.Deref.html#deref-coe...
In Swift it does not. But in Kotlin, `String?` is not an enum (sum type), but instead means `String | null`, a union type.
Post-submit clarity edit: Ah, I think I understand. You're objecting to OP's definition of subtyping, as it breaks down for certain language implementations.
By "it is ok pass a String where we expect a String?", I think he means that no such program can go wrong, therefore this is sound. Whether you do this via an implicit conversion or a subtyping relation doesn't really matter.
> What if your implicit coercions aren't transitive
Have an example in mind?
An example of intransitive implicit coercions: perhaps you have designed a language such that there is an implicit coercion from Booleans to integers (perhaps producing either 0 or 1), and also an implicit coercion from nullable references to Booleans. Arguably you have already sinned, but the situation becomes far worse if you apply transitive closure to the implicit coercions, because now a nullable reference to the integer 53 can be implicitly coerced to an integer—but the integer is 1, not 53!
Why not both?
> An example of intransitive implicit coercions...
Ok? Arbitrary nullable references are obviously not a subtype of booleans no matter what you do. If anything may break by substituting one type for another, those types do not have that subtype relationship, by definition.
It is true regardless. What you are talking about is a language implementation detail that is orthogonal to reasoning about the type system. Depending on your definition (reasonable people disagree and could be contextual), the memory layout is also rarely a concern when modeling type theory.
However, I can't make sense of the idea that "most languages don't have subtypes". Every language I can think of above ASM has at least some. In C, int8_t is a subtype of int16_t, for example.
And the idea that this is new territory... Here they contrast subtypes in C++ to that of "the new language Java".
https://www.cs.princeton.edu/courses/archive/fall98/cs441/ma...
I agree with the comment that OP really should make it explicit what they mean. It presents itself as "what is subtypes" but they unfortunately use the same term for different concepts in the same text, which I guess contributes to the wider confusion in this thread. Inserting a few "Algebraic ..." and making the context explicit in a place or two.
Or put differently: Algebraic subtypes are a subtype of subtypes.
You can handwave away these implementation details in a high-level language, but a thoughtfully-designed low-level language needs to consider whether or not any given language feature can feasibly be implemented without imposing an undesirable runtime cost.
This is also a pretty poor example for us to index on, because the idea of a function taking a `String?` (or `Option<String>` or whatever) is already so bizarre that's it naturally derails the discussion for want of a better example. It only makes sense to write such a function explicitly for users who do already have the nullable/optional type; if you have the non-nullable/non-optional version of the type, you should just be calling functions defined on that type.
I was under the impression that even today, most code is written in an object-oriented style (or at least, written in languages that support OOP). Therefore, most languages support subtyping via inheritance. Is that not true?
Whoa there - those are very different claims! Most modern languages are multi-paradigm. You can write Python in an OO way, or a data oriented way, or a functional way, or whatever you like. The same is true of JavaScript/typescript. And modern Java. And lots of languages.
Just because the language has the class keyword doesn’t mean everything can be subtyped. If you have an entity-component system, you can’t necessarily inherit from your Entity type. Likewise I can’t inherit from a react component, just because JavaScript has classes. (At least not using modern react)
Modern Java is still very definitely OOP and not multi-paradigm. Other JVM languages, like Scala or Kotlin, add more multi-paradigm features to that ecosystem, but modern Java doesn't.
And you can’t subtype those.
Other JVM languages, like scala, are more OO than Java.
I was pretty surprised and impressed to see a modern example lately. There’s Record data types, stronger type inference with `var`, pretty great structural pattern matching, switch expressions (that return a value), stream apis for map, filter, and reduce etc. All of these move it further away from strictly OOP.
And separate but still cool is a pretty neat virtual thread system too. Java has definitely had a bit of a glow up since I learned it in uni.
I suspect that the stronger claim is true - but even the weaker claim would invalidate the article's statements that "existing programming languages have little or no subtyping" and that OOP was a "fad" and has been left in the past.
> , “subtyping” might call to mind classes and inheritance hierarchies. However, subtyping is a far more basic and general notion than that.
Yes, there are other forms of subtyping, but saying that many languages don't have subtyping just because they don't have these other forms of subtyping is either cluelessness or satire.
Every "type" you use in Ada is actually a subtype.
In Ada, "A subtype of a given type is a combination of the type, a constraint on values of the type, and certain attributes specific to the subtype".
You don't ever refer to actual types in Ada, since creating a type with "type" actually creates an anonymous type and the name refers to the first subtype.[1]
type Token_Kind is (
Identifier,
String_Literal,
-- many more ...
-- These are character symbols and will be part of Token_Character_Symbol.
Ampersand,
-- ...
Vertical_Bar,
);
-- A subtype with a compile-time checked predicate.
subtype Subprogram_Kind is Token_Kind
with Static_Predicate => Subprogram_Kind in RW_Function | RW_Procedure;
subtype Token_Character_Symbol is Token_Kind range Ampersand .. Vertical_Bar;
This is exactly how "accessibility" of access types works in Ada[2]. If you have a pointer ("access type") to something on the heap, you can use it wherever an anonymous access type can be used. You can also create subtypes of access types which have the constraint of a "null exclusion".
In this case it doesn't seem very relevant, it looks like the article just assumes boxed records are dynamically or structurally typed, even though that's completely unrelated.
In C++ it's approximately std::unique_ptr<T> in a lot of the high level languages (indeed Java I mentioned above fits this if you're not familiar with the details) boxing is silently done for you and you are unaware of it unless you care about fine details.
Think of an arbitrary type Goose, where "is" the Goose? Assume for a moment there's data associated so the Goose does need to be stored somewhere, the two usual candidates are "the stack" and "the heap". If you've no idea what those are then I'm afraid you need a bit more CS to really engage with this conversation. Boxing puts things on the heap, typically with just a pointer to that box kept on the stack.
//boxing var a = 5; //int, value type
string b = (string)a; //string, reference type
Unboxing is the reverse process of transforming variables of reference types to value types.
A value type variable holds the value directly, while a reference type variable holds a reference that points to a memory address where the actual value is found.
I think a more generally correct statement would be:
> An unboxed value can be held in CPU registers directly, while a boxed value is referenced through a memory address where the actual value is found.
https://learn.microsoft.com/en-us/dotnet/csharp/programming-...
- parametric polymorphism (generics, templates, ...)
- ad hoc polymorphism (type classes are the nicest example)
- https://en.wikipedia.org/wiki/Row_polymorphism I think this one is the most relevant for the record discussion.
"In high level programmming languages, you expect subtyping as a given",
since we expect a lot of features to work as if subtyping was the way it was implemented?
Checking type unions and inferring information about conditional branching isn't really duck typing
It seems like the former should be a supertype?
Animal -> Dog
(and a Dog will have more fields than an animal)
Said differently, any function that applies to the general {x, y} also applies to the more specific {x, y, z} (it will just not use the z part) but a function that requires a {x, y, z} specifically will not work with all {x, y}s.
My point is, we can’t say TypeScript doesn’t need subtyping just because they botched it. As such, it may not be a good counter example of the article’s thesis.
Perhaps you're just missing some words here, but, just for clarity: it doesn't make any sense to say that covariance is a mistake. Covariance applied in specific places, like Java's mutable covariant arrays which leads to unsoundness, can be a mistake, but covariance itself in fine and essential in languages with subtyping. Function parameters should be covariant, function returns should be contravariant, mutable data structures should be invariant, etc.
I'm not very familiar with these relations, but shouldn't function returns be covariant? `String => Cat` is a subtype of `String => Animal`?
> Function parameters should be covariant
For function parameters, doesn't it depend on how the parameter is used?
You're right :) I mixed up covariance and contravariance for function parameters and return value in my comment.
> For function parameters, doesn't it depend on how the parameter is used?
I don't think so, but maybe there's specific circumstances I don't know of? Function parameter types is a constraint on _input_ to the function. Changing that to a subtype amounts to the function receiving arguments that satisfies a stronger constraint. That seems that something that would hold no matter how the parameter is used?
> I don't think so, but maybe there's specific circumstances I don't know of?
I don't know specific circumstances either, but I presume they exist because of things like Dart's `covariant` keyword [0], which makes function parameters covariant instead of contravariant.
Consider if we have `A <= B <= C`, and a function:
int Copy([out] Array<B> dest, [in] Array<B> src);
Buffer<A> asrc = ...
Buffer<B> bsrc = ...
Buffer<C> csrc = ...
Buffer<A> adest = allocate(...)
Buffer<B> bdest = allocate(...)
Buffer<C> cdest = allocate(...)
Copy(adest, asrc); // No! - How would Copy know how to copy `A` values when it only knows about `B`?
Copy(adest, bsrc); // No! - src argument is OK, but how can it downcast them to `A`?
Copy(adest, csrc); // No! - Same as above, and src elements must be at least `B`s`.
Copy(bdest, asrc); // Ok. - Any `A` in the src are interpreted as `B`s.
Copy(bdest, bsrc); // Ok, - all values are interpreted as `B`s.
Copy(bdest, csrc); // No! - Argument elements must be at least `B`s`.
Copy(cdest, asrc); // Ok - values are interpreted as `B`s in src, and as `C`s in dest.
Copy(cdest, bsrc); // Ok
Copy(cdest, csrc); // No! Argument elements must be at least `B`s`.
Copy(adest, asrc); // pass (wrong)
Copy(adest, bsrc); // pass (wrong)
Copy(adest, csrc); // fail
Copy(bdest, asrc); // pass
Copy(bdest, bsrc); // pass
Copy(bdest, csrc); // fail
Copy(cdest, asrc); // fail (wrong)
Copy(cdest, bsrc); // fail (wrong)
Copy(cdest, csrc); // fail
copy : Array<B> -> Array<B>If we consider inside the function:
foo : arg:String => result:Animal
foo =
;; arg <: String
;; Animal <: result
let result = foo (arg)
;; String <: arg
;; result <: Animal
Always? In that case, do you know why Dart has a `covariant` keyword [0], which makes function parameters covariant?
Another way to put it, if I create a subtype, then the subtype's functions are allowed to be more general in what they accept, and more specific in what they return.
This implies that there is no subtype relation between X[Supertype] and X[Subtype].
To switch up the examples a bit, Natural is a subtype of Integer, so it's perfectly valid to make Natural => Natural (the type of IntegerSqrt) a subtype of Natural => Integer (the type of functions returning integers given a natural-number argument, such as n => (-2)**n), and to make Integer => Natural (the type of IntegerAbs) a subtype of Natural => Natural. If someone is expecting a Natural => Natural function, no surprises will result if you secretly smuggle them IntegerAbs. They just won't happen to call it with a negative argument.
And others have pointed out that covariance and contravariance are both logically unsound for mutable container types like arrays. In particular, covariance would allow you to infer Vector<Natural> is a subtype of Vector<Integer>, which, together with the function subtyping rules above, lets you pass a Vector<Natural> to a function like a => a[0] := -1. That will store a negative number into the Vector<Natural>, and down the line, that -1 will be incorrectly used in Natural calculations, possibly producing incorrect results. Contravariance is no better, because then functions like a => IntegerSqrt(a[0]) fall down go boom.
What I haven't seen anyone mention yet is that covariance is perfectly sound for immutable container types. If you have an immutable List container type supporting Car, Cdr, Cons, and IsEmpty functions, no surprises will result from passing a List<Natural> to a function expecting a List<Integer>. It can add -1 to the List with Cons(-1, xs) but that doesn't mutate the original List; it returns a new, longer List, which is already statically typed as a List<Integer>.
This is far from an original observation, so I was surprised not to see it mentioned.
Nothing obliges you to add function or immutable-container subtyping to your language just because you have subtyping of some kind. You could require implicit or explicit adaptors to be inserted in cases like the above, perhaps eliding those adaptors as a compilation optimization. Logically, that's a perfectly sound thing to do. I don't know why you would want to. It seems inconvenient. But maybe you do.
If you have a type Animal, with subtypes Dog and Cat, then covariance means a list of Cat is a subtype of a list of Animal. The problem is that appending a Dog is a legal action for a list of Animals, but not a legal action for a list of Cats.
https://github.com/python/mypy/issues/4976 is an interesting discussion on this in Python: should a TypedDict be allowed where a dict argument is accepted? The basic consensus is no, because then one could modify the dict, adding keys that wouldn't be allowed in the specific TypedDict.
But this means that often you have to do cast(dict, my_typed_dict) to be able to interop with third party libraries that (quite naturally) believed that by typing their arguments as accepting a dict, they'd be accepting all dict-like things.
Const list<cat> is a subtype of Const list<animal>. But that does get complicated because. The difference between a mutable container of immutable elements and an immutable container of mutable elements is hard to get your head around, and verbose to capture in syntad.