[nem-en] Clarification on type-inference rules.

[Michal Moskal]

On 11/12/05, Gerard Murphy <g.j.murphy at sageserpent.com> wrote:
> > We had to choose between: fun (x) { x.Foo } (as oposed to fun (x :
> > SomeType) { x.Foo }) working and generic type inference. In case of a
> > language like Nemerle the choice was clear: the argument is that
> > generic local functions are much less useful, than the ability to use
> > member access without explicit type annotations.
>
> Yes, now that I've got over my surprise about this, I can see it is a much
> more useful thing to do in practice.

I'm glad to hear that :)

> > Now back to the program, when you use the empty list, the type of
> > elements stored in it is unknown, let's call it 'b. It unifies fine
> > with 'a where 'a : IComparable ['a], which results in 'b = IComparable
> > ['b]. This types is propagated to createAllPermutationsOf. So it tries
> > to assing type list ['b] where 'b = IComparable[b'] to things. Such a
> > type cannot be constructed, because it is cyclic (recall that it
> > cannot assign any polymorphic type to things), so there goes an error.
>
> OK, I take your point: I presume that local definitions must have all their
> type variables fully bound when their enclosing scope is fully compiled, so
> even if the expression 'array[]' can be legitimately interpreted as having
> type array['x] (by analogy with '[]' having type list['x]), presumably
> typing the result of the call to List.FromArray(array[]) as being list['x],
> then subsequent unification at the call sites of 'createPermutationsOf()'
> and 'selectSortedPermutation()' can only refine 'x to being 'x:
> IComparable['x].

Well, mostly.

The problem is that the call places a lower bound IComparable['x] on
'x. Next, no additional upperbound is placed on 'x, so the compiler
tries to use the lower bound as the actual type to be placed in the
generated assembly, which causes cyclic type.

Note that if the traditional IComparable was used, there would be no
problem, because 'x would got unified with IComparable.

So we run into a bit strange case, where we have a complete
description of the type, but we cannot find any instance of it to be
used.

> So the original array type *would be* successfully refined to array['x]
> where 'x: IComparable['x] - still a polymorphic type and so therefore
> forbidden.
>
>
> One moment, though - I accept that if you forbid polymorphic types for local
> definitions,

This is not exactly ,,forbidden''. We just infer some INSTANCE of a
possible polymorphic type. And the problem is that without user help,
here we cannot deduce a proper instance.

Generic local functions are allowed when you specify the type explicitly.

Sorry for any confusion.

> then all of this can't be allowed - but why not go with
> compilation of the definitions with polymorphic types? Isn't this what your
> average C# compiler that supports generics does?

C# compiler does not infer types.

> If I write some C# code with an F-bound like this...
>
> class Foo<X> where X: IComparable<X>
> {
>   // etc...
> }
>
> ... then doesn't the C# compiler emit a single piece of IL for this generic
> type,

Yes it does a single IL class for this.

> even though X is only going to be bound by a client who may well be
> compiled in a different assembly?

Yes.

> Is this connected with the on-the-fly generics run-time specialisation?

No, this is a restriction of the type inference algorithm.

> I
> could understand that for C# programs, the client code will supply exact
> bindings for the free type variables at link-time, so run-time
> specialisation can take place at call sites in client code or somewhere,
> whereas in this example there will never be an exact type to substitute in.
> If this is the case, couldn't you simply put in an internal placeholder type
> for a local polymorphic type when compilation of the enclosing scope is
> complete?

Yes, this would be possible, though I would call it a hack :-)

This can also lead to strange results, consider:

def sort['a] (l : list['a]) : where 'a : IComparable['a] {
  System.Console.WriteLine (typeof ('a));
}

sort ([]);

You would like, that we would generate something like this:

sort['a] (l : list['a]) : where 'a : IComparable['a] {
  System.Console.WriteLine (typeof ('a));
}

class __tmp_hack : IComparable[__tmp_hack] {
  public CompareTo (x : __tmp_hack) : int { 0 }
}

sort (new List.Nil[__tmp_hacl] ());

so the code would print __tmp_hack, which probably isn't what was
expected (I don't know what would the user expect here though).

Note that without the constraint we would use List[object] type, which
can also be argued to be not expected...

This isn't exactly the case you described, but the instantiation
problem is the same.

> Of course, if you had a subsequent mutative operation that would add an
> element to a polymorphically-typed array value,

This cannot be done, as arrays have fixed size. There is no problem
with array here, I guess you would have the same results with []
instead of List.FromArray (array []).

You could also use List.FromArray (array (10)), which can be changed
(the problem would be again the same though).

> I presume that the process
> of type unification would pick up the type of the element and therefore bind
> the type variable of the array type: so you would only need to use a
> placeholder for the one specific case where the array type still contains an
> unbound type variable in purely functional code.

It is hard to detect purely functional code in Nemerle. There is even
a bugreport for [Pure] attributes, but we haven't gotten to it yet.

And it can also lead to surprises in functional code, due to
reflection and related stuff.

> I have a feeling that I've missed something terribly obvious here - feel
> free to refer me elsewhere if this is getting painful. :-)

No problem! :-)

> > > Even if I accepted that the use of a partially-typed array literal is
> > > illegal (and I would like to see that allowed), I would dispute that the
> > > above error message is a correct diagnosis of the problem.
> >
> > But you're of course right here. We should investigate what can be
> > done about it. Anyway the rule of thumb is that if you want a
> > polymorphic local function, type it explicitly.
>
> I wonder if you could adopt a similar solution to what I think you do for
> lists - use a special subclass for the polymorphically-typed empty array
> values by analogy with 'list.Nil'. I know that lists are algebraic data
> types with variants, and arrays are not, but perhaps there's a way out in
> that direction?

I don't quite get it.

> > This is strange. Seems like a bug.
>
> I was tempted to just report this via the bug-tracker, but I didn't want to
> fill it up with my misunderstandings of how the language should work. If you
> don't mind, if I do spot any further issues, I will carry on reporting them
> to this list, at least until I'm a bit more confident about what should and
> shouldn't work.

I reported it as: http://nemerle.org/bugs/view.php?id=569

> On the other hand, I'm happy to fill out bug reports if you don't want to
> have the mailing list clogged up with these long E-mails.

This topic is much better for mailing list discussion I guess.

> > You can, you just need the full explicit type signatures.
>
> OK, but again - why can't the type inference mechanism infer a polymorphic
> type for a definition (after it has examined all usages in the enclosing
> scope). If you can compile a generic function with explicit type signatures,
> why not an implicitly generic function?

If the function remains generic after all scopes where it can be
accessed are closed, there is no point to make it generic, because
noone will ever use it (except for this instantiation problem, which
occurs only in some corner cases).

OTOH it is quite hard, if at all possible, to detect when a type
variable won't be restricted anymore and therefore can be generalized
(of course to detect it before we close all the scopes). This is for
example becasue macros can add their custom actions to typing to be
done at some later time.

> > > Going back to what I mentioned in ITEM3, the code that is compiled by
> > > default does use an explicit type variable and constraint on a function
> > > argument, in the same spirit as ITEM but at a higher level in
> > 'isSorted'.
> > > This does compile correctly which makes the behaviour for ITEM3 seem
> > more
> > > mysterious.
> >
> > This is why I think this is a bug :-)
>
> You mean the ITEM3 behaviour, I presume? I quite like the fact that the
> compiler accepts what I've described just above. :-)

Of course :-)

--
   Michal Moskal,
   http://nemerle.org/~malekith/