| | When you say there's a good theoretical foundation (typed lambda | | calcului) I think you are imagining that when we say | | | | f (x::a) = e | | | | we are saying "There's a /\a as well as a \x::a in this definition". | | No, that's not what I'm thinking. OK, let me try to give some type rules for what I have in mind. In these rules, I'm going to have an environment, T, that binds user type variables to types. (A "user type variable" is a type variable that appears in the program text.) There is still a conventional type environment, G (usually written Greek Gamma), that associates user term variables with their types. I'll just deal with type variables in lambda patterns, like \ (x::a) -> E Here's the rule: x_i = free-term-vars(pat) a_i = free-type-vars(pat) \ T (T, a_i=taua_i); (G, x_i:taux_i) |- pat : tau_1 (T, a_i=taua_i); (G, x_i:taux_i) |-- E : tau_2 ------------------------------------------------------- T;G |- \pat -> E : tau_1 -> tau_2 The a_i are the type variables brought into scope by the pattern; namely the free type variable of the pattern which are not already in scope (hence the \ T). The T environment is extended by binding each user type variable a_i to a type taua_i that is gotten out of thin air (as is common in type rules). This new T env is used when typechecking the pattern itself and the body E. The intereesting bit is how to typecheck patterns, and type inside them: T;G |- pat : tau T |- ty : tau ----------------- T;G |- pat::ty : tau That is, to typecheck the pattern (pat::ty), typecheck pat and typecheck ty. The judgement T |- ty : tau checks that the user type ty is well formed with type tau. The key rule of this judgement looks up a type variable in T: ----------------- T |- a : T(a) OK, that's it. The point is simply that the user type variables are regarded as the name of a type; the programmer doesn't specify just what that type is. The type rules just 'inline' the type wherever the name is used. All this translates into completely unmodified System F. | OK, so there are two questions | a) does that answer the question about the techincal foundation | b) is it a good design from a software engineering point of view | | I hope the answer to (a) is yes, but I realise that opinions may | differ about (b). This message is really just a second attempt at (a) Simon