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

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

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