Re: [Caml-list] [ANN] RTT (Run-time types) online toplevel for trying

[tiphaine.turpin@free.fr]

----- Mail original -----
> De: "Adrien" <camaradetux@gmail.com>
> À: "Tiphaine Turpin" <Tiphaine.Turpin@free.fr>
> Cc: caml-list@inria.fr
> Envoyé: Dimanche 23 Décembre 2012 18:15:53
> Objet: Re: [Caml-list] [ANN] RTT (Run-time types) online toplevel for trying


[...]
> I've started playing with RTT through the Try RTT page (great idea
> btw) and I'm not sure how to handle the following type:
>   type 'a t = {
>     t : 'a;
>   }


Not sure what you are asking, but here a value representation of the type constructor t is defined together with it (with name _type_t), as you can see in the toplevel. For basic usage, you don't need to use this value directly, but it is involved when you manipulate a (value of) type u t for some type u. For example, if you evaluate {t = ()} or {t = [1; 2]}, then _type_t will appear in the dynamic type of thoses values. More precisely, if you evaluate Rtt.typeof {t = ()}, the result will be the type Tconstr (_type_t, [_type_unit]).

> Also, it would be nice to see Rtt_type a bit more documented (the
> purpose of some elements in rttype is unclear). Also, examples with a
> few types would be very valuable.

I admit that this is not much documented (partly because the actual representation of types does not matter for the most basic usage).

> 
> Apart from these two remarks, I'm happy with it so far and very
> interested. The web toplevel is quite slow but I guess camlp4 is
> pretty slow in javascript.

There is not Camlp4 involved. Rtt acts as a pre-processor (when used for compiling) but it uses the OCaml parser (and type-checker). As for this inefficiency, I haven't looked at its cause yet.

> Btw, are you aware of http://lexifi.com/blog/runtime-types ? It
> should
> provide support for runtime types too without camlp4. I don't know
> how
> likely or close it is to being integrated into ocaml.

Yes. My prototype addresses the same question as the work presented by Alain Frisch, but I consider the two things largely orthogonal, here is why:

The extended compiler made by Lexifi uses a "typed" GADT-based representation of types to ensure a sound manipulation of run-time types. This representation is much more elaborate than mine, also account for type abstraction, and it has been applied in real world for several purposes, like safe unmarshalling, GUI, and databases (quoting the blog post you mention). However, as far as I understand, the type which is made available (using the additional syntax "(type of expr)") is, at first, the static type (which is less acurate when polymorphism is involved). I understand that, by adding type arguments to polymorphic functions, this limitation can be lifted, and that part of these additional arguments can be inferred by the modified compiler. The reason for my proposal is to go further in this way, providing (mostly) "exact" dynamic types, in a fully automated way (type representation arguments are added systematically by a program transformation). This is however not simple for the full language, and the proof of concept that I proposed does not solve all aspects.

Thank you for your feedback.
Best regards,

Tiphaine