Lambda the Ultimate

In the next version of Coq there will be type-classes so we'll get a kind of ad-hoc polymorphism / overloading.

An example that was previously on LTU:
Genuine Shift Reset

Rewriting logic (as per Maude) subsumes the kind of subtyping seen in systems such as OBJ, so approaches to marry systems like Coq with rewriting logic can(*) give overloading for free.

There's a lot riding on that "can" of course, but I think that I am not the only person here who thinks that this may provide an exciting and principled way to approaching this.

• http://algebraist.crowdvine.com
• http://www.aldor.org

I was looking at a new language feature for my programming language and I wonder if that is dependent types and if it relates to dependent type overloading (though not to generics)

This is what I have in mind: the programmer can define inter-dependent values with a formula, and the formula is used both to calculate free variables and to validate bound variables. For example:

abstract Segment
{
DEFINE float x (
	if (x < lowerBound) lowerBound
	else if (x >= upperBound) upperBound - epsilon
	else x)
DEFINE float lowerBound (
	if (x < lowerBound) x
	else min(lowerBound, upperBound))
DEFINE float upperBound (
	if (x >= upperBound) x + epsilon
	else max(lowerBound, upperBound))
}

That defines 3 inter-dependent variables. Then I can bind one or more variables:

class Seg: Segment
{
	float x
	float lowerBound
	float upperBound = 5000.0
} 

Seg t(x: 30) => Seg(x = 30.0, lowerBound = 30.0, upperBound = 5000.0)
Seg u(x: 8000) => ERROR
 value does not satisfy definition of x, suggested value: 4999.99999998
Seg v => Seg(x = 4999.99999998, lowerBound = 4999.99999998, upperBound = 5000.0)

Would that qualify as dependent typing? As for subtyping, I believe that a class that binds x in addition to upperBound is not a subclass of Seg, since setting a value for lowerBound will not adjust x accordingly which will go against the assumptions of the programmer.

A more obvious example of this would be a system of coordinates x, y, rho and theta (cartesian and polar coordinates)
If the class Cart binds x and y, rho and theta are well defined. But if rho and theta are bound as well in a subclass of Cart this code will fail if eg. rho is bound to 1.0:

self.x = 5.0

I don't think overloading (ad-hoc) is all that wonderful. You can already get the same effect through parametric polymorphism (think modules) and it is much more principled.

IMO, of course, but this might explain the dearth of papers.

On the page of Nicolas Oury I found a paper First-Class Type Classes that discusses an implementation of type classes in Coq:

Type Classes have met a large success in Haskell and Isabelle, as a solution for sharing notations by overloading and for specifying with abstract structures by quantification on contexts. However, both systems are limited by second-class implementations of these constructs, and these limitations are only overcomed by ad-hoc extensions to the respective systems. We propose an embedding of type classes into a dependent type theory that is first-class and supports some of the most popular extensions right away. The implementation is correspondingly cheap, general and very well integrated inside the system, as we have experimented in Coq. We show how it can be used to help structured programming and proving by way of examples.