From mboxrd@z Thu Jan 1 00:00:00 1970 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 p8QC7ZlJ022597 for ; Mon, 26 Sep 2011 14:07:35 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AlsBANxpgE5KfVM2kGdsb2JhbABBmRiObggUAQEBAQkJDQcUBCKBUwEBAQQSAhMZARMIEgsBAwwGBQsNDSEiAREBBQEKEgYTEgkHh1ydTQqLTIJchFA7iG4CAwaDEoNzBJNSjQk9g28 X-IronPort-AV: E=Sophos;i="4.68,444,1312149600"; d="scan'208";a="121469627" Received: from mail-gw0-f54.google.com ([74.125.83.54]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 26 Sep 2011 14:07:30 +0200 Received: by gwj18 with SMTP id 18so6679873gwj.27 for ; Mon, 26 Sep 2011 05:07:29 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; bh=WB6FY/+m6ojAqRz7kgv3GkVqmIPF6rG7k0YlV6CWSnM=; b=c9I82y8e1BknAYcsMNZS83bFjsA4tFnfiwvFFQYl9ajsyPdGBgofjwpSJvcvY539HM JzfUlR+4qaGsNC3rsyoyVaD7eOiO9hLrUD5dpIHKXXJxbJY8KKmTBG91VpwjCrE7Eqd/ j6TV1YWmM+OeSkdm8ZZOAyqlvOAUhThRRJECk= Received: by 10.42.144.72 with SMTP id a8mr2685251icv.131.1317038847085; Mon, 26 Sep 2011 05:07:27 -0700 (PDT) MIME-Version: 1.0 Received: by 10.42.172.65 with HTTP; Mon, 26 Sep 2011 05:07:07 -0700 (PDT) In-Reply-To: <10F5DBD5-5387-408C-967B-50B37367A6E1@lasmea.univ-bpclermont.fr> References: <10F5DBD5-5387-408C-967B-50B37367A6E1@lasmea.univ-bpclermont.fr> From: Thomas Braibant Date: Mon, 26 Sep 2011 14:07:07 +0200 Message-ID: To: =?ISO-8859-1?Q?Jocelyn_S=E9rot?= Cc: OCaML Mailing List Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id p8QC7ZlJ022597 Subject: Re: [Caml-list] Dependent types ? Hi, There was a somewhat related discussion some time ago: http://caml.inria.fr/pub/ml-archives/caml-list/2010/05/b2f6dda2453f395a23e0fbbc988a2e0a.en.html The idea was to define something like : type n16 type n32 type n64 type 'a sint = { value : int};; (* the record here is important *) let sint_plus (x : 'a sint) ( y : 'a sint) : 'a sint = {value = x.value + y.value};; With this solution you can not make computation the size, but it may be sufficient for your needs. Hope this helps. Thomas Braibant On Mon, Sep 26, 2011 at 1:42 PM, Jocelyn Sérot wrote: > 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> ... > > > -- > Caml-list mailing list.  Subscription management and archives: > https://sympa-roc.inria.fr/wws/info/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs > >