Home » forums » LtU Forum

Dependent Types, Generic Programming and Overloading.

Being interested in dependent typed programming for a little while I noticed a slight peculiarity of the field: there are almost no papers on overloading in dependent typed setting.

The only paper is here: Dependent Types with Subtyping and Late-Bound Overloading.

There are a plenty of papers describing techniques for generic programming, like Generic Programming Within Dependently Typed Programming. But no overloading.

In my own opinion overloading is quite important for regular programming and its' absence can be a substantial barrier on entry.

(A little discussion of overloading was here: http://lambda-the-ultimate.org/classic/message1575.html In some implementations a function can return a Set, ie, Type (an example is let (A:* ---- wList A:*) in Generic Programming with Dependent Types, so dependency on value of argument seems to be at least as general as dependence on the type of argument. But again, no one shows how to use it.)

So, the questions are: What precludes dependent typed programming languages to have overloading? And what should one do to work around that?

By Serguey Zefirov at 2008-03-23 18:22 | LtU Forum | previous forum topic | next forum topic | other blogs | 7764 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Coq gets typeclasses

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

By Gavin Mendel-Gleason at Mon, 2008-03-24 15:01 | login or register to post comments

Rewriting logic

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.

By Charles Stewart at Tue, 2008-03-25 14:30 | login or register to post comments

Aldor is a dependent-typed programming language with overloading

See:
By billpage at Tue, 2008-03-25 16:37 | login or register to post comments

I was looking at a new

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

By Denis Bredelet -jido at Mon, 2008-04-21 23:07 | login or register to post comments

Dependent types are types

Dependent types are types that depend on values. I'm not sure where the types are in this example. This looks more like constraint programming, and I don't see how you're going to get this to work. Have you implemented this? Do you have an implementation in mind?

By Matt M at Tue, 2008-04-22 14:20 | login or register to post comments

Dependent values

I guess I was confused between dependent types and dependent values. What I was thinking of is a type like "number between 1 and 500", hence my example. That would be the type of x.

By Denis Bredelet -jido at Tue, 2008-04-22 19:17 | login or register to post comments

I did not implement it.

I did not implement it. The algorithm I had in mind would go like:

Seg t(x: 30)
=> set x to 30
=> x is defined:
DEFINE float x (
	if (x < lowerBound) lowerBound
	else if (x >= upperBound) upperBound - epsilon
	else x)
=> verify constraint
	if (x < lowerBound) lowerBound
=> lowerBound is defined:
DEFINE float lowerBound (
	if (x < lowerBound) x
	else min(lowerBound, upperBound))
=> cannot evaluate condition
	(x < lowerBound)
=> try with condition = true
=> lowerBound = x
=> verify constraint
	if (x < lowerBound) lowerBound
=> condition is false, verify constraint
	else if (x >= upperBound) upperBound - epsilon
=> upperBound is bound to 5000.0
=> condition is false, verify constraint
	else x
=> entered value: 30, calculated value: 30
=> SUCCESS

By Denis Bredelet -jido at Tue, 2008-04-22 19:55 | login or register to post comments

Parametric polymorphism

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.

By mrd at Tue, 2008-04-22 17:34 | login or register to post comments

Interesting example in Coq

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.

By Serguey Zefirov at Fri, 2008-05-23 00:35 | login or register to post comments