In type inference, the compiler starts with the formal structure of a function--its representation in some programming language--and infers the type that such an expression must have.
Two ideas I have posted, implicit arguments and commutative programming languages, perform inference in the reverse direction: they start with the type of a function, and infer what the arguments are. In other words, they determine the structure of an expression based on its type. This is a more general concept that I'll call "expression inference."
I do not think that "value inference," even though values are normally thought of as the counterparts of types, is a good name for this type of inference. The reason is that type inference also infers values; the type of an expression must combine with the form of the expression to determine the actual value of the expression. Both "type inference" and "expression inference" can be thought of simply as two different kinds of "value inference."
Commutative programming and implicit arguments are two examples of expression inference. Some more examples of what you might ask the compiler to do with expression inference (and, in some cases, dependent types):
Two ideas I have posted, implicit arguments and commutative programming languages, perform inference in the reverse direction: they start with the type of a function, and infer what the arguments are. In other words, they determine the structure of an expression based on its type. This is a more general concept that I'll call "expression inference."
I do not think that "value inference," even though values are normally thought of as the counterparts of types, is a good name for this type of inference. The reason is that type inference also infers values; the type of an expression must combine with the form of the expression to determine the actual value of the expression. Both "type inference" and "expression inference" can be thought of simply as two different kinds of "value inference."
Commutative programming and implicit arguments are two examples of expression inference. Some more examples of what you might ask the compiler to do with expression inference (and, in some cases, dependent types):
- "Give me a function of type Int -> Int"
- "Choose two functions from this set S of functions, so that their composition has type A -> B"
- (method overloading) "Pick one of the methods of a class C that are named 'init,' so that the type signature of this method is A -> B"
- (using dependent types to express pattern matching)"Give me a function f of type x -> y such that x and y are integers, and if x is 0 then y is 1, and if x is greater than 0 then y is x * f(x - 1)"
- (using dependent types to express sorting)"Give me a function of type x -> y where x and y are lists of integers and x and y are equal when considered as multisets and for all z, w in y, index(z) <= index(w) iff z <= w"
© Bart Parkis
Last modified:Tue May 19 19:07:52 2009