On Wed, Jul 9, 2014 at 6:54 PM, Jonathan S. Shapiro <[email protected]>
wrote:

> I understood you. But the standard for inference is sound and complete
> inference. If you have that, no "auxiliary" inference engine is necessary,
> required, or useful.
>

I'm sorry, Matt. I'm being terse because I'm racing to get out the door for
something. Here's a more constructive response:

Where inference is concerned, we're going to end up in one of two positions:

1. Sound and complete inference for everything, with explicit type
annotations permitted but not required.
2. Local inference, where procedure types must be explicitly declared.

The thing that may drive us to [2] is polymorphic recursion, or
(equivalently) the variant in which methods may be overloaded on type. That
pushes you to semi-unification, which is not generally decidable. At that
point you have several options to choose from:

1. Require type annotations, at least in certain cases
2. Give up complete inference, identifying the cases where the inference
algorithm will require annotations.

Since the Tofte-Talpin region system *also* pushes you to semi-unification,
we'll at least end up with a set of deficiencies that manifest in a
consistent way in different parts of the type system. I think it would feel
awkward if region type inference tended to fail for qualitatively different
reasons than (e.g.) polymorphic recursion. It makes it much harder to get
any intuitive handle on what's going on.

Then there's the fact that rank-k polymorphic type reconstruction for k>2
isn't decidable...


Type inference is a thing that sits on several different kinds of sharp
edges all at once. I'm tempted to say that we should just require top-level
procedure types to be annotated. The problem with that is that humans turn
out to be pretty bad at discovering complete types when the types start
getting complicated, and we have a bunch of interacting typing problems
going on at once in our type system in ways that other languages have never
explored.


shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev

Reply via email to