So, one way we can get unification is by doing it in “the stupidest way possible”, i.e. by just saying “this is so”. We introduce type quotients (I’m guessing the type theorists have their own name for this concept). Essentially, we’d want to allow introduction of rules like the following (warning, ad-hoc syntax).
quot<A, B> UnitMul<A, B> = UnitMul<B, A> where ..;
More specifically, we have a grammar like
quot_type := "quot" TyParams? Ty = Ty Where? ";"
which does more-or-less what you expect: two copies of Mul are glued together along the given equality. Unfortunately there’s a few problems with this:
- There’s no good way to say “ah yes this is how these types are equivalent”, unless we require the types to both be ZSTs or uninhabited, unless we require a
const body after the declaration or whatever.
- This is probably a coherence and inference disaster.
As a neat example, type aliases desugar to quotients:
type New<T, ..> = Ty<F<T>, ..>;
// becomes
struct New<T, ..> = { /* fields of Ty<F<T>, ..> */ }
quot<T, ..> New<T, ..> = Ty<F<T>, ..> where ..;
which is admittedly a pretty silly example.
I rather like this solution, because it doesn’t require us to bake units into the language, and we can build much more hilariously complicated structures than what is essentially the polynomial ring Z[x1, x2, ...]. Of course, it’s also hilariouslly unfeasible.