[Caml-list] Expansion of type-constructors in ctype.ml

[Caml-list] Expansion of type-constructors in ctype.ml

[Christoph Höger]

Dear all,

as a followup to [1], I figured out what causes both the massive
unnecessary work and the huge output files.

The fundamental problem is as follows:

In case you have a type constructor in your implementation, say

val x : 'a -> 'a foo

the compiler will, among other things, try to match the implementation
with its (inferred) interface. During this process, the routines eqtype,
morgen and unify2 in ctype.ml are used.

In all of these routines, however, the first step is to do an
expand_head, which will replace the Tconstr with whatever is on its
right-hand-side.

If you happen to have a large rhs (as I do from a compiler), this
process kills the compiler performance. I will try to write a script
that autogenerates an example to demonstrate the issue later, but
consider the form of:

class ['a] c_n (a : 'a) = object
  method m = (new c_<n-1>) a
  method n = (new c_<n-1>) a
end

for an arbitrary n.
Instead of checking e.g. the equality of a c_n with b c_n, by comparing
a and b first, c_n is unfolded to an object. Then that object's fields
are compared (and instead of comparing a c_<n-1> with b c_<n-1> ... you
get the idea).

So I intend to patch the compiler to try to avoid these expansions, when
possible. But to do that, I need some more information:

1. In the case of equality, it seems fairly simple. Iff the path of two
constructors is the same and both argument lists are equal, the types
are equal, right?

2. In the case of unification, if both paths are the same, the argument
lists are of the same length, we can directly unify the arguments, right?

3. In the case of moregen, I am a little bit lost. Trying to just move
up the Tconstr {..} case before the expansion made bootstrapping fail
with inconsistent assumptions in the hashtbl module. So it seems
something relies on the expansion's side-effect. Does anyone know why?

Maybe in all these cases above, I'll have to do expansion in case the
result is negative (non-equal, unification not possible etc.), would
that be acceptable?

And besides all this: Is there some clever trick that would let me avoid
compiler patching at all? (Note that there is currently no way to
autogenerate interfaces, I only have the implementations).

regards,

Christoph

[1]: https://sympa.inria.fr/sympa/arc/caml-list/2015-08/msg00132.html
-- 
Christoph Höger

Technische Universität Berlin
Fakultät IV - Elektrotechnik und Informatik
Übersetzerbau und Programmiersprachen

Sekr. TEL12-2, Ernst-Reuter-Platz 7, 10587 Berlin

Tel.: +49 (30) 314-24890
E-Mail: christoph.hoeger@tu-berlin.de

Re: [Caml-list] Expansion of type-constructors in ctype.ml

[Jeremy Yallop]

On 22 August 2015 at 08:42, Christoph Höger
<christoph.hoeger@tu-berlin.de> wrote:
> 1. In the case of equality, it seems fairly simple. Iff the path of two
> constructors is the same and both argument lists are equal, the types
> are equal, right?

"If", but not "iff", unless you expand first.  Consider

   type 'a t = unit

Then 'int t' and 'float t' should be considered equal, since they both
expand to 'unit', even though the argument lists are unequal

> 2. In the case of unification, if both paths are the same, the argument
> lists are of the same length, we can directly unify the arguments, right?

Again, you need to expand the path first.  Consider the following
function, using the same definition of 't' as above:

   fun (a : 'a) (b : 'b) ->
      let c : 'a t = ()
      and d : 'b t = () in
      ignore [c; d];

The last line involves unifying the types 'a t and 'b t.  Unifying the
type arguments 'a and 'b results in the following type for the
function:

    'a -> 'a -> unit

Expanding 't' before unifying means that 'a and 'b are not unified,
and the function can be given the more general type:

    'a -> 'b -> unit

Re: [Caml-list] Expansion of type-constructors in ctype.ml

[Christoph Höger]

Right, that is a good point. That means unification _is_ a special
issue. How about moregen?

However, I wonder what the true special case is, here: Does this only
apply to type-constructors where some argument is left unused? So if I
would apply my optimization only to constructors where all arguments
appear on the right-hand side (how would I check that?) would that help?

I am facing a real issue here, because my thesis depends on the
compilation of 12k such classes into OCaml, and I need to demonstrate
its practical feasibility. So patching the compiler is not a big issue
(since I find it quite readable). However, I would prefer to upstream
these changes, of course and this would require some mentoring (API,
code style etc.)

