From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p8QCDUGu022980 for ; Mon, 26 Sep 2011 14:13:30 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: An4BAI1rgE7RVdY2imdsb2JhbABBmUyOOggUAQEBCgkNBxIGIoFTAQEBBBICEwsBBQgBGxwCAwwGBQsWFg8JAwIBAgEREQEFARwTCAEBHodYBJ1FCotMglyEUzuIbgIDBocFBJNShSKBKoY9PYNv X-IronPort-AV: E=Sophos;i="4.68,444,1312149600"; d="scan'208";a="110539899" Received: from mail-bw0-f54.google.com ([209.85.214.54]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 26 Sep 2011 14:13:25 +0200 Received: by mail-bw0-f54.google.com with SMTP id zs8so9521653bkb.27 for ; Mon, 26 Sep 2011 05:13:25 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=message-id:date:from:user-agent:mime-version:to:subject:references :in-reply-to:content-type:content-transfer-encoding; bh=ntRyUGoWbZcRdzf1Ki7+wDqo5GUOgg+O2NBJNXvCZDQ=; b=kTZgyCE8thGWp9N5Z5VBL06xx9oDrMd7BYSoLB6c0SxSiURPDQuKeBV4bZiTYjc/q3 bj0vl33ydNWVlRNFU9u0i++am4U96gy7p0FXrkFBot9ryhDYHN3ibLlGaznm77ukTuqI k36bRvbrCGTrYbcNDY4kMUnp69xGnOJ6D0HYQ= Received: by 10.204.156.15 with SMTP id u15mr391155bkw.401.1317039205008; Mon, 26 Sep 2011 05:13:25 -0700 (PDT) Received: from [192.168.1.20] (APuteaux-154-1-32-171.w83-199.abo.wanadoo.fr. [83.199.87.171]) by mx.google.com with ESMTPS id af16sm20632310bkc.10.2011.09.26.05.13.23 (version=TLSv1/SSLv3 cipher=OTHER); Mon, 26 Sep 2011 05:13:24 -0700 (PDT) Message-ID: <4E806C6F.5050407@gmail.com> Date: Mon, 26 Sep 2011 14:13:35 +0200 From: Denis Berthod User-Agent: Mozilla/5.0 (Windows NT 5.1; rv:6.0.2) Gecko/20110902 Thunderbird/6.0.2 MIME-Version: 1.0 To: caml-list@inria.fr References: <10F5DBD5-5387-408C-967B-50B37367A6E1@lasmea.univ-bpclermont.fr> In-Reply-To: <10F5DBD5-5387-408C-967B-50B37367A6E1@lasmea.univ-bpclermont.fr> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 8bit Subject: Re: [Caml-list] Dependent types ? Hello, I think that achieving something very near from what you whant is relatively easy using phantom types. That avoid the boxing/unboxing in records. type i16 type i32 module SizedInt: sig type 'a integer val int16: int -> i16 integer val int32: int -> i32 integer val add: 'a integer -> 'a integer -> 'a integer end = struct type 'a integer = int let int16 x = x let int32 x = x let add x y = x + y end then open SizedInt let bar = let x = int16 42 in foo x must have type i16 integer -> i16 integer Regards, Denis Berthod Le 26/09/2011 13:42, Jocelyn Sérot a écrit : > 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 * int -> int > > 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 > * int -> int <2*n> ... > > >