archives

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?