From: Mark van Gulik [mailto:ghoul6@...]

>From: wtanksley@...

>on the stack as its result, I'm fairly confident we can express the
>program's evaluation strictly in terms of a finite list of
>rewriting rules.

Again, I'm going to have to study your comments. They seem fatally flawed
right now, but perhaps my own knowledge of the subject is blocking me from
seeing the truth in what you're saying.

>On a mostly unrelated topic, I was considering how much
>expressive power was
>lost by Joy's lack of support for lexical closures.

Snicker. Lexical closures? You mean, "total lack of variables"? I'm
sorry, but there's ZERO possibility for lexical closures when there are zero
variables.

>Sure,
>locally bound
>variables and arguments can be bisimulated by finite stack
>manipulations,
>but are lexically closed variables also possible (the question
>of software
>re-use being my motivating concern)?

You're unmistakably trapped in the lambda-fallacy: thinking that everything
is a variant of the lambda calculus. Not every good thing in computer
science comes from the lambda calculus. Joy, for example, is COMPLETELY
unrelated to lambda; Forth is nearly so.

Code reuse is FAR easier when you do _not_ have variables, lexically closed
or otherwise.

>A simple scheme (no pun intended) to support closures would be
>to simply
>implement a closed function as a pair of things -- the function and an
>aggregate of lexically closed variables.

Think about this, though; you're binding variables to functions. This
completely destroys the concept of "concatenative" and replaces it with
"applicative". _Every_ other language in the world is applicative; it's not
a hard problem to solve anymore. I'm interested in solving the problems of
concatenative languages, not in making yet another new applicative one, as
though THIS one would suddenly behave differently from all other other ones
before it.

>Every time a closure
>is needed,
>this pair of things would be used. To invoke the closure,
>simply push the
>aggregate of closed variables onto the stack (as an aggregate)
>and invoke
>the function, which is written to expect this aggregate to be
>on the top.

Forth's local variables work this way -- take a look at them. Some people
use them; I personally see no use for them.

>Closure provides enough power to easily support polymorphism,
>which in turn
>is strong enough to host object-oriented programming. I'm
>*not* saying Joy
>is object-oriented, I'm just saying an object-oriented
>language can be built
>fairly easily and efficiently on top of it.

You seem to believe that OO requires variables, which is simply wrong. I'm
also highly confused by your association of polymorphism with closures; just
because the PROBLEM of polymorphism with closures has been solved doesn't
mean that closures SUPPORT polymorphism; in fact, polymorphism has to be
forced onto closures.

And you then act as though OOP required a huge stack of things. There are
many OOP packages in Forth which add nothing to the language, but provide
full polymorphism.

Now, I happen to like static typechecking with full polymorphism. The right
way to do this isn't to borrow all of the problems of another language in
hopes of being allowed to use their solution; the right way is to develop a
way to statically typecheck a concatenative language. It just so happens
that someone's finally worked that out.

It turns out to be terrifically simple. Every type is given an ID number,
and every "word" (that is, a function with a name) is given a type signature
denoting what its inputs and outputs are (for example, "+" might have one
variant which looks like "( int int -- int )", and "swap" would look like
"(single single -- 2nd 1st)"). User-defined words are required to begin
with a written typesignature.

At compile-time, we have an extra stack, called the type-stack. When we
start compiling a word, we push the types of the inputs onto the typestack;
for each word in the definition, we check that the input of that word is
compatible with the items on top of the typestack, then we remove the input
type-items and replace them with the output ones.

That's the simple version which only does non-polymorphic typechecking.
However, I'm sure you see that polymorphism only requires us to have a type
tree; then we report whether the given types are compatible (instead of
simply checking that they're equal). Going a step further, we can trivially
add overloading; but when we do that we see that unless we do a complete
tree search we might not get the correct word.

So we take that extra step, and use ML-style type inferencing. Now that
we've done this, we can also do things that most other languages can't, such
as overloading on the return values as well as the input values. (We can
even overload on the _number_ of return values, which is something that a
non-concatenative language simply can't do).

Taking a closer look at what we've built, we see that we're typechecking not
_variables_, but rather _dataflow_. In other words, even our simplest
typecheck is doing a partial dataflow analysis, a problem which causes
compiler writers for applicative languages major headaches. How far are we
from a complete dataflow analysis?

-Billy

wtanksley@... wrote:

> [...]
> Now, I happen to like static typechecking with full polymorphism. The right
> way to do this isn't to borrow all of the problems of another language in
> hopes of being allowed to use their solution; the right way is to develop a
> way to statically typecheck a concatenative language. It just so happens
> that someone's finally worked that out.
>
> It turns out to be terrifically simple. Every type is given an ID number,
> and every "word" (that is, a function with a name) is given a type signature
> denoting what its inputs and outputs are (for example, "+" might have one
> variant which looks like "( int int -- int )", and "swap" would look like
> "(single single -- 2nd 1st)"). User-defined words are required to begin
> with a written typesignature.
>
> At compile-time, we have an extra stack, called the type-stack. When we
> start compiling a word, we push the types of the inputs onto the typestack;
> for each word in the definition, we check that the input of that word is
> compatible with the items on top of the typestack, then we remove the input
> type-items and replace them with the output ones.

Well said Bill. The first time I saw type checking with a stack was in a paper
by Stoddart and Knaggs [1], about type inference in Forth programs, and I was
surprised from the simplicity of this method. But they use type variables for
polymorphic words.

> That's the simple version which only does non-polymorphic typechecking.
> However, I'm sure you see that polymorphism only requires us to have a type
> tree; then we report whether the given types are compatible (instead of
> simply checking that they're equal). Going a step further, we can trivially
> add overloading; but when we do that we see that unless we do a complete
> tree search we might not get the correct word.

mmm .. can you expand on this? I'm not so smart ... :o) I am thinking how
eliminate type variables since some time with scarce results.

> So we take that extra step, and use ML-style type inferencing.

Yes, an hypothetical Forth or Joy system with type inference is very interesting:
the system immediately give out the inferred type signature for every definition
or expression (like at the top-level interpreter of functional languages like ML
or Haskell).

> Now that we've done this, we can also do things that most other languages can't,
> such as overloading on the return values as well as the input values. (We can
> even overload on the _number_ of return values, which is something that a
> non-concatenative language simply can't do).
>
> Taking a closer look at what we've built, we see that we're typechecking not
> _variables_, but rather _dataflow_. In other words, even our simplest
> typecheck is doing a partial dataflow analysis, a problem which causes
> compiler writers for applicative languages major headaches. How far are we
> from a complete dataflow analysis?
>
> -Billy

P.S.: As usually, sorry for my bad English.

References

[1] Bill Stoddart and Peter J. Knaggs. Type Inference in Stack Based Languages.
Formal Aspects of Computing, 5(4):289--298, 1993.
http://dec.bournemouth.ac.uk/dec_ind/pknaggs/papers/fac-type.ps.gz

--
Massimo Dentico

From: peter_easthope@...

>> ... lexical closures ...

>Someone please explain what a lexical closure is.

Good question -- thanks for asking.

"A lexical closure is a function which when invoked executes the body of the
lambda-expression in the lexical environment within which the closure was
created." (Quotation from the LISP FAQ.)

In other words, a 'closure' is a function which has variables defined for
use inside it. A lexical closure is a function which has variables defined
by syntax outside of the function itself.

Consider the following:

MODULE myPrinter:
int line = 0
def display(text):
line = line+1
print line, ": ", text
END myPrinter;

IMPORT myPrinter.display as disp;

Okay? Now "disp" is the name of a closure. It has access to, and modifies,
a variable outside of itself. "disp" is a lexical closure because the
definition of disp followed lexical rules: that is, "line" was defined
correctly at the time it was used.

Now, lexical closures are irrelevant for Joy, because closures require
variables, and Joy doesn't have variables.

Joy can have objects; a list of values would serve acceptably as an object,
although no typechecking would be possible (in Joy). Lexical closures are
not essential to OO; they can, however, be used to implement encapsulation,
which is a useful tool commonly used in OO.

>Thanks, Peter E.

-Billy

RE: [stack] Re: Joy as tree rewriting

wtanksley@bigfoot.com — 2000-05-22 17:22:05

Massimo Dentico — 2000-05-23 17:11:17

wtanksley@bigfoot.com — 2000-05-22 22:00:54