Type constructors based on capabilities of type arguments?

Recently I was coding up libraries in one of my hypothetical toy languages (I hope I'm not the only one :), and I came across a potentially novel (too me) type feature that might actually make sense. So naturally, I wonder if this has been examined before.

Imagine a simple type constructor Vector[T]. I would like to have Vectors be comparable for equality, but *this* feature is only possible if the actual type parameter T is also comparable for equality.

So we might have some silly syntax like this.


mixin Eq[T] is def? ==(T,T):Bool; end

class Vector[T] mix (Eq when T <: Eq) is
...some stuff...
--
-- Compare two Vector[T]'s for equality
--
def ==(rhs:Self):Bool =
self.len = rhs.len and
(_ == _).andmap(self, rhs); -- this compares the elements

...some other stuff...
end


Hopefully one gets the idea. Furthermore, what I really want is not to *require* T <: Eq, but to simply notate and elide the methods that depend upon T <: Eq, most notably avoiding writing a gazillion different Vector[T] classes, each featuring some different interesting quality of T that happens to affect an interesting quality of the resulting Vector[T].

Has any other person smarter than I am explored type systems(other than the "uber search and replace" C++ templates) that feature this kind of "capability parametrized" parametrically polymorphic type system with method elision/disqualification before?

Much thanks,

Scott

Comment viewing options

C++ Concepts - a proposal for C++0x that didn't make it in - was focused on this sort of type analysis. One of the goals was to simplify error messages for template failures.

Related: [1], [2].

Haskell's Type Classes also support the features for which you're looking here. A 'type class' uses the nominative typing features of Haskell to associate an operation with a value based on its inferred type. Something like the above example would be:

 Eq a => [a] -> [a] -> Bool

Though Eq and Show are often derived automatically.

Derived vs. inferred

Though Eq and Show are often derived automatically.

I think that one has to be a little careful with this statement. It is true that the type constraint Eq will sometimes appear in a type signature even if not explicitly stated:
 (==) :: (Eq a) => a -> a -> Bool 
but I think that this should be called inference, not derivation, for the benefit of those not familiar with Haskell. Using ‘derived’ seems to invite confusion with deriving clauses of the form
 data Set a = [a] deriving (Eq, Show) 
where something else entirely (the automated generation of code implementing instances of Eq and Show) is happening.

I used 'derived' in

I used 'derived' in reference to the 'deriving' clause and the automated generation of code implementing instances of Eq and Show. (I can see how the context in which I used it causes confusion, though.) I agree with your distinction between 'derived' vs. 'inferred'.

Yep

The original post does seem like the classic motivation for Haskell's type classes. :-)

HaXe sort of does it, so I assume OCaml also?

http://haxe.org/ref/type_params

See Constraint Parameters

You could 'sort of' achieve

You could 'sort of' achieve it with a subclass as in
 class VectorEq <T : Eq> extends Vector <T>, implements Eq { compare (...) } 

..but that creates further problems because there are now two classes that you have to explicitly choose between everywhere, especially when extending.

Secondly, haXe is not too closely related to OCaml so I don't believe the assumption is appropriate.