3 ms·

> 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 i

by 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.

by 3np 2y ago

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.