Hello,
I think that achieving something very near from what you whant is
relatively easy using phantom types.
That avoid the boxing/unboxing in records.
type i16
type i32
module SizedInt:
sig
type 'a integer
val int16: int -> i16 integer
val int32: int -> i32 integer
val add: 'a integer -> 'a integer -> 'a integer
end
=
struct
type 'a integer = int
let int16 x = x
let int32 x = x
let add x y = x + y
end
then
open SizedInt
let bar =
let x = int16 42 in
foo x
must have type i16 integer -> i16 integer
Regards,
Denis Berthod
Le 26/09/2011 13:42, Jocelyn Sérot a é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<s> * int <s> -> int<s>
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<n>
* int<n> -> 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
