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

[Gerard Murphy]

Michal,

Thanks for getting back to me so promptly ... replies inline below

> -----Original Message-----
> From: devel-en-bounces at nemerle.org [mailto:devel-en-bounces at nemerle.org]
> On Behalf Of Michal Moskal
> Sent: 12 November 2005 11:58
> To: devel-en at nemerle.org
> Subject: Re: [nem-en] Clarification on type-inference rules.
> 
> On 11/11/05, Gerard Murphy <g.j.murphy at sageserpent.com> wrote:
> > Hello,
> >
> > I'm exploring Nemerle via some simple exercises, and so far I've found
> it a
> > very pleasant experience - my congratulations to the language design and
> > implementation team.
> >
> > However, I'd like to ask for some clarification on some less intuitive
> > aspects of the type inference rules.
> >
> > Before going any further, I'm aware from both the discussion at
> > http://nemerle.org/blog/archive/2005/Mar-13.html and from
> > previous use of OCAML about the loopholes in type-inference in the
> presence
> > of mutable operations.
> >
> > My questions here are however about type-inference in a more
> conventional
> > setting where the operations are purely functional.
> 
> The problem here is that even if one doesn't use impure features, the
> type system has to still
> account for them.  This is also true for other features.
> 

Yes, indeed.

*** SNIP ***

> I'll drop in some comments how to make the code shorter, if you
> already know something - just ignore it.
> 

*** SNIP ***

> Nemerle.Collections.List.Map(addElementToSequenceAtEachPosition(tailOfSequ
> ence),
> 
> Here you can also use
> addElementToSequenceAtEachPosition(tailOfSequence).Map (fun (...) { ... })
> 
> All functions taking a single list as a first parameter from
> Nemerle.Collections.List are also duplicated as member functions of
> the list variant.

I didn't know one could do that - thanks for the tip!!


> 
> Also in the code like:
> 
>   | pat1 => { def x = foo; bar (x) }
> 
> the { } are superflous (this is unlike in OCaml, where { ... } (called
> begin and end) are sometimes needed in such situations).

Again, thanks.

> > ITEM1
> >
> > If you comment-in the define for 'ITEM1', the program contains a use of
> an
> > array with an unbound type variable for the element type (at least
> that's
> > how I think about it). I would imagine that this would be a valid thing
> to
> > do - analogous to using a value '[]' in OCAML, where the constructed
> value
> > of the empty list is structurally independent of the type variable
> > representing the list item type.
> >
> > Yes, I know that this can lead to nasty surprises in OCAML if such an
> empty
> > list is accessed via a mutable path (i.e. a reference or record), but
> I'm
> > thinking of the purely functional case here.
> >
> > This doesn't compile, however: I see an error of the form:-
> >
> > "error : the types
> System.IComparable[System.IComparable[System.IComparable[System.IComparabl
> e[System.IComparable[...]]]]]
> > and
> System.IComparable[System.IComparable[System.IComparable[System.IComparabl
> e[System.IComparable[...]]]]]
> > are not compatible [simple unify]"
> >
> > This is reported at the definition of 'createAllPermutationsOf'.
> 
> OK the general problem is that the Nemerle type inference engine does
> not infer generic types.

Aha! I suspected that was the case...

> 
> 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.

> 
> 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].

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, 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?

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, even though X is only going to be bound by a client who may well be
compiled in a different assembly?

Is this connected with the on-the-fly generics run-time specialisation? 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?

Of course, if you had a subsequent mutative operation that would add an
element to a polymorphically-typed array value, 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.

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

> 
> > 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?

> 
> > ITEM2
> >
> > If you comment-in the define for 'ITEM2', the program localises use of
> an
> > explicit type variable and F-bound constraint to the nested definition
> > 'isLessThanOrEqualTo'.
> >
> > This causes the compiler to crash with a stack overflow.
> 
> OK, this is even worse. But I'm affraid this stack overflow will be
> turned into a cryptic message like the above...
> 
> > ITEM3
> >
> > Commenting-in the define for 'ITEM3' uses a variation of explicit
> typing,
> > where type annotations are used to capture an explicit type variable. I
> > would argue that unification of the argument type of 'sequence' via the
> > pattern-matching guards should succeed, deducing a type of list['a] with
> a:
> > IComparable['a].
> >
> > This doesn't compile, I see an error:-
> >
> > "error : the matched value type list.Cons[Element.231] was expected to
> be
> > compatible with list.Nil[System.Object+]: Nemerle.Core.list.Nil is not a
> > subtype of Nemerle.Core.list.Cons [simple require]"
> >
> > It seems to get stuck on the more specific type of list.Cons['a] instead
> -
> > but only in this specific case as you will see later.
> 
> 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.

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.


> 
> > ITEM4
> >
> > This doesn't use any explicit type variables to help the compiler
> understand
> > that the sequence elements are comparable - but it compiles. Given that
> > there is insufficient information in the definition of 'isSorted' to
> > ascertain the generic form of the IComparable interface for 'head' and
> for
> > 'nextOne', or even just the old-fashioned IComparable interface for
> 'head',
> > I presume that further type-unification is going on at the external call
> > sites for 'isSorted' and 'selectSortedPermutation' that brings in the
> exact
> > type of the sequence elements - namely string.
> >
> > Put another way, the type inference process can propagate information
> down
> > and back from usages as well as up and forwards from definitions. I
> guess
> > this is implicit from the description at
> > http://nemerle.org/blog/archive/2004/Sep-07.html, but it
> > caught me by surprise - I was expecting unification of a function's type
> > variables to stop locally at a definition, i.e. to be dependent purely
> on
> > the internals of the definition.
> 
> You're 100% right here! ;-) Please have a look at this article:
> 
>   http://nemerle.org/Type_inference
> 
> I also intend to extend it this week.


I look forward to reading the update!


*** SNIP ***

> > I presume that this is allowed for local definitions as there is a
> finite
> > amount of code that can use such definitions: so you can't define a
> truly
> > generic function that is local: what is allowed is to simply omit the
> > explict type signatures.
> 
> 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?


> 
> > I presume that is another reason why type inference is disallowed at a
> > method level for public methods - you would need whole-program type
> > inference to clamp down the type variables for public methods; which
> would
> > contradict separate compilation of assemblies.
> 
> Yes.
> 
> We want it for private functions, though. Probably with some
> restrictions. This will require compiling all the functions in a class
> together (that is in a single type inferencer object).

That's got my vote.

> 
> > Again, this took me surprise: I had started out expecting a local
> Nemerle
> > definition to act like a global OCAML let construct as regards type
> > inference. I'll pre-empt the obvious next question by stating that I've
> > never given type inference for local let-constructs in OCAML any thought
> > whatsoever in the past; now I'll have to go an investigate that too. :-)
> 
> The algorithm here is quite different. The W algorithm used in ML is
> really a pretty one, but it doesn't fit well with the class model of
> .NET.

I suspect this is where my ideas above are going to fall over: I think I
need to do some research into the low-level aspects of the .NET generics
model for my own benefit.

> 
> > 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. :-)

> 
> > I'm using the 0.9.1 version of ncc, against the Microsoft .NET 2
> framework -
> > (Beta 2.0.50727.42).
> >
> > In closing, I'd appreciate it if somebody could either confirm my
> thoughts
> > or put me right on the subject.
> 
> I hope this helps!

Greatly, many thanks for your help.

Regards,

Gerard


Gerard Murphy, www.sageserpent.com