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

[Gerard Murphy]

Michal,

> -----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 17:00
> To: devel-en at nemerle.org
> Subject: Re: [nem-en] Clarification on type-inference rules.
> 
> On 11/12/05, Gerard Murphy <g.j.murphy at sageserpent.com> wrote:

*** SNIP ***

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


Ah yes, I see now: I keep thinking of 'x: IComparable['x] as being a
concrete interface - I'm mixing the notion of a Liskov-style substitution
interface with a type bound: this doesn't work when an F-bound is involved.

Otherwise one could mix strings and ints and just about anything else into
the bargain when doing comparisons.

Again, doh! :-)


*** SNIP ***

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


My dialect of English calls that a, ahem, *feature*. ;-)


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


Well, I was thinking more of:-

interface __tmp_hack: IComparable[__tmp_hack]
{
}

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

Still, it's basically the same idea: equally as horrible.

As you reminded me, arrays are immutable, so either variation might work for
empty arrays too.

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

I agree with your diagnosis, though - when I thought of this I forgot about
upcasting and reflection.

*** SNIP ***

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

I was thinking that however the type inference system currently deals with
empty lists could be leveraged to deal with empty arrays - so in effect
there would be 'array['x]' on one hand and 'empty_array' on the other,
analogous to 'list.Cons', 'list.Nil'.

Still, this suffers from the same faults as the '__tmp_hack' solution above:
the 'empty_array' type is visible via reflection, and instances of
'empty_array' can escape local scopes via upcasting to System.Object or
System.Array.


You've made me realize that it might not be worth fixing up this corner case
in the language after all.

I say this because most of the time, empty arrays will arrive in a local
scope via some expression whose type can be inferred (e.g. a function
argument), rather than from an empty array constructor expression. That's
both useful in real life and perfectly permissible as the array element type
is known.

Even if an array constructor expression *is* used to create an empty array,
chances are that a couple of lines further down in the code, there will be
some use of the array that will cause type inference to bind the type
variable to something concrete.

This leaves code like my example as the remaining open case - and to be
honest I can probably live without that after all. Provided the compiler
emits a suitable error message...

"Gerard, you dolt, why are you creating an empty array that you could never
do anything useful with?"

...then I'd be happy!


Cheers,

Gerard