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 p8RMDCM9002426 for ; Wed, 28 Sep 2011 00:13:12 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ap0DACFJgk5QDPJ9kGdsb2JhbABBhGWBeZIsjwwBAQEBCQkNBxQDI4F9BCIlQAIJHQJHPQmHXwSZfY1qkWaBLIFsgmKBEQSTUoFdj1k X-IronPort-AV: E=Sophos;i="4.68,451,1312149600"; d="scan'208,217";a="121835820" Received: from smtp03.smtpout.orange.fr (HELO smtp.smtpout.orange.fr) ([80.12.242.125]) by mail1-smtp-roc.national.inria.fr with ESMTP; 28 Sep 2011 00:13:07 +0200 Received: from LENOVO-R60 ([90.29.110.75]) by mwinf5d57 with ME id dyDp1h0061depua03yDqAi; Wed, 28 Sep 2011 00:13:51 +0200 X-ME-engine: default From: "Damien Guichard" To: caml-list@inria.fr Content-Type: multipart/alternative; charset="UTF-8"; boundary="6DNsLwLOD=_VZ1esd0WrKgxQCM5nA2Xj9h" MIME-Version: 1.0 Date: Wed, 28 Sep 2011 00:12:58 +0200 Message-ID: <558697822355394825@orange.fr> X-Mailer: EssentialPIM Portable v. 3.12 X-Validation-by: alphablock@orange.fr Subject: [Caml-list] Dependent types ? This is a multi-part message in MIME format --6DNsLwLOD=_VZ1esd0WrKgxQCM5nA2Xj9h Content-Type: multipart/alternative; boundary="Q8=_VjmflwAHLhX6WZ54iPyYmCIG63ljuL" --Q8=_VjmflwAHLhX6WZ54iPyYmCIG63ljuL Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 =3D | Word of 'a | DWord of ('a * 'a) size type n16 =3D int size type n32 =3D (n16 * n16) size type n64 =3D (n32 * n32) size add : 'a size -> 'a size -> 'a size=20 mul : 'a size -> 'a size -> ('a * 'a) size=20 div : ('a * 'a) size -> 'a size -> ('a size * 'a size) - damien Le 26/09/2011 =C3=A0 13:42, "Jocelyn S=C3=A9rot" =C3=A0 =C3=A9crit : >Hello, > >I've recently come across a problem while writing a domain specific=20 >language for hardware synthesis (http://wwwlasmea.univ-bpclermont.fr/Perso= nnel/Jocelyn.Serot/caph.html >). >The idea is to extend the type system to accept "size" annotations for=20 >int types (it could equally apply to floats). >The target language (VHDL in this case) accept "generic" functions,=20 >operating on ints with variable bit width and I'd like to reflect this=20 >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 =3D 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=20 >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=20 >Paretto, .. ) and dependent types (DML for ex), but my goal is far=20 >less ambitious. >In particular, i dont want to do _computations_ (1) on the size (and,=20 >a fortiori, don't want to prove anything on the programs). >So sized types / dependent types seems a big machinery for a=20 >relatively small goal. >My intuition is that this is just a variant of polymorphism in which=20 >the variables ranged over are not types but integers. >Before testing this intuition by trying to implement it, I'd like to=20 >know s/o has already tackled this problem. >Any pointer - including "well, this is trivial" ! ;-) - will be=20 >appreciated. > >Best wishes > >Jocelyn > >(1) i.e. i dont bother supporting declarations like : val mul : int=20=20= =20 >* int -> int <2*n> ... > >=20 > >--=20 >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 --Q8=_VjmflwAHLhX6WZ54iPyYmCIG63ljuL Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
That's pretty cool, everyone and his mother has a solution to= the proposed problem.
I think, for the sake of exhaustivity, i can sh= are my own weird hack.
It can express all power of 2 sizes (for exampl= e add, mul and div).
It uses a nested data type.


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

 =   type n16 =3D int size
   type n32 =3D (n16 * n16) siz= e
   type n64 =3D (n32 * n32) size

   a= dd : 'a size -> 'a size -> 'a size
   mul : 'a size -= > 'a size -> ('a * 'a) size 
   div : ('a * = 'a) size -> 'a size -> ('a size * 'a size)


- = damien


Le 26/09/2011 à 13:42, "Jocelyn S&eacut= e;rot"=20  à écrit :
>Hello,
>
&g= t;I've recently come across a problem while writing a domain specific
>language for hardware synthesis (http://wwwlasmea.univ-bpclermont.fr/P= ersonnel/Jocelyn.Serot/caph.html
>).
>The idea is to exten= d the type system to accept "size" annotations for
>int = types (it could equally apply to floats).
>The target language (VHD= L in this case) accept "generic" functions,
>operating o= n ints with variable bit width and I'd like to reflect this
>in th= e source language.
>
>For instance, I'd like to be able to = declare :
>
>val foo : int * int -> int
>
&= gt;(where the type int is not annotated, i.e. "generic")
>= ;
>so that, when applied to, let say :
>
>val x : i= nt<16>
>val y : int<16>
>
>(where <1= 6> is a size annotation),
>
>like in
>
>= let z =3D foo (x,y)
>
>then the compiler will infer type in= t<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, i= t has to do with the theory of sized types (Hughes and
>Paretto, .= . ) and dependent types (DML for ex), but my goal is far
>less amb= itious.
>In particular, i dont want to do _computations_ (1) on the= size (and,
>a fortiori, don't want to prove anything on the progr= ams).
>So sized types / dependent types seems a big machinery for a=
>relatively small goal.
>My intuition is that this is jus= t a variant of polymorphism in which
>the variables ranged over ar= e not types but integers.
>Before testing this intuition by trying = to implement it, I'd like to
>know s/o has already tackled this pr= oblem.
>Any pointer - including "well, this is trivial" != ;-) - will be
>appreciated.
>
>Best wishes
&= gt;
>Jocelyn
>
>(1) i.e. i dont bother supporting d= eclarations 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 --Q8=_VjmflwAHLhX6WZ54iPyYmCIG63ljuL-- --6DNsLwLOD=_VZ1esd0WrKgxQCM5nA2Xj9h--