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

[weis@yquem.inria.fr (Pierre Weis)]

> Pierre Weis wrote:
> > In the next version of the compiler, you will have an extension to the
> > definition of types with private construction functions (aka ``private''
> > types) that just fulfills your programming concern: in addition to usual
> > private sum and record private type definitions, you can now define a type
> > abbreviation which is private to the implementation part of a module (see
> > note 1).
> > 
> At first glance, this improvement does satisfy my concerns, but I think
> it still falls short of optimal in ways that seem easy to fix.
> 
> > Since the values of a private type are concrete, it is much easier for the
> > programmer to use the values of the type abbreviation.
> > 
> This concerns me - I'd like to require explicit casting/coercion to
> create or use the internal value of the abstract type, maybe with an
> exception for literals.  Could you elaborate on this?

Values of a private type abbreviation are concrete in the sense that they are
public and not hidden to inspection. However, a value of the private type
abbreviation has a type that is the one of the private type, not the one f
the abbreviated expression. To project such a value you need some syntactic
construct: either a (identity) function call or a sub-typing constraint as
already proposed on this list.

To create a value of the private type abbreviation, you must use the
construction function (as usual with private types, you cannot freely crete
values, you must use the provided injection).

> > This solution does not require any additional tagging or boxing, only the
> > usage of injection/projection function for the type. As for usual private
> > types, the injection function is handy to provide useful invariants (in the
> > row type example case, we get ``a row value is always a positive integer'').
> > 
> With a bit of low-level support, I imagine it not difficult to implement
> the following:
> 
> type row = private int constraint (fun i -> i >= 0)
> 
> such that the compiler uses the provided constraint function to check
> any (x :> row) casts, throwing an exception(?) on false. This solution
> wouldn't involve the module system just to have positive integer types,
> and gets rid of the function call overhead on 'from'.

The function call overhead can be avoided easily, if the from function is
provided by the compiler or if we use a sub-typing constraint row :> int.

On the other hand, the construction you proposed also applies to abstract
types: we need module to define an abstract type; we can have something
lighter such as a direct abstract type definition:

type rat = abstract {
     numerator : int;
     denominator : int;
  } with

  let make_rat n d = ...
  and numerator {numerator = n} = n
  and denominator ...

  let plus_rat r1 r2 = ...
  let mult_rat r1 r2 = ...

  ...

> > In addition, the private abbreviation is publicly exposed in the interface
> > file. Hence, the compiler knows about it: it can (and effectively does)
> > optimize the programs that use values of type row in the same way as if the
> > type row were defined as a regular public abbreviation.
> > 
> Does this mean I can do:
> 
> let one (r:row) = r+1
> let onea (r : row) = r = 1
> let two (r:row) (i:int) = r+i
> let three : row -> string = function 3 -> "three" | _ -> "not three"

No, you must explicitely project row values to int values (even if this is an
identity):

let one r = from r + 1
let onea r = from r = 1
let two (r:row) (i:int) = from r + i
let three : row -> string =
  fun r -> match from r with
  | 3 -> "three" | _ -> "not three"

> > Last but not least, being an instance of the identity function, the from
> > projection function is somewhat generic: we can dream to suppress the burden
> > of having to write it for each private type definition, if we find a way to
> > have it automatically associated to the new private type by the compiler.
> > 
> The use case for this feature is restricted construction to enforce
> invariants, no?

Yes.

>  Anything more complex should probably be totally
> abstract and not simply private.  In which case, the constraint keyword
> seems an effective way to tell the compiler what to do, and just let :>
> coercions do their magic.

Given that the injection function (the make function or the constraint part
of your construction) must enforce arbitrarily complex invariants, we may
need a module for private abbreviation as well (imagine for instance a
private abbreviation for prime numbers, that only injects into the prime type
integer arguments that are indeed prime numbers: you may need some room to
define the predicate!).

Thank you for your suggestions.

Best regards,

-- 
Pierre Weis

INRIA Rocquencourt, http://bat8.inria.fr/~weis/