Re: [Caml-list] record labels of record scope using camlp4

[Alain Frisch <frisch@clipper.ens.fr>]

On Thu, 17 Jan 2002, Didier Remy wrote:

> > Another way would be to use type information provided by the type-checker.
> > For accessing field, here is a description of a simple patch to the
> > type-checker that could be handy; the idea is that, when the expression e
> > is known to be a record of a given type, one can use a "record scope" rule
> > for label.
>
> Isn't this just a form of static and local resolution of overloading?

Yes.

> However, local resolution does not commute with unification...
> Hence, the specification of well-typed programs should then strongly
> depend on the order in which unifications (i.e. type inference) are
> performed. Do you have a specification of well-typed programs but
> the type-inference algorithm itself?

No, but I'm not sure how important it is for the ``Real Life''.
How many people fully understand OCaml type system (including subtleties
with variant types and objects) ?  Maybe it is because I am just a
newcomer to OCaml (3 years), but I don't, and the fact that the full type
system _could_ be formalized in a nice formal system is not a big help
for me _as a programmer_ (and as far as I can tell, OCaml type system
is fully specified nowhere).

For the specific case, it is easy to give informal sufficient conditions
of well-typedness ("a type annotation must allow to know the record
type constructor [not the type arguments] for the record expression
before its use"). Note that this condition is too strong, as
it does not cover this case:

# type t = { x : int };;
type t = { x : int; }
# let f () = { x = 2 };;
val f : unit -> t = <fun>
# type s = { x : string };;
type s = { x : string; }
# (f ()).x;;
- : int = 2

> It is true that Ocaml differs from the nice theory of core ML in a few
> places.  However, we have tried to keep those differences as
> unsignificant as possible, and as few as possible.
>
> For example, a module with a weak type variable in its principal signature
> is rejected, while any ground instantiation of this weak type variable would
> be accepted, so, yes: ``Ocaml does not have principal types''. However, type
> inference is still easy to specify, and in particular does not rely in which
> operations are performed.

Note that the patch I proposed was not a suggestion for inclusion in
OCaml; I think it solves in a light way a practical problem (theoretical
non-issue) encountered by many people, but I know it is not really in
OCaml spirit.




Alain

-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr