Argument count of lambdas
Albert Graef
matter what the actual number of arguments is:
> bar = \x y -> x*y;
> nargs bar;
1
> nargs (bar x);
1
[1] see http://pure-lang.googlecode.com/svn/docs/purelib.html#inspection
The rationale behind this is that \x y -> x*y is considered equivalent
to \x -> \y -> x*y, so the outer lambda is indeed a one-argument
function (which returns another one-argument function as its result).
So this makes sense in a way, but it might still be a bit surprising,
because it's different from explicitly defined functions:
> bar x y = x*y;
> nargs bar;
2
So it might also make sense to have 'nargs (\x y -> x*y)' return 2. This
is at odds with the above equivalence, though. I'm not sure what the
Right Thing is here. Opinions?
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
max.wolf
I vote for nargs = 2 in both cases.
a)
i dont see how calling a functions that returns always 1 can be
useful
b)
The current implementation seems inconsistent to me.
Both versions can be called in a curried form.
Why doesnt the rational you gave for the closure not apply to the
function?
Regards,
Max
John Cowan
> The current implementation seems inconsistent to me. Both versions
> can be called in a curried form. Why doesnt the rational you gave
> for the closure not apply to the function?
--
He made the Legislature meet at one-horse John Cowan
tank-towns out in the alfalfa belt, so that co...@ccil.org
hardly nobody could get there and most of http://www.ccil.org/~cowan
the leaders would stay home and let him go --H.L. Mencken's
to work and do things as he pleased. Declaration of Independence
Albert Graef
> The current implementation seems inconsistent to me.
> Both versions can be called in a curried form.
to return 1 for each and every function that takes more than zero
arguments, because in a language with curried function applications
there are in fact no multiple-argument functions at the semantic level.)
What 'nargs' reports is a purely syntactical attribute, namely the
number of arguments in the *definition* of a function. Consider the
following example:
foo x = f with f y = x*y end;
functions which, given two arguments a and b, compute the product a*b.
But 'nargs foo' is 1, while 'nargs bar' is 2.
In the case of lambdas, there is no explicit definition (that's the
point of a lambda after all). But Pure considers a single-argument
lambda \x -> y as equivalent to 'f with f x = y end' (where 'f' is a new
function symbol different from all other symbols in your program), which
of course implies that 'nargs (\x -> y) == 1'.
Thus it all boils down to how multi-argument lambdas like '\x1 ... xn ->
y' are handled. Right now these are just syntactic sugar for nested
lambdas '\x1 -> ... -> \xn -> y' in Pure. This is in line with classical
lambda calculus and also simplifies the job of the compiler, but of
course it implies that the 'nargs' value of any lambda is always 1.
E.g., 'nargs (\x y -> x*y) == nargs (\x -> \y -> x*y) == nargs (f with f
x = g with g y = x*y end end) == 1'.
That's not the only way to do it. One might also consider '\x1 ... xn ->
y' as equivalent to 'f with f x1 ... xn = y end', which is in effect
what Haskell does. Then we'd have 'nargs (\x1 ... xn -> y) == n'. But
note that this isn't quite the same as the previous definition.
Specifically, '\x x -> x*x' is ok in classical lambda calculus (it's
just the same as '\y x -> x*x'), whereas it has to be rejected because
of the non-linearity if the second interpretation is used. (One might
argue that this is a rather useless corner case, though.)
Libor
if the role of nargs is understood to be to give the maximum number of
arguments that can
be supplied without getting a mismatch error, then the moment you
allow your
"syntactic sugar" of multiple argument lambdas, this seems to argue
for answer= 2 in your original example. In other words, I agree with
Max and John, though for somewhat more prosaic reasons.
Libor
max.wolf
and so was I.
But
1
For Albert it is obvious that nargs foo == 1.
So i change my vote and suggest:
- leave nargs as is
- provide a "maxargs" functions.
Max
Albert Graef
> But
>> foo x = f with f y = x*y end;
>> nargs foo;
> 1
> For Albert it is obvious that nargs foo == 1.
first-class functions gives you a *lot* of freedom. E.g., nothing keeps
you from defining "variadic" functions like the following in Pure:
> foo 1 x = f with f y = x*y end;
> foo 2 x = g with g y z = x*y/z end;
> foo 1 a b;
a*b
> foo 2 a b c;
a*b/c
There's no definite "real" argument count here; it's determined on the
fly. As Pure is Turing-complete, this means that in general your
suggested 'maxargs' function wouldn't even be computable. (The only way
to figure out how many arguments a given function might digest in the
end is to actually run the function.)
Libor
So, I understand now that nargs just syntactically counts the
arguments on the lhs of a rule
(and the compiler gives an error for rules with different nos. of
arguments on the lhs).
So, as it is just a matter of how the lhs was written, perhaps it is
not necessary to emphasise the underlying equivalence of n-arg lambdas
to 1-arg lambda? My guess is that lambda calculus afficinados will
know about it and others will prefer the syntactical consistency of
nargs giving n for n-arg lambda if that is how it was written.
Libor
Albert Graef
> So, I understand now that nargs just syntactically counts the
> arguments on the lhs of a rule
> (and the compiler gives an error for rules with different nos. of
> arguments on the lhs).
Yes, exactly.
> So, as it is just a matter of how the lhs was written, perhaps it is
> not necessary to emphasise the underlying equivalence of n-arg lambdas
> to 1-arg lambda? My guess is that lambda calculus afficinados will
> know about it and others will prefer the syntactical consistency of
> nargs giving n for n-arg lambda if that is how it was written.
Right, I'm working on that right now. Once that is done, I'll also
reconsider the left-linearity restriction.
Eddie Rucker
> Right, I'm working on that right now. Once that is done, I'll also
> reconsider the left-linearity restriction.
Albert, I thought left-linearity was written in stone to keep the interpreter fast and lean. Is the change in heart due to
pure *always* producing machine code through LLVM? Does this mean we will be able to write equations like
x*y+x*z = x*(y+z);
as we did in Q?
e.r.
Albert Graef
> On Thu 17/12/09 1:17 AM , Albert Graef Dr.G...@t-online.de sent:
>> Right, I'm working on that right now. Once that is done, I'll also
>> reconsider the left-linearity restriction.
>
> Albert, I thought left-linearity was written in stone to keep the interpreter fast and lean.
Well, quoting myself from a previous thread [1]: "It's a design
decision, and as such open to debate." Debate it we did :), and the
general consensus seemed to be that non-linearities would be nice to
have. I also mentioned that this wouldn't be difficult to implement; it
doesn't really make the interpreter much fatter, I'm more concerned with
the "hidden magic" issue here, see below.
[1]
http://groups.google.com/group/pure-lang/browse_thread/thread/d8bd796a11fb49b0
One of my objections was that non-linearities would cause confusion
because of the way that lambdas were handled. That is fixed now (as of
r2821) so that we have proper multi-argument lambdas which are given the
same treatment as named functions when it comes to non-linearities. I
must say that I'm quite happy with that; it seems to be the Right Thing
after all.
My other objection was the hidden inefficiencies (and even potential
nontermination issues, with lazy data) in non-linearities. (Note that
this isn't about the efficiency of the interpreter or generated code,
it's about the ease with which the programmer himself can write horribly
inefficient Pure programs.) That argument (as well as the
'non-linearities as typos' issue) still holds, but I have to weigh it
against the added convenience of non-linear definitions and Pure's
general "laissez fair" attitude when it comes to enabling the programmer
to blow his leg off. ;-)
I also mentioned a few theoretical difficulties (mostly related to
modularity of term rewriting w.r.t. confluence and termination
properties), but these aren't really that important in Pure because of
the deterministic reduction strategy.
Note that the main objection against non-linearities in *Haskell* (and
other H/M-typed languages), namely that Haskell doesn't have a notion of
syntactic equality of terms (instead, a non-linear variable would have
to be an instance of the Eq class, over which the compiler has no
semantic control), isn't an issue with Pure, as syntactic equality is
always defined and has a clear semantics.
So I'm willing to give it a go now; I can always add a paragraph about
the pitfalls of non-linearity to the "Caveats and Notes" section later.
> Does this mean we will be able to write equations like
>
> x*y+x*z = x*(y+z);
>
> as we did in Q?
Yup, that's what it's all about. And yes, it *is* convenient, especially
when doing computer algebra.
Cheers,
Albert
John Cowan
> My other objection was the hidden inefficiencies (and even potential
> nontermination issues, with lazy data) in non-linearities. (Note that
> this isn't about the efficiency of the interpreter or generated code,
> it's about the ease with which the programmer himself can write horribly
> inefficient Pure programs.) That argument (as well as the
> 'non-linearities as typos' issue) still holds, but I have to weigh it
> against the added convenience of non-linear definitions and Pure's
> general "laissez fair" attitude when it comes to enabling the programmer
> to blow his leg off. ;-)
I think, especially given the typo concern, that it would be appropriate
to print a warning when encountering a nonlinear rule. (There needs to
be a command to silence such warnings, of course.)
> I also mentioned a few theoretical difficulties (mostly related to
> modularity of term rewriting w.r.t. confluence and termination
> properties), but these aren't really that important in Pure because of
> the deterministic reduction strategy.
True. Still, it's easier to reason about complex Pure functions if
you can easily write disjoint rules and don't have to depend on the
source-code order.
--
John Cowan co...@ccil.org http://ccil.org/~cowan
Objective consideration of contemporary phenomena compel the conclusion
that optimum or inadequate performance in the trend of competitive
activities exhibits no tendency to be commensurate with innate capacity,
but that a considerable element of the unpredictable must invariably be
taken into account. --Ecclesiastes 9:11, Orwell/Brown version
Eddie Rucker
> One of my objections was that non-linearities would cause confusion
> because of the way that lambdas were handled. That is fixed now (as of
> r2821) so that we have proper multi-argument lambdas which are given
> the same treatment as named functions when it comes to non-linearities. I
> must say that I'm quite happy with that; it seems to be the Right Thing
> after all.
That's nice to hear.
e.r.
Eddie
On Dec 18, 8:57 am, John Cowan <co...@ccil.org> wrote:
> I think, especially given the typo concern, that it would be appropriate
> to print a warning when encountering a nonlinear rule. (There needs to
> be a command to silence such warnings, of course.)
Yea, I think John has the right idea.
e.r.
Libor
I think with some examples of the code to be avoided,
this will be great.
Libor
Albert Graef
> I think, especially given the typo concern, that it would be appropriate
> to print a warning when encountering a nonlinear rule. (There needs to
> be a command to silence such warnings, of course.)
Well, it doesn't make much sense to me to add a language feature and
then warn about its uses by default; that's just annoying. I could maybe
add a pragma (off by default) which could selectively be turned on in
the source, though.
> True. Still, it's easier to reason about complex Pure functions if
> you can easily write disjoint rules and don't have to depend on the
> source-code order.
Right, but IMHO that's a question of programmer discipline. If you want
real equational logic semantics then you'll just have to stick to
confluent and terminating rewriting systems. The Pure compiler doesn't
keep you from writing your definitions that way, but it won't force you
to do it either.
John Cowan
> Well, it doesn't make much sense to me to add a language feature and
> then warn about its uses by default; that's just annoying.
That sounds like a matter of timing. Suppose the feature had been there
all the time (as in Q) and you had had complaints: "Hey, my foot is half
shot off here". Adding a warning would make sense then, hmmm? So I'm
just suggesting that you preempt that.
When current behavior makes something an error, people unconsciously rely
on the error being reported to protect them against making it. Extending
the system to make the behavior do something unusual takes away that
security blanket. (This is why you can't subset a programming language
by just teaching people part of it; inevitably they write something that
happens to be a feature of the full language, and then they can't debug
their programs. Such people need computer assistance in the form of a
precompiler or linter.)
> Right, but IMHO that's a question of programmer discipline.
If you want C, you know where to find it. :-)
> If you want real equational logic semantics then you'll just have
> to stick to confluent and terminating rewriting systems. The Pure
> compiler doesn't keep you from writing your definitions that way,
> but it won't force you to do it either.
"The task is not yours to complete, but neither are you free to desist
from it." --Rabbi Tarfon, 1st century C.E.
--
My corporate data's a mess! John Cowan
It's all semi-structured, no less. http://www.ccil.org/~cowan
But I'll be carefree co...@ccil.org
Using XSLT
On an XML DBMS.
Albert Graef
> That sounds like a matter of timing. Suppose the feature had been there
> all the time (as in Q) and you had had complaints: "Hey, my foot is half
> shot off here". Adding a warning would make sense then, hmmm? So I'm
> just suggesting that you preempt that.
I can see your point, but I prefer to wait until the complaints roll in.
I really don't like the idea to warn about legal code if there's no way
to actually detect the dubious cases. (However, the compiler does an
occurrence check to throw out "as" variables repeated in the
corresponding subpatterns (such as xs@(x:xs)), since these can't
possibly yield finite matches anyway.)
Support for non-linearities is implemented as of r2834. So if you're
running the latest svn, rules like the following will do the right thing
now:
a*c+b*c = (a+b)*c;
a*b+a*c = a*(b+c);
The same applies to repeated variables in the lhs of lambdas, case, when
and let/const, of course. I didn't test these heavily yet, so please
consider this experimental and report any bugs that you find. I hope
that I can release this as Pure 0.40 before xmas.