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

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

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.

What you would need to do is recognize a contextual situation where
you type-check an implementation *given* a known signature context
(just as we extended type-checking expression to know about the
expected type for GADTs in 4.00), instead of type-checking it by
itself. This is essentially equivalent to the design considerations of
the (module type) feature that only makes sense in the context of a
larger signature sealing, only you're doing it implicitly.

(I think that once you realize that, you end up with something
equivalent to Edgar's proposal.)

On Wed, Oct 31, 2012 at 5:48 PM, Edgar Friendly <thelema314@gmail.com> wrote:
> I hope my solution is not only potentially simpler, but easier for people to
> use and more natural for people coming to OCaml from other languages where
> types are declared once.  It also allows us to sidestep the issue of type
> declarations and recursion, as it doesn't depend on any new syntax.

Convincing. I'll fight for having signature items usable in structures
(and forward references) another day, consider me a supporter of your
thought experiment.


On Wed, Oct 31, 2012 at 5:48 PM, Edgar Friendly <thelema314@gmail.com> wrote:
> On 10/31/2012 11:12 AM, Gabriel Scherer wrote:
>>>
>>> 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 missed one case:
> 4) any type can be re-declared as itself.
> This uses up the one "re-declaration" that an auto-imported type is allowed.
>
>> 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.)
>
> Yes, the backwards compatibility is key to my proposal; existing .ml+.mli
> files would re-declare everything, resulting in all types being as listed in
> the .ml file.
>
>> 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.
>
> I hope my solution is not only potentially simpler, but easier for people to
> use and more natural for people coming to OCaml from other languages where
> types are declared once.  It also allows us to sidestep the issue of type
> declarations and recursion, as it doesn't depend on any new syntax.
>
> E.