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

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

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