Hi Simon, | 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. When you say "f (x::a) = e", I'm reading it as meaning something like: "f = \(x::a).e". This is the typed lambda-calculus perspective that I was referring to. And, in such systems (whether simply typed or polymorphicly typed) the type annotation on the lambda bound variable x does not bind any type variables appearing in a. (And note that the type annotation may not contain any variables, or it could contain repeated uses of the same variable, etc...) Binding of type variables is a separate matter. It may be done by some kind of /\, either explicit or implicit. For the binding above, those variables would have to be bound somewhere, either added, implicitly to the binding of f, or else to some enclosing function. | But I'm suggesting something different | | * Place the big lambdas wherever they would be now (i.e. not influenced | by the position of (x::a) type signatures. | | * Explain the pattern type signatures as let-bindings for types. Thus | we might translate f to system-F like this: | | f = \x::T -> let-type a = T in e | | I've use let-type here, but one could equally well say (/\a -> e) T. This is a different interpretation of type annotations than the one you'll find in many typed lambda-calculi. (That's a statement of fact rather than a judgment of merits.) In fact I'm not aware of any work on type systems like this. The simple translation that you give for let-type looks ok from the perspective of System-F, say. However, in the context of Haskell, I think it would be prudent to determine how it extends to and interacts with things like type inference, polymorphism, and overloading. Perhaps it would be worth considering a new language construct, such as: let-type expr :: type in expr with the intention that the first expr is not evaluated, but used to guide the binding of type variables in the "type" part, which would then be in scope in the second expression. This is a little more powerful than your let-type because it allows a kind of pattern matching on type expressions. But I don't know if this would be a well-behaved construct, or if it would be useful ... | 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). I'm not persuaded about (a), I can't comment on (b), and I think there should be a third question: c) when is it useful? what holes does it fill? All the best, Mark PS. Aside ... if you'd like type variables in type annotations to be binding, then perhaps you'd also like them to work more like regular pattern bindings and to see functions like the following: f :: a -> b -> String f (x::a) (y::a) = "Yes, the arguments are the same type" f _ _ = "No, the arguments have different types" showList :: [a] -> String showList (xs::[Char]) = ... show a string enclosed in "'s ... showList xs = ... show list enclosed in [ ... ]s ... Who needs overloading anyway? :-)