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