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

[Gerard Murphy]

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.

It was that kind of thinking that led me to propose adding support for []
and array[] is being values of polymorphic types.

I can see why you might not be able to have a *value* with a run-time
polymorphic type in .NET, even though the compile-time type is truly
polymorphic, so this won't work straightaway in Nermele.

(Although that begs the question as to how it works in F#? Anybody reading
this who knows the answer?)

Now, you could try simulating this in Nemerle with a compiler-generated
interface type that captures the idea of the polymorphic type for a value
that is structurally independent of any type parameters...

[] is of type list 'a, so get the compiler to generate:-

interface __tmp_hack_1
{
}

new List[__tmp_hack_1]()


isSorted([]) causes [] to be of polymorphic type list 'a where 'a:
IComparable['a], so get the compiler to generate:-

interface __tmp_hack_2: IComparable[__tmp_hack_2]
{
}

isSorted(new List[__tmp_hack_2]())


The idea is to generate these interfaces on the fly as you compile. You do
this whenever you see a non-directed polymorphic *value* in the code,
'freezing' any cyclic dependencies into where constraints on the concrete
interface type. This concrete interface type should never have any
subclasses in real code.

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

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.


I think that you are considering a solution along these lines, but I'd like
to try and talk you out of this...


1. Going back to the original code, the only reason why I wrote that with an
empty array was to do a quick test to see if the sort algorithm would work
correctly on an empty list.

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


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.

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


2. If you still aren't convinced, here's a snippet of code that forms the
text of an assembly, let's call it Assembly #1...

// Assembly #1....

namespace Provider
{
    module ProblemCases
    {
        public static
        thinkBadThoughts(): System.Object
        {
            []
        }
        
        public static
        makeTrouble(): System.Object
        {
            def whatTypeAmI()
            {
                []
            }

            whatTypeAmI()
        }

        public static
        makeMoreTrouble(): System.Array
        {
            def whatTypeAmI()
            {
                array[]
            }
        }

        public static
        beIrritating(): System.Object
        {
            makeMoreTrouble()
        }

        public static
        forGodsSake(): System.Object
        {
            def iAmAStubAndWillEventuallyDoSomethingUseful()
            {
                []
            }

            def isSorted(sequence) 
            {
                | head::nextOne::tail =>
                  def isLessThanOrEqualTo[Element](lhs, rhs) where Element:
System.IComparable[Element]
                  {
                      lhs.CompareTo(rhs) != 1
                  }
                  isSorted(nextOne::tail) && isLessThanOrEqualTo(head,
nextOne)

                | []
                | _::[] => true
            }

            def result = iAmAStubAndWillEventuallyDoSomethingUseful();

            if (isSorted(result))
                result
            else
                throw System.ArgumentException("Drat: postcondition
failure.")
        }

        public static
        pleasePutMeOutOfMyMisery(): System.Object
        {
            def iAmAStubAndWillEventuallyDoSomethingUseful()
            {
                array[]
            }

            def isSorted(sequence)
            {
                def isSortedStartingAtIndex(index) 
                {
                    if sequence.Length() >= 2 + index
                    {
                        def isLessThanOrEqualTo[Element](lhs, rhs) where
Element: System.IComparable[Element]
                        {
                            lhs.CompareTo(rhs) != 1
                        }
                        isSortedStartingAtIndex(index + 1) &&
isLessThanOrEqualTo(sequence[index], sequence[index + 1])
                    }
                    else
                        true
                }

                isSortedStartingAtIndex(0)
            }

            def result = iAmAStubAndWillEventuallyDoSomethingUseful();

            if (isSorted(result))
                result
            else
                throw System.ArgumentException("Drat: postcondition
failure.")
        }
    }
}

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.

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

Now, consider what some code in a client assembly might want to do with the
results of calling these public static functions in module 'ProblemCases'...


I'll follow up with the source text of Assembly #2 tomorrow if you wish, but
I'll leave the above with you for now... it beats me as to how you could
solve this in an elegant but efficient way.


As ever, if you see flaws in my arguments so far, I would be delighted to
have them refuted. :-)

Regards,

Gerard