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
_______________________________________________
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
