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)
- 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
>