Re: [Caml-list] Why should I use .mli files?

[Tiphaine Turpin <Tiphaine.Turpin@free.fr>]

On 10/31/12 18:15, Gabriel Scherer wrote:
> On Wed, Oct 31, 2012 at 6:32 PM, Tiphaine Turpin
> <Tiphaine.Turpin@free.fr> wrote:
>> Here is another proposal on this type topic : why not change the
>> semantics of module type inclusion to consider missing types (and module
>> types as well) as if they were declared with the same definition ? In
>> other words, a signature S would be a subtype of S' if there exists some
>> set of type declarations which, if prepended to S, make it have the type
>> S' in the usual sense ? Exactly as [> `a ] is a subtype of [> `a | `b ]
>> for polymorphic variants.
> The problem with this idea is that you cannot ask yourself if "the
> signature S (coming from the .mli) is a subtype of the signature S'
> (coming from the .ml)" if the .ml, or the module definition, cannot be
> type-checked without information coming from S. (S') doesn't exist
> here, as the implementation cannot be type-checked by itself.
I realize that I overlooked a detail in my suggestion: fields and
constructors names must be declared before they are used in expressions
and patterns... The idea works well for polymorphic variant types and
objects, with their structural typing. Here is an example:

a.ml:
    let f = function `a | `b -> ()

a.mli:
    type t = [`a | `b]
    val f : t -> unit

You can infer the signature

"sig val f : [< `a | `b ] -> unit end"

for a.ml, and then check that it is a subtype (in the non-conventional
sense) of a.mli

This doesn't mean that it is impossible to adapt this for record and
variant types (at the cost of implicit field and constructor
declaration), but you are right, a "contextual" typing seems more
natural. However, this doesn't fit well with the module system of OCaml,
where a module type can be declared a subtype of several others, and
this subtyping can happen anytime "after" the definition of the first
module type. So this could only be an ad hoc trick for toplevel modules,
which is seems much less appealing to me (maybe its my under-exposure to
C++).

Tiphaine