Le 26 sept. 11 à 18:44, Gabriel Scherer a écrit :
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>.
Yes. Good point. Thanks for the idea.
IIUC, my add function would be declared as :
val add : 'a sized_int * 'a sized_int -> 'a sized_int
then, with
val x : size16 sized_int
val y : size16 sized_int
the type infered for z in
let z = add (x,y)
will be
z : size16 sized_int
Am i right ?
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.
Thanks for the pointer. I'll have a look at this.
But i'm afraid that this would require a too profound change in the
implementation of the type system..
Jocelyn
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
