From mboxrd@z Thu Jan  1 00:00:00 1970
X-Sympa-To: caml-list@inria.fr
Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82])
	by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p8QBh3wb021408
	for <caml-list@sympa-roc.inria.fr>; Mon, 26 Sep 2011 13:43:03 +0200
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AvAAAOhjgE7D3XqWmWdsb2JhbABBqA4UAQEBAQEICwsHFCaCARECgT8+iA0EmnefAIYrYASMB4dLhSKMEw
X-IronPort-AV: E=Sophos;i="4.68,443,1312149600"; 
   d="scan'208";a="121465524"
Received: from ubpmes.univ-bpclermont.fr ([195.221.122.150])
  by mail1-smtp-roc.national.inria.fr with ESMTP; 26 Sep 2011 13:42:57 +0200
Received: from localhost (localhost.localdomain [127.0.0.1])
	by ubpmes.univ-bpclermont.fr (Postfix) with ESMTP id 554DA2A1B18
	for <caml-list@inria.fr>; Mon, 26 Sep 2011 13:42:57 +0200 (CEST)
X-Virus-Scanned: amavisd-new at univ-bpclermont.fr
Received: from ubpmes.univ-bpclermont.fr ([127.0.0.1])
	by localhost (ubpmes.univ-bpclermont.fr [127.0.0.1]) (amavisd-new, port 10024)
	with ESMTP id tGJDpqqqvPRW for <caml-list@inria.fr>;
	Mon, 26 Sep 2011 13:42:56 +0200 (CEST)
Received: from [172.27.1.69] (unknown [193.54.50.250])
	by ubpmes.univ-bpclermont.fr (Postfix) with ESMTP id 1E08B2A1A3C
	for <caml-list@inria.fr>; Mon, 26 Sep 2011 13:42:56 +0200 (CEST)
Message-Id: <10F5DBD5-5387-408C-967B-50B37367A6E1@lasmea.univ-bpclermont.fr>
From: =?ISO-8859-1?Q?Jocelyn_S=E9rot?= <Jocelyn.SEROT@ubpmes.univ-bpclermont.fr>
To: OCaML Mailing List <caml-list@inria.fr>
Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes
Content-Transfer-Encoding: 7bit
Mime-Version: 1.0 (Apple Message framework v935.3)
Date: Mon, 26 Sep 2011 13:42:51 +0200
X-Mailer: Apple Mail (2.935.3)
X-Validation-by: jocelyn.serot@ubpmes.univ-bpclermont.fr
Subject: [Caml-list] Dependent types ? 

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> ...