[Prev][Next][Index][Thread]
Type inference and implicit conversions
Because of the recent messages on the interaction between type inference
and implicit conversions, I'd like to call attention to my research
report, "Lambda Calculi with Implicit Type Conversions," in which I
present some results on the effects of alpha-, beta-, and eta-reduction
on the types of phrases in what I call "coercive lambda calculi."
By way of introduction, let me say that a "coercive lambda calculus" has
a partially ordered set of types. It has a principal type checking
discipline. Type inference is defined in terms of a homomorphism between
algebras because of my belief that determining the type of phrase should
be much easier than carrying out the computation denoted by a phrase. A
coercive lambda calculus has the untyped lambda calculus sitting in in a
natural way.
Unsurprisingly, alpha-conversion does not change the type of a phrase.
However, the statement of this result that I give has an interesting
algebraic formulation saying that there is a unique homomorphism that
makes a certain diagram commute.
Beta-reduction may change the type of a phrase, but it does so in a
coherent way. Roughly speaking, the type of a phrase is reduced in the
partial order. Alternatively, one may say the type moves away from the
maximal type "top" (which I formerly called "nonsense"). This reflects
the intuition that beta-reduction is a positive computational step that
can bring us closer to the natural transformation that a phrase denotes
in a Cartesian closed category.
To obtain the above results on alpha-conversion and beta-reduction in an
elegant, one should first develop an algebraic approach to simultaneous
substitution in any lambda calculus, and one should formulate a general
result describing what happens to the type of a phrase L when one
simultaneously substitutes new phrases for some of the identifiers that
occur freely (i.e. unbound, and hence, in a sense, untyped) in L. The
above results are then corollaries to the general theorem.
Eta-reduction is a delicate matter. I give a theorem indicating when
eta-reduction is reasonable, and in these cases eta-reduction reduces the
type of a phrase much as does beta-reduction. Certain phrases, that I
call "purely procedural phrases" (phrases that have higher order types
in all contexts) play a distingushed role because they have an
especially strong eta-reduction property: roughly speaking, an
eta-reduction which results in such a phrases causes no trouble, no
matter what the context.
Precise statements of these results with detailed proofs are in the
research report. Some of these results were in my Ph.D. dissertation,
but the new treatment is much more complete and more extensive.
Frank J. Oles (oles@ibm.com)