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

[Michal Moskal]

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.

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

> Here's the source I've been working with:-
[snip]
>         def someSortableThings =
> Nemerle.Collections.List.FromArray(array["Ooble",
> "Booble"]);

using Nemerle.Collections;

at the beginning and later List.FromArray (...) would shorten things.

> Nemerle.Collections.List.Map(addElementToSequenceAtEachPosition(tailOfSequence),

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.

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

> OK, this is a form of BogoSort – you may or may not enjoy my coding style.
> :-)

:-)

> 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.IComparable[System.IComparable[...]]]]]
> and
System.IComparable[System.IComparable[System.IComparable[System.IComparable[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.

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.

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.

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

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

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

> ITEM5
>
> This provides two usages of 'createPermutationsOf', each one using a list
> with a different substituted type variable. This fails to compile with an
> error:-
>
> "error : in argument #1 (things), needed a list[string]-, got list[int-]:
> System.Int32 is not a subtype of System.String [simple require]"
>
> Again, this seems to be the same phenomenon as discussed above for ITEM: the
> usages of the function 'createPermutationsOf' are causing further
> unification of that function's type variables, so the first call binds the
> argument type to list[string].

You're right again.

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

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

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

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

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

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