Thanks to all for your answers. Phantom types could be a solution but we must declare a new type for each possible size, which is cumbersome / annoying. Moreover, since i'm writing a DSL, the fact that they do not require a modification to the existing type system is not really an advantage. My language has its own type system (largely inspired from OCaml's) so what I was looking for was more a way to modify the type representation to support the requested behavior. To those familiar with Caml compiler source code, i was wondering if i could hack the following definitions (from types. ml) type typ = | TyVar of typ_var | TyTerm of string * typ list and typ_var = { mutable level: int; mutable value: tyvar_value } and tyvar_value = | Unknown | Known of typ by adding a notion of "size variable" (sorry if this sounds imprecise, this is still a but hazy in my mind..) type typ = | TyVar of typ_var | TyTerm of string * typ list * typ_size and typ_sz = { mutable value: tysz_value } and tyvar_value = | Unknown | Known of int and update the unification engine accordingly.. Well, the easiest answer is maybe just to try :-S I'm just a bit surprised that no one seems to have proposed such an extension yet. Jocelyn Le 26 sept. 11 à 14:45, Yaron Minsky a écrit : > As written, the behavior of the types might not be what you expect, > since addition of two 16 bit ints may result in an int that requires > 17 bits. > > When using phantom types, you need to be especially careful that the > types mean what you think they mean. > > On Sep 26, 2011 8:13 AM, "Denis Berthod" > wrote: > > 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 * 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 > >