Minimize inferred type annotations

[joshsh]

Currently, Hydra's type inference infers, and stores as an annotation, a type not only for every element in a graph, but also for every subterm of every element. If you think of a term as a tree, every node in the tree bears a type annotation after type inference. Because every subterm has an annotation, we don't have to anticipate when the annotations will actually be needed, and when they will not. The Java coder, for example, relies much more heavily on type annotations than the Haskell coder does.

We could eliminate most of the overhead of computing, transforming, and storing these annotations if we simply provide a context-specific criterion for adding them. If the criterion evaluates to true, then we store an annotation. If not, then we don't. The Haskell coder only needs top-level annotations on elements, and nothing more. The Java coder additionally needs annotations on lambdas and other function terms, as well as in a few other places -- but it certainly doesn't need an annotation on every subterm. Type inference should be much faster after this is fixed.

[joshsh]

Another approach to this problem is simply to follow Algorithm W in storing type annotations in two places: domain types for lambdas, and forall types for 'let' bindings. It is TBD whether this is enough to support Java, which in some circumstances requires internal type signatures for anonymous functions, including the domain and codomain type.

[joshsh]

Keeping this issue open only as long as it takes to adjust the Java coder to the new inference implementation. The new format for inferred type annotations has been finalized, but the Java coder has not caught up yet.

[joshsh]

This issue is not useful any longer. While the Java coder has not caught up yet, the Python coder uses only System F -style type annotations. The Java coder will be updated soon enough.