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 >