Date: Sun, 27 Apr 2003 19:37:35 -0400 (EDT)
From: C. Scott Ananian
To: jsr14-prototype-comments@sun.com
Subject: Type inference failure.

I was reading "Subtypes vs. Where Clauses: Constraining Parametric
Polymorphism" (Day,Gruber,Liskov,Myers) in the OOPSLA'95 proceedings, and
came across an example of which it was said, "Langugages whose type
systems are based on F-bounded quantification... cannot express the type
of findpath".  Well, said I, I wonder if JSR-14 can?

The original example, in Theta syntax, I think, was:

  findpath[N,E] (s,d:N) returns (array[N]) signals (no_path)
     where N has edges() yields (E),
                 equal(N) returns (bool),
           E has source() returns (N),
                 dest() returns (N)

The key property here is that there is mutual recursion between the bounds
on N and E.

I translated the example into JSR-14 to obtain:
-------
import java.util.List;
public abstract class Baz {
    static interface Node<N extends Node<N,E>, E extends Edge<N,E>> {
	List<E> edges();
	boolean isEqual(N n);
    }
    static interface Edge<N extends Node<N,E>, E extends Edge<N,E>> {
	N source();
	N dest();
    }

    static <N extends Node<N,E>, E extends Edge<N,E>>
				    List<N> findPath(N source, N dest) {
	return null;
    }
}
------

This compiles.  So far so good.  We *can* express mutual recursion between
type bounds! (I'll have to go fix my javadoc-for-JSR14 tool, since I'd
assumed the lexical scope of type parameter 'E' started at the definition
of E --- but silly me, the spec says clearly that the scope should be the
entire section.)

Anyway, so I go ahead and add an implementation and a invocation of
findPath to Baz:

----
    static class MyNode implements Node<MyNode,MyEdge> {
	public List<MyEdge> edges() { return null; }
	public boolean isEqual(MyNode n) { return true; }
    }
    static class MyEdge implements Edge<MyNode,MyEdge> {
	public MyNode source() { return null; }
	public MyNode dest() { return null; }
    }

    public static void main(String[] args) {
	MyNode a = new MyNode(), b = new MyNode();
	List<MyNode> l = findPath(a, b);
    }
-------

And, unfortunately, this no longer compiles:
---
Baz.java:28: findPath<N extends Baz.Node<N,E>, E extends
Baz.Edge<N,E>>(N,N) in Baz cannot be applied to (Baz.MyNode,Baz.MyNode)
        List<MyNode> l = findPath(a, b);
                         ^
1 error
---
[Complete source code to Baz attached, so you can try this yourself.]

I believe this should be considered a bug in the type inference algorithm.
Am I wrong?

You seem to have hinted that a new (more-powerful?) inference algorithm is
in the works.  Can the new algorithm correctly resolve this code?

Hopefully this example is helpful.
 --scott

Saddam Hussein Bush quiche RUCKUS security South Africa colonel immediate 
[Hello to all my fans in domestic surveillance] Yeltsin India Clinton 
                         ( http://cscott.net/ )

    [ Part 2, ""  Text/PLAIN (Name: "Baz.java")  18 lines. ]