[Caml-list] Dependent types ?

["Jocelyn Sérot" <Jocelyn.SEROT@ubpmes.univ-bpclermont.fr>]

Hello,

I've recently come across a problem while writing a domain specific  
language for hardware synthesis (http://wwwlasmea.univ-bpclermont.fr/Personnel/Jocelyn.Serot/caph.html 
).
The idea is to extend the type system to accept "size" annotations for  
int types (it could equally apply to floats).
The target language (VHDL in this case) accept "generic" functions,  
operating on ints with variable bit width and I'd like to reflect this  
in the source language.

For instance, I'd like to be able to declare :

val foo : int * int -> int

(where the type int is not annotated, i.e. "generic")

so that, when applied to, let say :

val x : int<16>
val y : int<16>

(where <16> is a size annotation),

like in

let z = foo (x,y)

then the compiler will infer type int<16> for z

In fact, the exact type signature for foo would be :

val foo : int<s> * int <s> -> int<s>

where "s" would be a "size variable" (playing a role similar to a type  
variable in, for ex : val map : 'a list -> ('a ->'b) -> 'b list).

In a sense, it has to do with the theory of sized types (Hughes and  
Paretto, .. ) and dependent types (DML for ex), but my goal is far  
less ambitious.
In particular, i dont want to do _computations_ (1) on the size (and,  
a fortiori, don't want to prove anything on the programs).
So sized types / dependent types seems a big machinery for a  
relatively small goal.
My intuition is that this is just a variant of polymorphism in which  
the variables ranged over are not types but integers.
Before testing this intuition by trying to implement it, I'd like to  
know s/o has already tackled this problem.
Any pointer - including "well, this is trivial" ! ;-) - will be  
appreciated.

Best wishes

Jocelyn

(1) i.e. i dont bother supporting declarations like : val mul : int<n>  
* int<n> -> int <2*n> ...