I've been pondering this over dinner. It's a rough thought, but I want to
put it out for consideration.
Type inference is a form of constrained proof discharge. In the examples
that concern us, inference is decidable. It is decidable because (a) the
constructors are statically resolvable [non abstract], (b) there is a
certain property of inductive decomposition due to the nature of type
construction providing structural induction, and (c) there are no points of
non-deterministic choice.
I have spoken of statically resolved constant terms. Others here have
spoken of "lifting" certain kinds of constants to types. I think both of
these views are valid, but I want to suggest an alternative way to think
about this: it's all about the "laws of inference".
Seen in a certain light, HM-style inference has very little to do with
types. The basic requirements are (1) there exists some set of ground
(atomic) entities, and (2) there exists some form of structural composition
over these, leading to a structural induction, and (3) the names of the
atomic entities and the constructors are statically resolvable. There is
nothing magical in saying that [1] is ground types and [2] is type
constructors. If it were somehow useful we could do HM-style inference on
literals and construction over literals (composite literals).
So one view is that we are "lifting" some things into higher-order types.
But another view is that we are expanding the domain over which inference
can sensibly operate in such a way that the enabling laws of inference are
preserved. The two views are clearly inter-convertible. Conceptually, we
could replace the domain of "types" in a programming language with the
domain of "inductibles" without fundamentally altering anything.
Up to a point.
Consider a perverse, hypothetical instantiation of Ord 'a over int:
instance Ord int is
(<) = fn x y is
count := count +1
primative_int_less(x, y)
Note the update to "count", with the intent being that we will count the
number of invocations of integer-<. Note further that the presence or
absence of this count does not alter the fact that this "binding" for "Ord
int" is sufficiently constant to be treated as something that is (a)
structurally inductable, and (b) compile-time specializable.
What this seems to suggest is that the test of "can it be
structurally-inductively inferred and specialized" is more subtle than I
suggested above. I'm not exactly sure how to state the requirement for this
form of specialization to be legal. In the end, I suspect it has a lot to
do with static resolvability.
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
