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

[Goswin von Brederlow <goswin-v-b@web.de>]

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