3 ms·

> If a function accepts a value that can be String or null, it is ok to pass it a value that is guaranteed to be a String and not null. Or in other words, Strin

> If a function accepts a value that can be String or null, it is ok to pass it a value that is guaranteed to be a String and not null. Or in other words, String is a subtype of String?! 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.

zarakshR 2y ago
> The language can just have an implicit conversion rule for convenience 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
- lmm 2y ago
  > the presence of an implicit conversion rule `T -> T?` amounts to the observation that `T <: T?`, where <: is the subtyping relation 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.
  - zarakshR 2y ago
    > 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`.
    - lmm 2y ago
      > But surely, you can still use subtyping in other cases -- when it is already unboxed -- right? 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.
  - dwattttt 2y ago
    > Not necessarily, because you might consider it acceptable for the implicit conversion to change the memory layout in this sense. 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.
    - lmm 2y ago
      > 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)
      - dwattttt 2y ago
        But isn't it being implicit what makes it a subtype? It doesn't have to be a pointer; integer coercion should also be considered a form of subtyping. 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)
        lmm 2y ago
        My point is that allowing an A to implicitly convert to a pointer to A when calling a function that takes a pointer to A is reasonable, whereas always allowing that implicit conversion anywhere in your program is rather less so. The same applies to integer conversion; there are contexts in which it should maybe happen implicitly, but not everywhere.
- masklinn 2y ago
  > the presence of an implicit conversion rule `T -> T?` amounts to the observation that `T <: T?`, where <: is the subtyping relation 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).
  - zarakshR 2y ago
    > because PHP and Javascript will implicitly convert back and forth 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!
  - marcosdumay 2y ago
    Yes, numbers and strings are the same type in Javascript and PHP. And yes, a C++ constructor declares a subtype relation. That's the semantics of those languages.
  - meltyness 2y ago
    Yeah I think this is "Deref coercion" in Rust.[0] 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-coercion https://doc.rust-lang.org/std/ops/trait.Deref.html#deref-coe...
    - meltyness 2y ago
manmal 2y ago
In Swift, String? is an alias to Optional<String>. Optional is an enumeration with two cases: some, and none, where the former has the non-nil value attached. I‘m not sure how that ties in with subtyping though.
- ackfoobar 2y ago
  > how that ties in with subtyping In Swift it does not. But in Kotlin, `String?` is not an enum (sum type), but instead means `String | null`, a union type.
tlb 2y ago
Implicit conversions from Foo? to Foo are a major footgun, because the point of returning a Foo? is to have the caller check for failure before assuming there's a Foo to use. Even C++ avoids the implicit conversion from optional<T> to T.
- naasking 2y ago
  Yes, but they were describing an implicit conversion going the other way around, eg. String <: String?.
- kragen 2y ago
  Does C++ support implicit coercion from T to optional<T>? I think it doesn't, but that would be the corresponding case.
clord 2y ago
I think that whole section of the post was "For example, in Kotlin," presumably these are true in that language.
wesselbindt 2y ago
Maybe I'm off the mark here, but in my mind the definition of subtype is as follows: t1 is a subtype of t2 if any instance of t1 is an instance of t2. Surely with this definition String is a subtype of String?. Every instance of String (i.e. every string) is an instance of String?, after all. 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.
- seanmcdirmid 2y ago
  String <: String? is true (Any non-null string is a possibly null string), but String? <: String isn’t true (Any possibly null string may not be a non-null string).
  - wesselbindt 2y ago
    We're all in agreement there it seems.
    - seanmcdirmid 2y ago
      If you just state it as a logical quantified proposition, it’s pretty obvious unless the type is complicated (then you need to break it down into multiple logical quantified propositions).
      - wesselbindt 2y ago
        Yes of course, but again, I don't think anyone disagrees with you on this.
naasking 2y ago
> The language can just have an implicit conversion rule for convenience 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.
- kragen 2y ago
  I don't think subtyping and implicit coercions are really equivalent. What if your implicit coercions aren't transitive, or if different chains of possible implicit coercions give different results, or if implicit coercions change the in-memory representation of a value? In the last case, for example, reflectively examining the dynamic type will give different results.
  - 3np 2y ago
    They aren't equivalent, they're in different domains and abstraction levels. Subtypes are an abstract notion in type theory and grammar while coercions are implementation details/syntax. > What if your implicit coercions aren't transitive Have an example in mind?
    - kragen 2y ago
      I think implicit coercions are a semantics issue, not an issue of implementation details. 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!
      - 3np 2y ago
        > I think implicit coercions are a semantics issue, not an issue of implementation details. 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.
3np 2y ago
> That's... not true? The language can just have an implicit conversion rule for convenience. 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/mainus/node12.html 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.
- kibwen 2y ago
  > What you are talking about is a language implementation detail that is orthogonal to reasoning about the type system. 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.

zarakshR 2y ago

> The language can just have an implicit conversion rule for convenience 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

lmm 2y ago
> the presence of an implicit conversion rule `T -> T?` amounts to the observation that `T <: T?`, where <: is the subtyping relation 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.
- zarakshR 2y ago
  > 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`.
  - lmm 2y ago
    > But surely, you can still use subtyping in other cases -- when it is already unboxed -- right? 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.
