3 ms·

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

> 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.
      - kragen 2y ago
        It seems like you aren't thinking very clearly.
- naasking 2y ago
  I didn't say they were equivalent, I said they were both sound in that context. By "doesn't really matter", I meant in the sense that I had just described, eg. that it "cannot go wrong".
  - kragen 2y ago
    I agree, if we're talking about Milner's sense (he means roughly "can't produce a runtime error").

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.
    - kragen 2y ago
      It seems like you aren't thinking very clearly.
naasking 2y ago
I didn't say they were equivalent, I said they were both sound in that context. By "doesn't really matter", I meant in the sense that I had just described, eg. that it "cannot go wrong".
- kragen 2y ago
  I agree, if we're talking about Milner's sense (he means roughly "can't produce a runtime error").