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 p8S7S3f2026551 for ; Wed, 28 Sep 2011 09:28:03 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AkgDACrLgk7RVdY2imdsb2JhbABBhGWUKI5zCBQBAQEKCQ0ZBiKBUwEBAQQSAg8EGQEIExILAQMMBgMCCwMTBB0CAg8CEhEBBQEKEgYNAQcBAQ4JB4dYBJs1CosIRIJchRE7iG4CBAaDEoJigREEglSQfoUigSqGPj2Dbw X-IronPort-AV: E=Sophos;i="4.68,454,1312149600"; d="scan'208,217";a="121921305" Received: from mail-bw0-f54.google.com ([209.85.214.54]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 28 Sep 2011 09:27:57 +0200 Received: by bkbzs8 with SMTP id zs8so13026475bkb.27 for ; Wed, 28 Sep 2011 00:27:57 -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:cc:subject :references:in-reply-to:content-type; bh=0Q/wNQsTJwmKQziEVKcNUpch6A7+iqfwXv8n1+fXo2A=; b=VBFAuKLi2o9iJKlAEOtDAzorXaAQJoa2Xhxxt4Pyf3AheIUXnF8qlBWvcmLqxiUt1B TlUrdCORIvUoy2JiXw4OBDmjej7MTsBnvbfT0D7+VmyJY3w1exlAX2b6p1/jsU2Gt0CS Rir8l9Wjrrf2c+IN4gWkLdMplLUpSKm8Ckzms= Received: by 10.204.132.23 with SMTP id z23mr5814556bks.383.1317194875797; Wed, 28 Sep 2011 00:27:55 -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 z9sm27121235bkn.7.2011.09.28.00.27.50 (version=TLSv1/SSLv3 cipher=OTHER); Wed, 28 Sep 2011 00:27:53 -0700 (PDT) Message-ID: <4E82CC7B.10808@gmail.com> Date: Wed, 28 Sep 2011 09:27:55 +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: Damien Guichard CC: caml-list@inria.fr References: <558697822355394825@orange.fr> In-Reply-To: <558697822355394825@orange.fr> Content-Type: multipart/alternative; boundary="------------090505010007050303000402" Subject: Re: [Caml-list] Dependent types ? This is a multi-part message in MIME format. --------------090505010007050303000402 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Le 28/09/2011 00:12, Damien Guichard a écrit : > > That's pretty cool, everyone and his mother has a solution to the > proposed problem. > I think, for the sake of exhaustivity, i can share my own weird hack. > It can express all power of 2 sizes (for example add, mul and div). > It uses a nested data type. > > > type 'a size = > | Word of 'a > | DWord of ('a * 'a) size > > type n16 = int size > type n32 = (n16 * n16) size > type n64 = (n32 * n32) size > > add : 'a size -> 'a size -> 'a size > mul : 'a size -> 'a size -> ('a * 'a) size > div : ('a * 'a) size -> 'a size -> ('a size * 'a size) div (2. ** 32.) 1. might be a problem here. Denis. > - damien > > > Le 26/09/2011 à 13:42, "Jocelyn Sérot" à é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> ... > > > > > > > >-- > >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 > > > > > -- > Mail created using EssentialPIM Free - www.essentialpim.com > --------------090505010007050303000402 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: 8bit Le 28/09/2011 00:12, Damien Guichard a écrit :

That's pretty cool, everyone and his mother has a solution to the proposed problem.
I think, for the sake of exhaustivity, i can share my own weird hack.
It can express all power of 2 sizes (for example add, mul and div).
It uses a nested data type.


  type 'a size =
   | Word of 'a
   | DWord of ('a * 'a) size

   type n16 = int size
   type n32 = (n16 * n16) size
   type n64 = (n32 * n32) size

   add : 'a size -> 'a size -> 'a size
   mul : 'a size -> 'a size -> ('a * 'a) size 
   div : ('a * 'a) size -> 'a size -> ('a size * 'a size)

div (2. ** 32.) 1. might be a problem here.

Denis.

- damien


Le 26/09/2011 à 13:42, "Jocelyn Sérot"  à é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> ...
>
>
>
>--
>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
>

--
Mail created using EssentialPIM Free - www.essentialpim.com

--------------090505010007050303000402--