Am 22.08.2015 um 11:23 schrieb Jeremy Yallop:
> On 22 August 2015 at 08:42, Christoph Höger
> <christoph.hoeger@tu-berlin.de> wrote:
>> 1. In the case of equality, it seems fairly simple. Iff the path of two
>> constructors is the same and both argument lists are equal, the types
>> are equal, right?
> 
> "If", but not "iff", unless you expand first.  Consider
> 
>    type 'a t = unit
> 
> Then 'int t' and 'float t' should be considered equal, since they both
> expand to 'unit', even though the argument lists are unequal
> 
>> 2. In the case of unification, if both paths are the same, the argument
>> lists are of the same length, we can directly unify the arguments, right?
> 
> Again, you need to expand the path first.  Consider the following
> function, using the same definition of 't' as above:
> 
>    fun (a : 'a) (b : 'b) ->
>       let c : 'a t = ()
>       and d : 'b t = () in
>       ignore [c; d];
> 
> The last line involves unifying the types 'a t and 'b t.  Unifying the
> type arguments 'a and 'b results in the following type for the
> function:
> 
>     'a -> 'a -> unit
> 
> Expanding 't' before unifying means that 'a and 'b are not unified,
> and the function can be given the more general type:
> 
>     'a -> 'b -> unit
> 


-- 
Christoph Höger

Technische Universität Berlin
Fakultät IV - Elektrotechnik und Informatik
Übersetzerbau und Programmiersprachen

Sekr. TEL12-2, Ernst-Reuter-Platz 7, 10587 Berlin

Tel.: +49 (30) 314-24890
E-Mail: christoph.hoeger@tu-berlin.de

Re: [Caml-list] Expansion of type-constructors in ctype.ml

[Jacques Garrigue]

On 2015/08/22 20:41, Christoph Höger wrote:
> 
> Right, that is a good point. That means unification _is_ a special
> issue. How about moregen?
> 
> However, I wonder what the true special case is, here: Does this only
> apply to type-constructors where some argument is left unused? So if I
> would apply my optimization only to constructors where all arguments
> appear on the right-hand side (how would I check that?) would that help?

This is indeed a pretty difficult problem, as you must be careful of not
changing the semantics of unification.
Until recently, the only solution was to expand the type, as there was
no static information cacheing whether an argument was used in the
body or not.
However, since relatively recent changes about variance information
(the switch to 7 flags…), we actually have at least an approximation
of which unifications must be done imperatively, and which needn’t
be done at all.
So it might be doable at least for part of the parameters.

Note that this is tricky, and forgetting some needed unification is of course
unsound.
Also, expansion is used in many places, so that avoiding it completely
would be very hard. In theory, we only expand to a graph, so the problem
is only if your mutual recursion between classes has very long cycles.
You might consider turning some of the types into concrete datatypes,
to cut the cycles.

> I am facing a real issue here, because my thesis depends on the
> compilation of 12k such classes into OCaml, and I need to demonstrate
> its practical feasibility. So patching the compiler is not a big issue
> (since I find it quite readable). However, I would prefer to upstream
> these changes, of course and this would require some mentoring (API,
> code style etc.)

I would have to see the code to tell you more.
As stated above, the real problem is the length of the cycles in the expanded
graph.

Jacques Garrigue

> 
> Am 22.08.2015 um 11:23 schrieb Jeremy Yallop:
>> On 22 August 2015 at 08:42, Christoph Höger
>> <christoph.hoeger@tu-berlin.de> wrote:
>>> 1. In the case of equality, it seems fairly simple. Iff the path of two
>>> constructors is the same and both argument lists are equal, the types
>>> are equal, right?
>> 
>> "If", but not "iff", unless you expand first.  Consider
>> 
>>   type 'a t = unit
>> 
>> Then 'int t' and 'float t' should be considered equal, since they both
>> expand to 'unit', even though the argument lists are unequal
>> 
>>> 2. In the case of unification, if both paths are the same, the argument
>>> lists are of the same length, we can directly unify the arguments, right?
>> 
>> Again, you need to expand the path first.  Consider the following
>> function, using the same definition of 't' as above:
>> 
>>   fun (a : 'a) (b : 'b) ->
>>      let c : 'a t = ()
>>      and d : 'b t = () in
>>      ignore [c; d];
>> 
>> The last line involves unifying the types 'a t and 'b t.  Unifying the
>> type arguments 'a and 'b results in the following type for the
>> function:
>> 
>>    'a -> 'a -> unit
>> 
>> Expanding 't' before unifying means that 'a and 'b are not unified,
>> and the function can be given the more general type:
>> 
>>    'a -> 'b -> unit

