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
Tue, 8 May 2001 00:47:58 -0700, Simon Peyton-Jones <simonpj@microsoft.com> pisze:
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).
Really? I disagree. Making pattern type sygnatures perform unification of the variable with the supplied signature is useful for resolving ambiguities, and backward-compatible (valid programs will remain valid), and doesn't allow "unwanted generality" to cause trouble (when an expression has a more general type than needed). Currently ghc does not accept: (\(x::a) -> x) :: Int->Int but accepts this: (let f = \(x::a) -> x in f) :: Int->Int Hugs accepts both! But it doesn't like (\(x::a) -> (x::Int)) I would make all three legal. Unfortunately it doesn't help for my example: f:: (IArray a e, Ix i) => a i e -> a i e f arr = runST (do (marr :: STArray s i e) <- thaw arr do some stateful operations on marr freeze marr) unless the type inference could deduce that the constraint MArray (STArray s') e (ST s) in the presence of instance MArray (STArray s) e (ST s) unifies s' with s. -- __("< Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK
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? :-)
participants (3)
-
Marcin 'Qrczak' Kowalczyk -
Mark P Jones -
Simon Peyton-Jones