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

[Gabriel Scherer <gabriel.scherer@gmail.com>]

> Maybe it's my over-exposure to C++ lately, but I see a clear semantic for
> type re-declaration:
> 1) It is only allowed to re-declare types from the auto-import of a module
> signature
> 2) abstract types can be re-declared arbitrarily
> 3) private foo types can be re-declared to foo
> Nothing else can be re-declared.

Why not. We even have a syntax for explicit type overriding: "type! u = int"!
(But if you want to preserve backward-compatibility and still make the
implicit inclusion of the interface in the implementation the default,
you need to allow innocent-looking definitions to have a rebinding
semantics.)

I liked the idea of reusing the "with type ..." semantics instead of
introducing a new feature, but if this proposal can get rid of the
rather ad-hoc "module type" construct, you're trading one ad-hoc for
another ad-hoc yet potentially simpler feature. I would be happy with
such a langage feature.

Alain wrote:
> Type-checking compilation units as recursive modules addresses several
> issues at the same time:
>  - Mutual recursion between type-level components of different kinds
> (e.g. a data type declaration and a class type).
> The current solution is to introduce a local recursive module.
>
> - Avoid duplication of type declarations between the interface and the implementation
> (at least for structuraldefinitions; a type-include feature, as described in the Mantis ticket,
> would also give a solution for data types).
>
> In addition, compiling units as recursive modules (not only for type-checking) would address
> the common need of forward references and the less common need of allowing recursion between,
> say, a class definition and a function.  The current work-around is to use references to break
> the recursion, but this is quite an ugly solution (the nice thing with it, though, is that it also works
> for allowing recursion between several compilation units).

Those are all compelling arguments (in terms of "necessary language
change" to "solved problems" ratio, your proposal is probably
optimally low), but the complexity cost (in term of theory but also of
program comprehension for the unaware beginner) of module recursion
are really high. I would favor working out smaller, isolated solutions
for type duplication, forward references and mutually recursive
structure items -- but indeed that would mean more language changes,
which often means no change at all. Besides, the proposal still
requires some form of (include (module type of M)) in m.ml to avoid
type redefinitions, which is less ad-hoc than (include (module type))
but also less convenient that the implicit-and-by-default solution
that Edgar champions.

On Wed, Oct 31, 2012 at 2:50 PM, Edgar Friendly <thelema314@gmail.com> wrote:
> On 10/30/2012 5:25 PM, Gabriel Scherer wrote:
>>
>> ## Proposal
>>
>>
>> 1. allow to insert signature items anywhere in a module structure or
>> .ml file, giving a reasonable semantics to it
>>      (in particular allow inclusion of signature as a structure item,
>> with the derived semantics)
>
> This seems a quite reasonable feature for OCaml to have, as annotating the
> desired type of a declaration
>
>> 2. have a syntax to designate the mli signature from the ml file
>> (possible suggestion: "module type", used a signature expression)
>
> Eww.  This seems quite ugly, especially using the complex "with type foo =
> bar" syntax for something as common as giving the implementation of an
> abstract type.
>
>> It is also natural, in particular if you come from the world of C
>> prototypes and predeclared types, to wish to accept something like
>>    type u
>>    type u = int (* refining semantics *)
>> I think we should reject those because they have a muddier semantic
>> (you could define what the least abstract "unifier" of two definitions
>> would be, but let's net get down that road). The "S with type u = ..."
>> (in particular when S is "module type") allows to refine type in a
>> principle way without shadowing/redeclaration.
>
> Maybe it's my over-exposure to C++ lately, but I see a clear semantic for
> type re-declaration:
> 1) It is only allowed to re-declare types from the auto-import of a module
> signature
> 2) abstract types can be re-declared arbitrarily
> 3) private foo types can be re-declared to foo
> Nothing else can be re-declared.
>
> I might even go so far as to say that these re-declarations have to be at
> the top of the module definition; before any value declarations or private
> type declarations.  I see some use in forcing these to complete before
> normal compilation can proceed, to avoid the case of having to type a value
> before its concrete type is declared.
>
> module Foo = sig
>     type t
>     val x : t
> end = struct
>     let x = 5
>     type t = string
> end
>
> Rules like this should allow a module signature to have its typechecking
> effect on the associated module implementation as that module implementation
> is compiled and typechecked without needing a second pass over the inferred
> signature of the module to verify that the final result of the module is
> compatible.  Not that the second pass is a bad thing, but you're right that
> we will enable better error messages from a one-pass, local typing as
> opposed to a global structure comparison.
>
> E.