Interesting behavior of "include"

Interesting behavior of "include"

[John Prevost]

I started using the "include" directive in signatures recently, then
realized that it's not actually documented anywhere (although it's
quite useful at times.)

I also discovered a little "problem" with it.

module type test =
  sig
    type t
    val a : t
  end

module type test2 =
  sig
    include test
    val b : t
  end

module type test3 =
  sig
    include test
    val c : t
  end

module type testbad =
  sig
    include test2
    include test3 with type t = t
  end

    (* This would seem to imply that the new type t is the same as the old
       when the above expands to:
       sig
         type t
         val a : t
         val b : t
         type t = t (* just "type t" without the "with" part above. *)
         val a : t
         val c : t
       end
       So that a, b, and c would all have the same type.

       If you try it without the with, you'll see that they do actually end up
       all with the same type, but no matter how hard you try to constrain the
       signature using "with", the second "type t" causes t to be abstract.

       If you use the with above to try to constrain the second type t
       in the signature to be the same as the first (you can't name
       which t you mean, since include doesn't let you refer to the
       first t as Test2.t), you get an even worse problem:

         module type testbad =
           sig type t val a : t val b : t type t = t val a : t val c : t end
         # module Testbad : testbad with type t = int = struct
	 #   type t = int
	 #   let a = 1
	 #   let b = 1
	 #   let c = 1
	 # end;;
	 module Testbad :
	   sig type t = int val a : t val b : t type t = t val a : t
	       val c : t end
         # Testbad.a;;
	 - : Testbad.t = Uncaught exception: Stack overflow

      This happens with or without the with in the module definition.

      Pretty neat, eh?  The with definition is allowing you to define a
      cyclic type abbreviation.  (This is correctly caught in all other
      places you can use with as being an unbound type constructor.  But
      in the include case, it must see that there is, in fact, a type t,
      without being able to express in the form of a signature that in
      the definition "type t = t", the second t refers to the previously
      defined t.

      This leaves two problems of course:  the first is "include ... with"
      needs to check for cyclic type abbreviations, and the second is that
      there's no way to constrain includes to be more "merging" than they
      are (so that I can define "MONAD_ZERO_PLUS" in terms of "MONAD_ZERO"
      and "MONAD_PLUS" instead of in terms of "MONAD", say.)

      Of course, I probably shouldn't be using an undocumented feature
      in the first place.
    *)

jmp

Re: Interesting behavior of "include"

[Francisco Valverde Albacete]

John Prevost wrote:

> I started using the "include" directive in signatures recently, then
> realized that it's not actually documented anywhere (although it's
> quite useful at times.)

I hope that does not mean it will be discontinued! I have been using it
extensively for developing ADT's ever since it was included in the release, some
(O)camls back...

My own rationale was that the module system could be used to incrementally develop
richer and richer structures from basic ones, perhaps specialising them for
particular purposes... Signatures figured in it supplying the basis for
(sintactic) specifications for the basic and derived types...

So far so good... then came the nasty surprises which your mail explains pretty
well:

> I also discovered a little "problem" with it.
> (stuff deleted)
>        Pretty neat, eh?  The with definition is allowing you to define a
>       cyclic type abbreviation.  (This is correctly caught in all other
>       places you can use with as being an unbound type constructor.  But
>       in the include case, it must see that there is, in fact, a type t,
>       without being able to express in the form of a signature that in
>       the definition "type t = t", the second t refers to the previously
>       defined t.
>
>       This leaves two problems of course:  the first is "include ... with"
>       needs to check for cyclic type abbreviations, and the second is that
>       there's no way to constrain includes to be more "merging" than they
>       are (so that I can define "MONAD_ZERO_PLUS" in terms of "MONAD_ZERO"
>       and "MONAD_PLUS" instead of in terms of "MONAD", say.)

Exactly! "include" is just textual inclusion - just "shorthand" for a whole
signature - not a statement of the semantic relationship between ADTs so it is not
fit to deal with many interesting cases, for example constraint merging as you
suggested! And the nasty surprise comes about because you are trying to do some
semantic work  with a syntactic resource.

But the thing is the feature is so handy that you feel *compelled* to use
"include" in your constraining of signatures both for module parameters and for
functor application result's signatures.SO... From some of the emails seen in the
list by the Ocaml implementors I get the impression that the module system is far
from well understood thus we cannot give modules "first citizen" status:

- no recursive definition of modules (though this comes as naturally as mutually
recursive objects when your way of thinking is that of modules, believe me!). This
is difficult to conceive for the time being...
- no easy extension/merging of modules (spilling 'a la SML doesn't work for OCaml
so you have to rewrite entirely too much! Would this be like multiple inheritance
for modules?)
- no easy merging of signatures (which comes handy when you want to see a
structure as two different ADT's as you were trying to do. Don't try to constraint
semantically with a purely (proto)syntactic device.!)
- no easy mixing of modules (static shared-state algebraic structures?) and
objects (dynamic local-state elements?) or types, and no mixing of parameter
passing in function, functor or initialization application .

I can tell you if you are interested some (rather crude) workarounds for some of
these limitations... They are mainly programming style and piecewise signature
composition...

BTW this is something some old textbooks on ADT's were trying to introduce some 20
years ago, but it all turned out differently: objects where somewhat hazy then and
ADT's just mathematical entities (See "Algorithmic Language and Program
Development", by Bauer and Wossner, Springer-Verlag, 1982...)

>       Of course, I probably shouldn't be using an undocumented feature
>       in the first place.

But experimenting if a good part of the fun, isn't it? ;)

Hope this helps,

        Fran Valverde
------------------------------------------------------------------------------------------

Resum'e (en Francais epouvantable, je regret):

Il ne faut pas se tromper en considerant "include" une construction (s'emantique)
du langage plutot que de la sucre syntactique. Ca ne marche pas tres bien
d'essayer d'imposer des comportements semantiques en utilisant cette construction,
puisque le systeme des modules n'est pas assez bien compris pour supporter telle
manipulation  et que les modules ne sont vraiement pas des citoyens de premiere
classe... Il y a des certains trucs dont on peut s'en servir en ce qui concerne le
style de programmation qui permettent de manipuler les modules et ses signatures
pour en faire.

        F. Valverde