Type system with (type) classes and subtyping?

by

Normally, programming languages with typeclasses (aka traits) do not have subtyping polymorphism à la Java, like Haskell and Rust. By trait I mean “proper trait”, unlike Scala’s, which is just a composable version of Java interfaces.

Question: what if we mix subtyping with typeclasses? (this was asked on a Chinese website, by me :D)

Problem

So, I have answered the question myself, by presenting the following problem:

Given these Java-style definitions:

class Dad { }
class Kid extends Dad { }

We got a type Kid that is a subtype of Dad. Then, with the following Rust-style traits:

trait Add {
  fn add(Self, Self) -> Self;
}

We may create an implementation of Add, for type Dad:

impl Add for Dad {
  // implementation omitted.
}

Then, we may obtain two variables a and b, both of type Kid. By invoking Add::add(a, b), we may expect the result to be of type Kid, because two kids get added together would probably give you a Kid back.

However, the only available trait implementation is impl Add for Dad, so in fact we may infer the type of expression Add::add(a, b) to be Dad.

This doesn’t seem right, because intuitively you may expect add to return a value of the same type as the arguments.

Solution

So, I’d like to present a new restriction on type systems like this:

When extending a class or implementing an interface, you’re supposed to also implement all the traits that the super type has already implemented.

By doing this, the definition above will not check – you’ll have to provide the following implementation:

impl Add for Kid {
  // ...
}

This will make Add:add(a, b) return Kid when a and b are both Kid.

Is that all?

Of course not. There’s still another question: what if we have c of type Dad, and we have expression Add::add(a, c)? If we dispatch the invocation to impl Add for Kid, we won’t check because c is not of type Kid. If we dispatch the invocation to impl Add for Dad, we’re getting add to be of type Kid -> Dad -> Dad. This still doesn’t seem right.

I haven’t got a proper thought on this yet. Maybe we can restrict trait method invocation to exactly-matched types?

Is there any trade-off for this?


Tweet this Top

License

This work (Type system with (type) classes and subtyping?) is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

License



Create an issue to apply for commentary