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

["Christoph Höger" <christoph.hoeger@tu-berlin.de>]

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