Hacker News new | past | comments | ask | show | jobs | submit login

> Instead, coercions are used to emulate some of the advantages of subtyping.

Maybe I missed it in the article, but what does subtyping give you that coercions don't?




Economy of thought.

In my opinion, subtyping declares a "is" relationship, and coercions declare a "can be viewed as" relationship. You would want both in Practal. Subtyping is more tricky than coercions in the sense that if done wrongly, it can introduce inconsistencies, while coercions cannot (they just may fail to be unique).

For example, ℕ should be a subtype of ℝ. Because a natural number IS a real number. Let's say you have the theorem `∀ x : ℝ. P x` for some predicate `P`. With subtyping, also the theorem `P n` holds for any `n : ℕ`. With coercions, only the theorem `P (c n)` holds, where `c : ℕ → ℝ` is the coercion. Now you have an additional constant `c` in your theorem. It makes things more complicated than they have to be. Sure, some pretty printing and nifty automation can help you a lot here, but why would you want to deal with that added coercion tax in the first place for cases where you don't have to?


While I'm not sure it's impossible (though if it's possible I doubt it would be pretty or non-fragile), I've at least never seen anybody emulate generic intersection/union types using coercions. Dependent intersections like in Cedille are definitely impossible.


Very good point.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: