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

[Gerard Murphy]

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.

 

Here's the source I've been working with:-

 

/************** EXAMPLE *******************/

 

//#define ITEM1

//#define ITEM2

//#define ITEM3

//#define ITEM4

//#define ITEM5

 

module LearningNemerle

{

    public

    Main(): void

    {

        BogoSort();

    }

 

    private

    BogoSort(): void

    {

#if ITEM1

        def someSortableThings =
Nemerle.Collections.List.FromArray(array[]);

#else

        def someSortableThings =
Nemerle.Collections.List.FromArray(array["Ooble", "Booble"]);

#endif

 

        def createAllPermutationsOf(things)

        {

            | headOfThings::tailOfThings =>

              {

                  def addElementToSequenceAtEachPosition(sequence)

                  {

                      | headOfSequence::tailOfSequence =>
(headOfThings::headOfSequence::tailOfSequence)::Nemerle.Collections.List.Map
(addElementToSequenceAtEachPosition(tailOfSequence), fun
(subPermutationWithAddedElement)
{headOfSequence::subPermutationWithAddedElement})

                      | [] => [[headOfThings]]

                  }

                  

 
Nemerle.Collections.List.Flatten(Nemerle.Collections.List.Map(createAllPermu
tationsOf(tailOfThings),

 
addElementToSequenceAtEachPosition))

              }

            | [] => [[]]

        }

 

        def selectSortedPermutation(permutations)

        {

            | head::tail =>

              {

#if ITEM2

                  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

                  }

                  

#elif ITEM3

                  def isSorted[Element](sequence) where Element:
System.IComparable[Element]

                  {

                      | head::nextOne::tail => isSorted(nextOne::tail) &&
(head: Element).CompareTo(nextOne: Element) != 1

                      | []

                      | _::[] => true

                  }

#elif ITEM4

                  def isSorted(sequence)

                  {

                      | head::nextOne::tail => isSorted(nextOne::tail) &&
head.CompareTo(nextOne) != 1

                      | []

                      | _::[] => true

                  }

#else

                  def isSorted[Element](sequence: list[Element]) where
Element: System.IComparable[Element]

                  {

                      | head::nextOne::tail => isSorted(nextOne::tail) &&
head.CompareTo(nextOne) != 1

                      | []

                      | _::[] => true

                  }

#endif                  

                  if (isSorted(head))

                      head

                  else

                      selectSortedPermutation(tail)

              }

            | [] => throw System.ArgumentException("Precondition violation:
no sorted collection contained in 'permutations'.")

        }

 

       

#if ITEM5

 
System.Console.WriteLine(selectSortedPermutation(createAllPermutationsOf(som
eSortableThings)));

          

        def someOtherSortableThings =
Nemerle.Collections.List.FromArray(array[1]);

 
System.Console.WriteLine(selectSortedPermutation(createAllPermutationsOf(som
eOtherSortableThings)))

#else

 
System.Console.WriteLine(selectSortedPermutation(createAllPermutationsOf(som
eSortableThings)))

#endif

    }

}

 

 

/************** END OF EXAMPLE **********/

 

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

 

If you leave the initial defines commented out, the program compiles and
executes correctly and there are no surprises.

 

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

 

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.

 

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.

 

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.

 

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.

 

 

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

 

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.

 

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.

 

 

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

 

 

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.

 

 

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.

 

 

Kind Regards,

 

Gerard Murphy, www.sageserpent.com <http://www.sageserpent.com/> 

 

 

 

 

 

 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: /mailman/pipermail/devel-en/attachments/20051111/0ec0079c/attachment-0001.html