Re: [Caml-list] Expansion of type-constructors in ctype.ml

[Christoph Höger]

[-- Attachment #1: Type: text/plain, Size: 1423 bytes --]

Am 24.08.2015 um 00:18 schrieb Jacques Garrigue:
> This is indeed a pretty difficult problem, as you must be careful of not
> changing the semantics of unification.
> Until recently, the only solution was to expand the type, as there was
> no static information cacheing whether an argument was used in the
> body or not.
> However, since relatively recent changes about variance information
> (the switch to 7 flags…), we actually have at least an approximation
> of which unifications must be done imperatively, and which needn’t
> be done at all.
> So it might be doable at least for part of the parameters.

That sounds interesting. What are the relevant variance flags?

> I would have to see the code to tell you more.
> As stated above, the real problem is the length of the cycles in the expanded
> graph.

I really do not think that this is related to any cycles. It is just
about large unfolded types. I attached a script to generate a meaningful
example. When I try to run ocamlbuild m_9.cmo, it takes ~30s already. A
preliminary patched version of the ocaml compiler can handle this
particular example in pretty much no time at all.

regards,

Christoph

-- 
Christoph Höger

Technische Universität Berlin
Fakultät IV - Elektrotechnik und Informatik
Übersetzerbau und Programmiersprachen

Sekr. TEL12-2, Ernst-Reuter-Platz 7, 10587 Berlin

Tel.: +49 (30) 314-24890
E-Mail: christoph.hoeger@tu-berlin.de

[-- Attachment #2: create.zsh --]
[-- Type: text/plain, Size: 462 bytes --]

#!/usr/bin/env zsh

for ((i = 1 ; i < 10 ; i++)) ; do
  echo "class ['a] c (a : 'a) = object" > m_$i.ml
  echo "  method m_1 = (new M_$((i-1)).c) a#foo" >> m_$i.ml
  echo "  method m_2 = (new M_$((i-1)).c) a#foo" >> m_$i.ml
  echo "  method m_3 = (new M_$((i-1)).c) a#foo" >> m_$i.ml
  echo "  method m_4 = (new M_$((i-1)).c) a#foo" >> m_$i.ml
  echo "end" >> m_$i.ml
done

echo "class ['a] c (a : 'a) = object method m_1 = a#foo method m_2 = a#foo end" > m_0.ml

Re: [Caml-list] Expansion of type-constructors in ctype.ml

[Christoph Höger]

[-- Attachment #1: Type: text/plain, Size: 630 bytes --]

find attached a patch against the 4.02.3 tree that solves my issue with
compiling the problematic examples.

I am pretty confident that the change to eqtype is sound, I do not know
exactly what moregen() is intended to do, though and it seems that its
side-effects are required (that is why I expand the types there in any
case).

I appreciate any further comments,

Christoph

-- 
Christoph Höger

Technische Universität Berlin
Fakultät IV - Elektrotechnik und Informatik
Übersetzerbau und Programmiersprachen

Sekr. TEL12-2, Ernst-Reuter-Platz 7, 10587 Berlin

Tel.: +49 (30) 314-24890
E-Mail: christoph.hoeger@tu-berlin.de

[-- Attachment #2: large_classes.patch --]
[-- Type: text/x-patch, Size: 2117 bytes --]

diff --git a/typing/ctype.ml b/typing/ctype.ml
index d1ff9da..2125d00 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -2948,6 +2948,21 @@ let rec moregen inst_nongen type_pairs env t1 t2 =
         link_type t1 t2
     | (Tconstr (p1, [], _), Tconstr (p2, [], _)) when Path.same p1 p2 ->
         ()
+    | (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _))
+         when Path.same p1 p2 ->
+       begin try
+           moregen_list inst_nongen type_pairs env tl1 tl2 ;
+           (* expand afterwards, this seems to be an expected side-effect *)
+           ignore (expand_head env t1 ) ;
+           ignore (expand_head env t2 ) ;
+         with e ->
+           let t1' = expand_head env t1 in
+           let t2' = expand_head env t2 in
+           let t1' = repr t1' and t2' = repr t2' in
+           (* prevent non-termination (is this really necessary?) *)
+           if t1' == t1 && t2' == t2 then raise e else
+             moregen inst_nongen type_pairs env t1 t2
+       end
     | _ ->
         let t1' = expand_head env t1 in
         let t2' = expand_head env t2 in
@@ -3213,6 +3228,23 @@ let rec eqtype rename type_pairs subst env t1 t2 =
         end
     | (Tconstr (p1, [], _), Tconstr (p2, [], _)) when Path.same p1 p2 ->
         ()
+
+    | (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _))
+         when Path.same p1 p2 ->
+       (* Optimize equality of large type-constructors.
+          Equality of all arguments implies equality of the result, expand 
+          only in case of non-equality (since equivalence does not hold) *)          
+       begin try
+         eqtype_list rename type_pairs subst env tl1 tl2
+       with e -> 
+           let t1' = expand_head_rigid env t1 in
+           let t2' = expand_head_rigid env t2 in
+           let t1' = repr t1' and t2' = repr t2' in
+           (* prevent non-termination (is this really necessary?) *)
+           if t1' == t1 && t2' == t2 then raise e else
+             eqtype rename type_pairs subst env t1' t2'
+       end
+
     | _ ->
         let t1' = expand_head_rigid env t1 in
         let t2' = expand_head_rigid env t2 in

Re: [Caml-list] Expansion of type-constructors in ctype.ml

[Jacques Garrigue]

On 2015/08/24 19:15, Christoph Höger wrote:
> 
> find attached a patch against the 4.02.3 tree that solves my issue with
> compiling the problematic examples.
> 
> I am pretty confident that the change to eqtype is sound, I do not know
> exactly what moregen() is intended to do, though and it seems that its
> side-effects are required (that is why I expand the types there in any
> case).
> 
> I appreciate any further comments,
> 
> Christoph

Do you mean that modifying moregen and eqtype (but not unify)
in a conservative way would be enough to solve your problem?
Then indeed we could do that.
At least your code for eqtype seems fine. For moregen, this is not sufficient, due to non-local side effects.
By the way, we should keep your example around to prevent regressions.

On 2015/08/24 15:22, Christoph Höger wrote:
> Am 24.08.2015 um 00:18 schrieb Jacques Garrigue:
>> This is indeed a pretty difficult problem, as you must be careful of not
>> changing the semantics of unification.
>> Until recently, the only solution was to expand the type, as there was
>> no static information cacheing whether an argument was used in the
>> body or not.
>> However, since relatively recent changes about variance information
>> (the switch to 7 flags…), we actually have at least an approximation
>> of which unifications must be done imperatively, and which needn’t
>> be done at all.
>> So it might be doable at least for part of the parameters.
> 
> That sounds interesting. What are the relevant variance flags?
> 
You should read the following paper:
http://www.math.nagoya-u.ac.jp/~garrigue/papers/injectivity.pdf

If all the flags were always correct then it would be simple: any flag being
set would mean that the variable really appears in the type, so you must
recurse on it (at least for eqtype and moregen).
However, variance inference for the result of functors is not exact,
meaning that to be sure that a variable will not disappear, you must check
that inj is set (meaning that there is a concrete occurence).
In a nutshell:
may_pos and may_neg are both unset (i.e. nothing is set) => no need to recurse
inj is set => must recurse
otherwise => must expand

 Jacques Garrigue

Re: [Caml-list] Expansion of type-constructors in ctype.ml

[Christoph Höger]

Am 25.08.2015 um 16:02 schrieb Jacques Garrigue:
> Do you mean that modifying moregen and eqtype (but not unify)
> in a conservative way would be enough to solve your problem?

At least until now, it seems to solve it. I can compile my ~12k classes
in ~20min now. I expect the number of classes to decrease while I
optimize the output of my compiler and their size to increase while I
add more features. So the best bet is that the performance will stay the
same, unless I encounter some more performance problems.

Btw: Is there a place/format to discuss concrete proposed patches? This
list seems to be more on the user's side.

> Then indeed we could do that.
> At least your code for eqtype seems fine. For moregen, this is not sufficient, due to non-local side effects.
> By the way, we should keep your example around to prevent regressions.

Feel free to add the example wherever you want. I can also open a bug in
mantis if you think that is appropriate. Do you have any insights on
what could be done for moregen?

> You should read the following paper:
> http://www.math.nagoya-u.ac.jp/~garrigue/papers/injectivity.pdf

Thanks. Will do.

> may_pos and may_neg are both unset (i.e. nothing is set) => no need to recurse
> inj is set => must recurse
> otherwise => must expand

Sounds like inj is what I want for my concrete case. I recon there is no
flag yet to manually set it. Do you know of a trick to force the
inference mechanism to do so?

And by "no need to recurse" you mean that this argument could be left
out (i.e. replaced by unit)?



-- 
Christoph Höger

Technische Universität Berlin
Fakultät IV - Elektrotechnik und Informatik
Übersetzerbau und Programmiersprachen

Sekr. TEL12-2, Ernst-Reuter-Platz 7, 10587 Berlin

Tel.: +49 (30) 314-24890
E-Mail: christoph.hoeger@tu-berlin.de

Re: [Caml-list] Expansion of type-constructors in ctype.ml

[Jacques Garrigue]

On 2015/08/26 00:47, Christoph Höger wrote:
> 
> Am 25.08.2015 um 16:02 schrieb Jacques Garrigue:
>> Do you mean that modifying moregen and eqtype (but not unify)
>> in a conservative way would be enough to solve your problem?
> 
> At least until now, it seems to solve it. I can compile my ~12k classes
> in ~20min now. I expect the number of classes to decrease while I
> optimize the output of my compiler and their size to increase while I
> add more features. So the best bet is that the performance will stay the
> same, unless I encounter some more performance problems.
> 
> Btw: Is there a place/format to discuss concrete proposed patches? This
> list seems to be more on the user's side.

The standard place would be a problem report on Mantis.
Performance problems are perfectly valid.
However, I think this stills falls in the scope of this list too, as the problem is wide enough.
But opening a PR on Mantis is useful for future reference.

>> Then indeed we could do that.
>> At least your code for eqtype seems fine. For moregen, this is not sufficient, due to non-local side effects.
>> By the way, we should keep your example around to prevent regressions.
> 
> Feel free to add the example wherever you want. I can also open a bug in
> mantis if you think that is appropriate. Do you have any insights on
> what could be done for moregen?

The only safe way I see is to use the variance information.
I’ll look into that when I have some time.

>> You should read the following paper:
>> http://www.math.nagoya-u.ac.jp/~garrigue/papers/injectivity.pdf
> 
> Thanks. Will do.
> 
>> may_pos and may_neg are both unset (i.e. nothing is set) => no need to recurse
>> inj is set => must recurse
>> otherwise => must expand
> 
> Sounds like inj is what I want for my concrete case. I recon there is no
> flag yet to manually set it. Do you know of a trick to force the
> inference mechanism to do so?

You don’t have to set it. It’s inferred automatically for all type definitions.
When you look up a type with Env.find_type, you get the variance as a field of the result.
The you can check whether Inj is set by [Variance.(mem Inj v)].
You can check if there is no occurence with [v = Variance.null].

> And by "no need to recurse" you mean that this argument could be left
> out (i.e. replaced by unit)?

Yes. No need to compare, since it would never be visited after expansion.

Jacques Garrigue

Re: [Caml-list] Expansion of type-constructors in ctype.ml

[Goswin von Brederlow]

On Sat, Aug 22, 2015 at 10:23:04AM +0100, Jeremy Yallop wrote:
> On 22 August 2015 at 08:42, Christoph Höger
> <christoph.hoeger@tu-berlin.de> wrote:
> > 1. In the case of equality, it seems fairly simple. Iff the path of two
> > constructors is the same and both argument lists are equal, the types
> > are equal, right?
> 
> "If", but not "iff", unless you expand first.  Consider
> 
>    type 'a t = unit
> 
> Then 'int t' and 'float t' should be considered equal, since they both
> expand to 'unit', even though the argument lists are unequal
> 
> > 2. In the case of unification, if both paths are the same, the argument
> > lists are of the same length, we can directly unify the arguments, right?
> 
> Again, you need to expand the path first.  Consider the following
> function, using the same definition of 't' as above:
> 
>    fun (a : 'a) (b : 'b) ->
>       let c : 'a t = ()
>       and d : 'b t = () in
>       ignore [c; d];
> 
> The last line involves unifying the types 'a t and 'b t.  Unifying the
> type arguments 'a and 'b results in the following type for the
> function:
> 
>     'a -> 'a -> unit
> 
> Expanding 't' before unifying means that 'a and 'b are not unified,
> and the function can be given the more general type:
> 
>     'a -> 'b -> unit

In both cases wouldn't it make sense (and be semantically equivalent)
to first check for equality and only expand when not equal? I mean f
you already have 'a t and 'a t then it doesn't matter if t uses the 'a
or not. There is no need to expand it.

MfG
	Goswin