conflicting variable definitions in pattern
It is pretty clear, that the following is not a valid Haskell pattern: foo (x:x:xs) = x:xs My questions is _why_ this is not allowed. IMHO, the semantics should be clear: The pattern is expected to succeed, iff 'x' is each time bound to the same term. Isn't this allowed, because this would require a strict evaluation of the 'x' variables? Thanks, Martin
What would you expect foo [id, \x -> x] to be? Martin Hofmann wrote on 15.05.2009 12:09:
It is pretty clear, that the following is not a valid Haskell pattern:
foo (x:x:xs) = x:xs
My questions is _why_ this is not allowed. IMHO, the semantics should be clear: The pattern is expected to succeed, iff 'x' is each time bound to the same term.
Isn't this allowed, because this would require a strict evaluation of the 'x' variables?
Thanks,
Martin
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Martin Hofmann wrote:
It is pretty clear, that the following is not a valid Haskell pattern:
foo (x:x:xs) = x:xs
My questions is _why_ this is not allowed. IMHO, the semantics should be clear: The pattern is expected to succeed, iff 'x' is each time bound to the same term.
Isn't this allowed, because this would require a strict evaluation of the 'x' variables?
One reason is: What if the list were a list of functions? How would you decide "sameness" of lambda-terms? By investigating their in-memory representations? By trying to prove that they denote the same mathematical function? Ciao, Janis. -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de
Martin Hofmann wrote:
It is pretty clear, that the following is not a valid Haskell pattern:
foo (x:x:xs) = x:xs
My questions is _why_ this is not allowed. IMHO, the semantics should be clear: The pattern is expected to succeed, iff 'x' is each time bound to the same term.
How do you define the "same term"? One natural way of compiling it would be to foo (x:y:xs) | x == y = x:xs but then pattern matching can introduce Eq constraints which some might see as a bit odd.
Isn't this allowed, because this would require a strict evaluation of the 'x' variables?
The translation into == would probably introduce some strictness, for most implementations of Eq. I don't think this is a huge problem in itself. Ganesh =============================================================================== Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html ===============================================================================
Hi On 15 May 2009, at 09:11, Sittampalam, Ganesh wrote:
Martin Hofmann wrote:
It is pretty clear, that the following is not a valid Haskell pattern:
foo (x:x:xs) = x:xs
My questions is _why_ this is not allowed. IMHO, the semantics should be clear: The pattern is expected to succeed, iff 'x' is each time bound to the same term.
That's what my daddy did in 1970. It was an extension of LISP with pattern matching. He used EQUAL. That makes me one of the few functional programmers who's had this feature taken away from them. I'm not weeping, but I do miss it.
How do you define the "same term"?
One natural way of compiling it would be to
foo (x:y:xs) | x == y = x:xs
but then pattern matching can introduce Eq constraints which some might see as a bit odd.
Doesn't seem that odd to me. Plenty of other language features come with constraints attached.
Isn't this allowed, because this would require a strict evaluation of the 'x' variables?
The translation into == would probably introduce some strictness, for most implementations of Eq. I don't think this is a huge problem in itself.
There's some conceptual ugliness in that such a mechanism *relies* on fall-through. In principle a sequence of guardless patterns can always be fleshed out (at some cost) to disjoint patterns. What precisely covers the case disjoint from (x, x)? This is fixable if one stops quibbling about guardlessness, or even if one adds inequality patterns. One certainly needs a convention about the order in which things happen: delaying equality tests until after constructor matching --- effectively the guard translation --- seems sensible and preserves the existing compilation regime. Otherwise, repeated pattern variables get (==)-tested, linear ones are lazy. Meanwhile, yes the semantics depends on the implementation of (==), but what's new? That's true of do too. The guard translation: linearize the pattern, introducing new vars for all but the leftmost occurrence of repeated vars. For each new x' made from x, add a guard x == x'. The new guards should come in the same order as the new variables and stand before any other guards present. Presumably one can already cook up an ugly version of this with view patterns ((x ==) -> True). It seems to me that the only questions of substance remaining is whether improved clarity in normal usage is worth a little more translational overhead to unpick what's wrong when weird things happen, and whether any such gain is worth the effort in implementation. I miss lots of stuff from when I was a kid. I used to write elem x (_ ++ x : _) = True elem _ _ = False and think that was cool. How dumb was I? Cheers Conor
Conor McBride wrote:
Hi
Sittampalam, Ganesh wrote:
Martin Hofmann wrote:
It is pretty clear, that the following is not a valid Haskell pattern:
foo (x:x:xs) = x:xs
My questions is _why_ this is not allowed. IMHO, the semantics should be clear: The pattern is expected to succeed, iff 'x' is each time bound to the same term.
That's what my daddy did in 1970. It was an extension of LISP with pattern matching. He used EQUAL. That makes me one of the few functional programmers who's had this feature taken away from them. I'm not weeping, but I do miss it.
On the one hand, unification is awesome; on the other hand, pattern matching is simple. The nice thing about the simplicity is that it's easy to compile into efficient code, and it's easy to explain/understand. Unification has all sorts of unfortunate consequences[1] and it's much harder to explain to the uninitiated. Curry[2] has features like this, but then it has full backtracking-search logic programming. It might be interesting to see if a more restricted form is useful in Haskell, though it should be an optional feature IMO so that it can be disabled for guaranteed-efficient patterns and typo detection. [1] e.g. optimal factoring of an unordered set of Prolog terms is NP-complete. For a fixed ordering there are good algorithms, and Haskell has fixed ordering due to the semantics of overlapping patterns, but this should still give some clues about what lurks beneath. [2] http://www.curry-language.org/
How do you define the "same term"?
One natural way of compiling it would be to
foo (x:y:xs) | x == y = x:xs
but then pattern matching can introduce Eq constraints which some might see as a bit odd.
Doesn't seem that odd to me. Plenty of other language features come with constraints attached.
Another option is to use structural matching all the way down. This has the benefit of not calling user-defined code, though it has the disadvantages of not matching heterogeneous but semantically-equal values. Of course, by removing the Eq constraint this also re-raises the specter of comparing functions. But it's a good Devil's Advocate definition to bear in mind. -- Live well, ~wren
I miss lots of stuff from when I was a kid. I used to write
elem x (_ ++ x : _) = True elem _ _ = False
and think that was cool. How dumb was I?
Yeah, the Kiel Reduction Language had similarly expressive and fun pattern matching, with subsequence matching and backtracking if the guard failed. Of course, these days, you could use view patterns for the simpler cases, but it doesn't look quite as nice: elem x (break (==x) -> (_, _:_)) = True elem _ _ = False and gets ugly enough to spoil the fun quickly: -- lookup key (_++((key,value):_)) = Just value lookup key (break ((==key).fst) -> (_ , (_,value):_)) = Just value lookup _ _ = Nothing Also, view patterns don't handle match failure by an implicit Monad, let alone MonadPlus, so one often has to insert an explicit Maybe, and there is no backtracking:-( Claus -- Nostalgia isn't what it used to be [source: ?]
Conor McBride wrote:
On 15 May 2009, at 09:11, Sittampalam, Ganesh wrote:
but then pattern matching can introduce Eq constraints which some might see as a bit odd.
Doesn't seem that odd to me. Plenty of other language features come with constraints attached.
It's the introduction of a constraint from tweaking a pattern that is odd, I think. By way of precedent H98 rejected this kind of idea in favour of putting 'fail' into Monad. Ganesh =============================================================================== Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html ===============================================================================
In the original language design the Haskell committee considered
allowing multiple occurrences of the same variable in a pattern (with
the suggested equality tests), but it was rejected in favour of
simplicity.
-- Lennart
On Fri, May 15, 2009 at 11:30 AM, Sittampalam, Ganesh
Conor McBride wrote:
On 15 May 2009, at 09:11, Sittampalam, Ganesh wrote:
but then pattern matching can introduce Eq constraints which some might see as a bit odd.
Doesn't seem that odd to me. Plenty of other language features come with constraints attached.
It's the introduction of a constraint from tweaking a pattern that is odd, I think. By way of precedent H98 rejected this kind of idea in favour of putting 'fail' into Monad.
Ganesh
=============================================================================== Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html ===============================================================================
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
On 15 May 2009, at 12:07, Lennart Augustsson wrote:
In the original language design the Haskell committee considered allowing multiple occurrences of the same variable in a pattern (with the suggested equality tests), but it was rejected in favour of simplicity.
Simplicity for whom, is the question? My point is only that there's no technical horror to the proposal. It's just that, given guards, the benefit (in simplicity of program comprehension) of nonlinear patterns over explicit == is noticeable but hardly spectacular. Rumblings about funny termination behaviour, equality for functions, and the complexity of unification (which isn't the proposal anyway) are wide of the mark. This is just an ordinary cost-versus-benefit issue. My guess is that if this feature were already in, few would be campaigning to remove it. (By all means step up and say why!) As it's not in, it has to compete with other priorities: I'm mildly positive about nonlinear patterns, but there are more important concerns. Frankly, the worst consequence I've had from Haskell's pattern linearity was just my father's derision. He quite naturally complained that his programs had lost some of their simplicity. All the best Conor
Conor McBride wrote on 15.05.2009 16:19:
My guess is that if this feature were already in, few would be campaigning to remove it.
You're probably right. For example, I'm not compaigning to remove multiple inheritance (from non-abstract classes) from C++. But I still think it's an ugly feature, it'd be better not to have it, it's encouraging bad design etc. The same for this Eq-patterns. BTW, why stop on (x:x:xs)? Let's use patterns like (x:factorial(x):xs), or (factorial(x):x:xs), or (factorial(x):xs)... No, wait, the last pattern would be impossible to compile. But I think you've got the point.
Simplicity of pattern matching semantics, not of implementation (we
all knew how to implement it).
Miranda had non-linear patterns, but nobody really argued for them in Haskell.
If Haskell had them, I'd not argue to have them removed, but nor will
I argue to add them.
-- Lennart
On Fri, May 15, 2009 at 1:19 PM, Conor McBride
On 15 May 2009, at 12:07, Lennart Augustsson wrote:
In the original language design the Haskell committee considered allowing multiple occurrences of the same variable in a pattern (with the suggested equality tests), but it was rejected in favour of simplicity.
Simplicity for whom, is the question? My point is only that there's no technical horror to the proposal. It's just that, given guards, the benefit (in simplicity of program comprehension) of nonlinear patterns over explicit == is noticeable but hardly spectacular.
Rumblings about funny termination behaviour, equality for functions, and the complexity of unification (which isn't the proposal anyway) are wide of the mark. This is just an ordinary cost-versus-benefit issue. My guess is that if this feature were already in, few would be campaigning to remove it. (By all means step up and say why!) As it's not in, it has to compete with other priorities: I'm mildly positive about nonlinear patterns, but there are more important concerns.
Frankly, the worst consequence I've had from Haskell's pattern linearity was just my father's derision. He quite naturally complained that his programs had lost some of their simplicity.
All the best
Conor
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Conor McBride wrote:
Rumblings about funny termination behaviour, equality for functions, and the complexity of unification (which isn't the proposal anyway)
But unification is what you get by adding non-linearity. Sure, all terms are ground; would you prefer I said "testing for membership in an element of the RATEG class"? For more ickiness about RATEG, it's not closed under compliment and the emptiness problem is undecidable (so dead code elimination can't always work). Even restricting to the closed subset (aka "tree-automata with (dis-)equality constraints") leaves emptiness undecidable, though there are a couple still more restricted classes that are decidable. cf ch.4 of TATA http://tata.gforge.inria.fr/ -- Live well, ~wren
On 16 May 2009, at 03:54, wren ng thornton wrote:
Conor McBride wrote:
Rumblings about funny termination behaviour, equality for functions, and the complexity of unification (which isn't the proposal anyway)
But unification is what you get by adding non-linearity.
Hang on a minute: we're solving for sb in sb(p)=v not in sb(s)=sb(t)...
Sure, all terms are ground;
...which makes it a rather special and degenerate and unawesome case of unification: the kind of unification you don't need a unification algorithm to solve.
would you prefer I said "testing for membership in an element of the RATEG class"?
I'm not familiar with that terminology, but I'll check out the link.
For more ickiness about RATEG, it's not closed under compliment and the emptiness problem is undecidable (so dead code elimination can't always work). Even restricting to the closed subset (aka "tree- automata with (dis-)equality constraints") leaves emptiness undecidable, though there are a couple still more restricted classes that are decidable.
cf ch.4 of TATA http://tata.gforge.inria.fr/
Let's be clear. The suggestion is only that a slightly more compact notation be permitted for functionality already available via guards or view patterns. It cannot introduce any dead code elimination problems which are not already present. I'm sorry, but I just don't see the bogeyman here. All the best Conor
Dear Martin, I think that the (practical) reason is avoiding equality checks during pattern matching. For instance, how do you evaluate this: foo ((+1):(1+):[]) ? Both expressions in the first and second entries of the list are semantically equivalent, but from an operational point of view, you have to ensure the equality of two functions over an infinite domain (of integer numbers). Best regards, Salvador. Martin Hofmann escribió:
It is pretty clear, that the following is not a valid Haskell pattern:
foo (x:x:xs) = x:xs
My questions is _why_ this is not allowed. IMHO, the semantics should be clear: The pattern is expected to succeed, iff 'x' is each time bound to the same term.
Isn't this allowed, because this would require a strict evaluation of the 'x' variables?
Thanks,
Martin
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Why, then, not permit such definitions only for members of Eq?
My thoughts:
- because it will break an important invariant indicated by Martin,
namely the one that says that pattern variables are not forced
- it will make efficient compilation of pattern matching much harder
- it will make the termination behavior of pattern matching dependent
not only on the term being matched, but also on how Eq is implemented
for that type
- it will make the very rules of evaluation for pattern matching much
more complex, fragile and hard to understand: in what order should the
equated parts be evaluated? That influences termination behavior, so
it is important. In what order should equality comparisons be
performed in
f (Node a (Leaf b a) (Node a))) = b
?
2009/5/15 Salvador Lucas
Dear Martin,
I think that the (practical) reason is avoiding equality checks during pattern matching.
For instance, how do you evaluate this:
foo ((+1):(1+):[]) ?
Both expressions in the first and second entries of the list are semantically equivalent, but from an operational point of view, you have to ensure the equality of two functions over an infinite domain (of integer numbers).
Best regards,
Salvador.
Martin Hofmann escribió:
It is pretty clear, that the following is not a valid Haskell pattern:
foo (x:x:xs) = x:xs
My questions is _why_ this is not allowed. IMHO, the semantics should be clear: The pattern is expected to succeed, iff 'x' is each time bound to the same term. Isn't this allowed, because this would require a strict evaluation of the 'x' variables?
Thanks,
Martin
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
-- Eugene Kirpichov Web IR developer, market.yandex.ru
Algebraic datatypes are built and unpacked with constructors. Pattern matching is just a way to use these constructors. This is distinct from the kind of unification/validation that happens in logic languages like Prolog. There is no special list constructor for when the first two items are equal. -- Jason Dusek
participants (11)
-
Claus Reinke -
Conor McBride -
Eugene Kirpichov -
Janis Voigtlaender -
Jason Dusek -
Lennart Augustsson -
Martin Hofmann -
Miguel Mitrofanov -
Salvador Lucas -
Sittampalam, Ganesh -
wren ng thornton