Hi Mark, Thanks for your reply. | | Arguments in favour: | | - It's more like term-variable pattern matching | | Term variables in a pattern are binding occurrences, but type | variables are not. Making the latter look more like the | former would appear to be a recipe for unnecessary confusion | given that that they are actually different. Why do you say "type variables are not"?. When I say f x = e I mean "inside e, use x as the name for whatever value is passed as argument to f". Under what Marcin proposes f (x::a) = e would mean "inside (type signatures in) e, use a as the name for whatever type is the type of the argument passed to f". 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". In which case it would certainly be wrong to allow f :: Int -> Int f (x::a) = e 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 (admittedly informal) translation works fine if T happens to be Int, for exampe; i.e. x's type is not universally quantified. In short, the pattern type signature is used solely to bind names to types, and not for universal quantification. I want to have a slightly more elaborate let-type, thus: g :: (Int,Bool) -> Int g (x::(a,b)) = e translates to g = \x::(Int,Bool) -> let-type (a,b) = (Int,Bool) in e But notice that the RHS of a pattern-matching let-type is statically guaranteed to have the right shape. So I don't allow let-type (a,b) = c in ... (where c is a type variable). So it's just syntactic sugar, like let-type itself, and I could equally well write g = \x::(Int,Bool) -> let-type a = Int; b = Bool in e 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 thought this might be of general enough interest to be worth continuing to cc the Haskell list. Simon