> Is there a language like this already? Yeah, you're looking for typeclasses a la Lean; probably Agda and Coq as well but Lean (3 or 4) is really built around

> Is there a language like this already? Yeah, you're looking for typeclasses a la Lean; probably Agda and Coq as well but Lean (3 or 4) is really built around typeclass inference. Basically "typeclasses" are arbitrary types (not necessarily "classes" which are basically vtables) which can appear as a special kind of implicit argument. They can be given explicitly, but when inferred, the type is looked up in both a global and a local table for a registered value. The way this works is you might have a class `dec_order : (T : Type) -> Type` with a function `lt : T -> T -> bool` and then you can write a function `sort : (T : Type) [inst : dec_order T] -> list T -> list T`. By declaring an `instance : dec_order int` then you can now sort lists of integers. But you could also pass an explicit argument to `sort` so that, as in the example in the article, you can sort a list of indices into some other list using a comparison function which closes over that list. It really is the best of both worlds, traits/interfaces vs explicit vtables. But you probably wanted to skip the whole dependent types thing. So I guess I repeat the original question, but with the caveat "without dependent types"? In 30 years and this will be the new great thing for 10 more after that. You heard it here first.