dumb question on LHS linearity
Arman
I am a little confused as to the necessity of the LHS linearity
requirement. For instance, the following is not allowed:
same x x = 1;
But, this is equivalent to:
same x y = 1 if x===y;
Which would be easy for the compiler to figure out. So, why not allow
repeat variables in the LHS?
I assume this has something to do with not wanting the LHS expression
matching to fall into an infinite loop, e.g. "same (1..inf)
(1..inf)". Anyway, unification in Prolog allowed this sort of
matching and I can't see why its disallowed in pure.
Best Regards,
-arman
Albert Graef
> Which would be easy for the compiler to figure out. So, why not allow
> repeat variables in the LHS?
It's a design decision, and as such open to debate. You're right, it
would be quite easy to implement. There's no issue with infinite loops
like in unification here, this can't happen with simple matching. But
there are some good reasons why I did it this way:
- "No hidden magic". A nonlinearity may hide away a potentially costly
syntactic equality check. Forbidding non-linearities forces the
programmer to think about this, and maybe come up with a better way to
arrange the necessary checks.
- The linearity check allows the compiler to point out errors where the
programmer errorneously named two lhs variables the same. This is a
fairly typical editing blunder which happens more often than you might
think. ;-)
- 'bar x x = x*x' would mean something entirely different than 'bar x =
\x -> x*x' or 'frob = \x x -> x*x'. This is very confusing, especially
for beginners. Actually, this is what bothers me the most about
nonlinearities in a language with lambdas, and I suspect that's why
there's *no* FPL (except Q), to my knowledge, which allows them.
OTOH, forbidding nonlinearities makes symbolic factorization rules look
a bit clumsy. But it's only a minor annoyance in those cases, and I
think that the "cons" sketched out above just weigh in more.
Albert
--
Dr. Albert Gr"af
Dept. of Music-Informatics, University of Mainz, Germany
Email: Dr.G...@t-online.de, a...@muwiinfa.geschichte.uni-mainz.de
WWW: http://www.musikinformatik.uni-mainz.de/ag
Arman
> - "No hidden magic". A nonlinearity may hide away a potentially costly
> syntactic equality check. Forbidding non-linearities forces the
> programmer to think about this, and maybe come up with a better way to
> arrange the necessary checks.
lot of inadvertent or excessive pattern matching. I just don't
remember this being a problem when programming with Prolog many moons
ago.
> - The linearity check allows the compiler to point out errors where the
> think. ;-)
> - 'bar x x = x*x' would mean something entirely different than 'bar x =
> \x -> x*x' or 'frob = \x x -> x*x'. This is very confusing, especially
> for beginners. Actually, this is what bothers me the most about
> nonlinearities in a language with lambdas, and I suspect that's why
> there's *no* FPL (except Q), to my knowledge, which allows them.
of course, quite different from 'bar x = \x -> x*x'. I haven't dealt
with FP languages enough to know if this would confuse users.
As for 'frob = \x x -> x*x', perhaps this needs to result in a syntax
error as well under the current model?
> OTOH, forbidding nonlinearities makes symbolic factorization rules look
> a bit clumsy. But it's only a minor annoyance in those cases, and I
> think that the "cons" sketched out above just weigh in more.
Best Regards,
-arman
Albert Graef
> But this would only arise if the non-linearity in a program caused a
> lot of inadvertent or excessive pattern matching. I just don't
> remember this being a problem when programming with Prolog many moons
> ago.
Well, with Prolog this isn't a (big) issue because you don't have lazy
data structures in most Prolog dialects. Pure has those, and thus
non-linearities may cause an innocent-looking rule to loop on pattern
matching, which is *very* bad.
Even in term rewriting theory non-linearities wreak all kind of havoc.
Here's an old thread on the Haskell mailing list which sheds some light
on this: http://www.mail-archive.com/has...@haskell.org/msg03721.html
> As for 'frob = \x x -> x*x', perhaps this needs to result in a syntax
> error as well under the current model?
No. According to standard lambda calculus, \x x -> x*x is just \x -> \x
-> x*x and thus the x in x*x gets bound by the innermost \x. You don't
want to forbid this, otherwise you end up forbidding *all* shadowing of
variables, and that kind of defeats the purpose of having lexical block
structure.
L
> Well, with Prolog this isn't a (big) issue because you don't have lazy
> data structures in most Prolog dialects. Pure has those, and thus
> non-linearities may cause an innocent-looking rule to loop on pattern
> matching, which is *very* bad.
Still, I think this question is going to keep coming up because
a lot of people expect to gain maximum conciseness and ease
of programming in return for the dynamic typing performance penalty
and, unfortunately,
same x x = 1; // is much easier to write and read than:
Albert Graef
> I find this the most convincing reason so far.
The problem becomes even worse when there's n>2 instances of a variable
in a pattern. The compiler would have to decide which n-1 of the
n*(n-1)/2 equalities to check, and for each order there are cases were
any given order might not terminate while others might succeed, and of
course this isn't decidable either. This really sucks.
> same x x = 1; // is much easier to write and read than:
> same x y = 1 if x===y;
Seriously, how often do you write stuff like that, outside of computer
algebra? It's just a minor notational convenience. If it didn't have any
drawbacks I'd have implemented it long ago, but unfortunately this is
not the case.