[nem-en] Clarification on type-inference rules #2

[Michal Moskal]

On 11/13/05, Gerard Murphy <g.j.murphy at sageserpent.com> wrote:
> Michal, Kamil
>
> I thought I'd start a new thread on this, as it's getting quite hard to read
> through all the levels of replies.
>
> I've read all of your messages so far: I get the impression that I have
> persuaded you two to consider implementing support for non-directed,
> inferred polymorphic types in local definitions, specifically for the '[]'
> and 'array[]' expressions.
>
> After some reflection, I'm having second thoughts on this - I think my
> orginal advice was seriously wrong.
>
> I confess that my first impulse on this was to look at OCAML, where [] is
> completely polymorphic and of type list 'a. Even if I write code like...
>
> let troublesome = ref [];;
>
> troublesome <- [ "Gotcha" ];;
>
> ... in an interactive session with the OCAML interpreter, it will reunify
> the type of 'troublesome' from ref list 'a to ref list string. This is valid
> because the original value of [] is simply forgotten, so it remains validly
> typed as list 'a.

This is not exactly how it works in OCaml. When you write let x = ref
[], you get x : '_a list ref, note the '_'. This means that the value
is not polymorphic, it just doesn't have a type yet. This is also how
it should work in our interative interpreter, but unfortunately it
doesn't support passing type variables between expressions yet.
However in the regular code you can always do:

  mutable l = [];
  l = [ "gotacha" ];

with essentially the same effects.

Still [] has a proper (forall 'a. 'a list) polymorphic type in OCaml.
In Nemerle [] is a shortcut for "list.Nil ()", where list.Nil has type
(forall 'a. void -> list['a]), so the application results here in a
free, unquantified type variable, that is going to be unified later.

[snip]
> A naïve implementation would emit these interfaces for each site in the code
> where [] or array[] is seen.

You cannot do that in each and every place where [] is used, because
you wouldn't be able to do 1 :: [] and the like. This is only needed
later in code generation, where the proper type of [] cannot be found.

The problem is that we would need to analyse types to find such cases.
Such occurchecks are possibly expensive, though I guess they are
unavoidable anyway (we now use stack-height restriction).

> Note that I'm still thinking here along the lines that [] is independent of
> any particular substitution of 'a in list 'a, just as it is in OCAML - I
> know that's not how it works in Nermele at the moment; each [] belongs to
> some specific substitution: list <something> . I'm assuming for the sake of
> argument that you might change that behaviour.

We cannot change this physically. The tail of the list['a] needs to
have type list['a] which is impossible for any single Nil type to
fullfil, so we need Nil['a].

[snip]
> If I was doing this in C++, Java 2 or C# or Ada or Eiffel or whatever, I
> would have accepted that polymorphic types are directed and would have
> supplied some arbitrary type to substitute for the free type variable...
>
> array[]: int, or array[]: string, or array[]: IBogus
>
> This is bit nasty when I think of the dizzying heights of OCAML, but I do
> this every day in C++ without batting an eyelid:-
>
> new std::vector<StubTypeForTesting>()

We wanted to avoid this kind of stuff. But here we have a choice of
requiring the user to supply the type, or giving the function some
unexpected compiler generated type. As the later can be source of bugs
and the former cannot, I would go with the former.

> So my point is to have the compiler reject any use of [] or array[] that
> leaves the expression type is being polymorphic, unless it occurs in a
> directed context, i.e. where the type variables are supplied by an enclosing
> generic construct. I'm quite happy to accept this as a necessary evil.

So I guess we agree here :-)

> BTW: doesn't anybody else have any thoughts on this? Again, are there any
> readers from the F# or SML.NET communities?

I believe they do not support F-bounded polymorphism, which makes type
cyclic here. But possibly they also use some different strategies of
compilation.

[snip]
> I am assuming here that the type inference mechanism won't do an exact
> unification of System.Object with the polymorphic type list 'a: rather it
> will recognize that System.Object is a superclass of list 'a and use the
> latter as the most general unifier, allowing an upcast in the generated
> code.

Yes it will.

>
> Similarly, I assume that System.Array unifies with array 'a to make array
> 'a: again, an upcast would take place in the generated code.

Again, right :-)

What we need to do here anyway, is to detect this unfortunate
IComparable case and signal a better error message...

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