Re: [Caml-list] Compiler feature - useful or not?

[Edgar Friendly <thelema314@gmail.com>]

Fernando Alegre wrote:
> Even better would be to have a "parametrized finite" type. This would
> really need to be built into the compiler, as I don't think it can
> actually be emulated by either camlp4 or the C interface.
> 
> The idea is very simple: add a primitive "n finite" type to the
> language, where n is a positive integer constant.
> 
> For example:
> 
> type bit = 2 finite
> 
> type mod3 = 3 finite
> 
> Then, fill the type by coercion so that "(x :> n finite)", where both x
> and n are known to be constant at compile-time and 0 <= x < n, becomes a
> value of type "n finite".
> 
> This should be pretty straightforward to implement, and it may simplify
> code that depends on types such as "T1 | T2 | T3 | T4"
> 
> I don't know how much it would be possible to relax the constraint above
> while maintaining the typesystem sound. Does anybody whether this is
> a known problem?
> 
> Thanks,
> Fernando
> 
To implement these types (as well as what I've just proposed), the
interface between the type system and the runtime will have to change.
As Jacques pointed out, a coercion, being a type-level action, cannot
generate any code, and in order to do runtime coercion to a restricted
type, you need value checks to ensure a valid value.

I hope that it won't hurt my brain too much to see what can be done to
create such a bridge between the type system and the code generator,
even if INRIA never accepts the idea into the official OCaml distribution.

If you'd like to look at how another language implemented these ideas,
look here: http://www.adapower.com/rm95/RM-3-5-4.html

E.