> Phantom types could be a solution but we must declare a new type for > each possible size, which is cumbersome / annoying.
If you define the type system yourself, you can easily add a family of type constants `size<n>` (with `n` an integer literal) to the default environment of the type checker. Then you can define a parametrized type `type 's sized_int` (or float, etc.) and instantiate it with any of the size<n>. One issue with this minimal -- in term of modifications -- mechanism is that you can represent meaningless types such as `float size_int` : `float` is not a size. The canonical way to handle this is to add a kind system on top of your type system, that would classify the types into different kinds. Usual types would have kind `★`, and sizes would have kind `Size`. You would then restrict the `'a` type variable in `sized_int` to be of kind `Size`: type ('a : Size) sized_int http://en.wikipedia.org/wiki/Kind_(type_theory) Remark: There is another useful way to combine kinds and sizes, which is to use "sized kinds" to classify types whose memory representation has a given size in your implementation. For example you would have a kind `★` for types of one machine word, `★2` for two machine words... This allows to keep parametric polymorphism in presence of non-uniform representations, but it is restricted, less general, as a given polymorphic definition would not quantify over all types, but on all types of a given kind – unless you introduce kind polymorphism, etc. It may be useful for typing low-level programs, but it doesn't look like what you're looking for here. On Mon, Sep 26, 2011 at 5:55 PM, Jocelyn Sérot <jocelyn.se...@ubpmes.univ-bpclermont.fr> wrote: > 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" <denis.bert...@gmail.com> 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<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 >> > > -- 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