- dwattttt 2y ago
  > Not necessarily, because you might consider it acceptable for the implicit conversion to change the memory layout in this sense. 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.
  - lmm 2y ago
    > 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)
    - dwattttt 2y ago
      But isn't it being implicit what makes it a subtype? It doesn't have to be a pointer; integer coercion should also be considered a form of subtyping. 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)
      - lmm 2y ago
        My point is that allowing an A to implicitly convert to a pointer to A when calling a function that takes a pointer to A is reasonable, whereas always allowing that implicit conversion anywhere in your program is rather less so. The same applies to integer conversion; there are contexts in which it should maybe happen implicitly, but not everywhere.
masklinn 2y ago
> the presence of an implicit conversion rule `T -> T?` amounts to the observation that `T <: T?`, where <: is the subtyping relation 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).
- zarakshR 2y ago
  > because PHP and Javascript will implicitly convert back and forth 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!
- marcosdumay 2y ago
  Yes, numbers and strings are the same type in Javascript and PHP. And yes, a C++ constructor declares a subtype relation. That's the semantics of those languages.
- meltyness 2y ago
  Yeah I think this is "Deref coercion" in Rust.[0] 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-coercion https://doc.rust-lang.org/std/ops/trait.Deref.html#deref-coe...
  - meltyness 2y ago

manmal 2y ago

In Swift, String? is an alias to Optional<String>. Optional is an enumeration with two cases: some, and none, where the former has the non-nil value attached. I‘m not sure how that ties in with subtyping though.

ackfoobar 2y ago
> how that ties in with subtyping In Swift it does not. But in Kotlin, `String?` is not an enum (sum type), but instead means `String | null`, a union type.

tlb 2y ago

Implicit conversions from Foo? to Foo are a major footgun, because the point of returning a Foo? is to have the caller check for failure before assuming there's a Foo to use. Even C++ avoids the implicit conversion from optional<T> to T.

naasking 2y ago
Yes, but they were describing an implicit conversion going the other way around, eg. String <: String?.
kragen 2y ago
Does C++ support implicit coercion from T to optional<T>? I think it doesn't, but that would be the corresponding case.

clord 2y ago

I think that whole section of the post was "For example, in Kotlin," presumably these are true in that language.

wesselbindt 2y ago

Maybe I'm off the mark here, but in my mind the definition of subtype is as follows: t1 is a subtype of t2 if any instance of t1 is an instance of t2. Surely with this definition String is a subtype of String?. Every instance of String (i.e. every string) is an instance of String?, after all. 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.

seanmcdirmid 2y ago
String <: String? is true (Any non-null string is a possibly null string), but String? <: String isn’t true (Any possibly null string may not be a non-null string).
- wesselbindt 2y ago
  We're all in agreement there it seems.
  - seanmcdirmid 2y ago
    If you just state it as a logical quantified proposition, it’s pretty obvious unless the type is complicated (then you need to break it down into multiple logical quantified propositions).
    - wesselbindt 2y ago
      Yes of course, but again, I don't think anyone disagrees with you on this.

naasking 2y ago

> The language can just have an implicit conversion rule for convenience 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.

kragen 2y ago
I don't think subtyping and implicit coercions are really equivalent. What if your implicit coercions aren't transitive, or if different chains of possible implicit coercions give different results, or if implicit coercions change the in-memory representation of a value? In the last case, for example, reflectively examining the dynamic type will give different results.
- 3np 2y ago
  They aren't equivalent, they're in different domains and abstraction levels. Subtypes are an abstract notion in type theory and grammar while coercions are implementation details/syntax. > What if your implicit coercions aren't transitive Have an example in mind?
  - kragen 2y ago
    I think implicit coercions are a semantics issue, not an issue of implementation details. 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!
    - 3np 2y ago
      > I think implicit coercions are a semantics issue, not an issue of implementation details. 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.

3np 2y ago

> That's... not true? The language can just have an implicit conversion rule for convenience. 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/mainus/node12.html 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.

kibwen 2y ago
> What you are talking about is a language implementation detail that is orthogonal to reasoning about the type system. 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.