Re: [Caml-list] Clever typing for client-server communication?

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

On 2015/08/09 06:39, Markus Mottl wrote:
> 
> The object type trick is pretty neat and can actually be used with
> module types, too.  The advantage there is that whereas object types
> are "flat", module types support more structure via submodules, e.g.:
> 
>  module type Bla = sig module Foo : sig type t end end
>  type 'a t = 'foo_t constraint 'a = (module Bla with type Foo.t = 'foo_t)
> 
> Sadly, there is one significant shortcoming here: there does not seem
> to be any way to exploit subtyping with module types.  Not sure, but
> the only reason for this seems to be that values of module type (i.e.
> first-class modules) cannot be reasonably implemented with subtyping,
> because unlike objects they don't carry around a dictionary at runtime
> for looking up entries in the module.
> 
> Please correct me if I'm wrong, but from a pure typing perspective I
> think that there should be no reason to disallow support for
> expressing subtyping with module types.  The compiler is already able
> to infer whether module signatures satisfy subtyping relationships
> anyway.


The problem is that if you allow expression subtyping for module types,
then I see no way to avoid its being applied to … modules. Which we want to
avoid, since the semantics of subtyping for modules is not the same as
for expressions (i.e., modules require coercions).

By the way, you can also define deep structures with object types, so
I don’t see the advantage of using module types. For an example of
nested object structures, you can see lablgtk, with its sub-object approach
for signals.

Jacques Garrigue