There's more between the two type systems than "one is static, one is dynamic".
Conversation
Another reason it shouldn't count as type coercion is that the two phrases have the same type. So I see it more as sugar/diff ways to write same thing, like 1:2:3:[] vs [1,2,3] while also a short-hand that didn't age well.
2
1
Type Coercion is not sound but parametric polymorphism is a very deep concept that relies on concepts that reach further than just programming languages.
1
1
*cough* GHC's Core language has type-safe coercions. It just makes you carry around the proof that they're safe before you actually use them, and they're for things like GADTs.
1
4
Hmm I think carrying around a proof is convincing not coercion :p
1
Heh - perhaps, but they've been called coercions in the literature since at least the 80s (including systems that translated legit subtyping into explicit coercion calls).
You're just not trying to coerce a mountain with a banana in the back :-)
1
2
Consider perhaps that when comparing JS and Haskell I was intentionally using a non-rigorous definition of coercion.
I think it would be a reasonable definition to say that type inference is coercing source code to a checkable model.
2
Not in a compsci setting.
We use the term "elaborating", it's a semantically-aware transformation into a different (if related) language.
In the case of Haskell it's not one that has the kind of subtyping you see in OO languages and their descendants, or C-style coercion.
1
2
It still works utterly differently to a dynamically-typed language with runtime value coercions.
Personally, if I'm going to use dynamic typing that's one thing I can go without.
1
I feel a bit like you all have some dictionary you agreed upon beforehand that I haven’t read.
I made a flippant remark that the type refinement of “List a” into “List Char” is superficially similar to how JS coerces to strings for comparison!
I’m writing a tweet, not a paper!
2
I guess we're just trying to help make it clearer because it's an interesting, important distinction. 😃 I can definitely see why it looks superficially _like_ coercion, even though it would be muddying definitions to call it that.