14

Type system with (type) classes and subtyping?

 4 years ago
source link: https://ice1000.org/2020/08-01-TraitWithSubtyping.html
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
neoserver,ios ssh client

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?


report

Recommend

About Joyk


Aggregate valuable and interesting links.
Joyk means Joy of geeK