▲ | chriswarbo 3 days ago | |
The role of unification in type systems is interesting here, e.g. for the problem of incompatible set orderings we would like the type of `union` to be something like:
This allows any `O : Ord<T>` we like, as long as both `Set` values have the same one. However, it's not clear what "the same" would mean. A whole-program compiler could see whether both symbols unify (i.e. they point to the same thing); but separate compilation would require a system for referencing/naming each implementation, which would come with its own headaches (e.g. stability across versions, avoiding clashes, etc.). The article mentions an approach based on naming, which I assume is related. Maybe it's time to content-address our definitions like Unison does? |