Re: [stack] rewriting + second order vs. higher order expressivity

On Jun 19, 2008, at 9:27 AM, William Tanksley, Jr wrote:

> John Nowak <[email protected]> wrote:
>
>> I'm not really sure what I'm asking here. Perhaps I'm just looking  
>> for
>> a gut response to the C2R proposal. If anyone has any thoughts, I'd
>> very much appreciate them. This is the last "big decision" for 5th
>> before I can release something.
>
> Well, you've got my sympathy... That's an unfortunate dilemma. It
> looks like this model of a first-order language works very poorly with
> concatenativity. It this purely a result of this model -- might it be
> possible to partly solve this by other means?
>
> Would it be possible to
> define some kind of pseudofunctional that can be called from inside a
> functional to mean "lift a stack item into here"? My mind is rebelling
> from this, so it's probably a really bad idea. I can't tell.


Such an approach is the only way I can think of to solve the problem.  
Unfortunately, such an approach is also impossible (or, at least,  
requires far too much magic to be worth it). I could give some  
examples that demonstrate this, but you probably already have a good  
intuition for why this can't work.

I should note that a postfix language based on term rewriting is  
actually a very nice thing! I'm not exactly disappointed to be in this  
situation; it's just something of a surprise.

I should also note that allowing the programmer to define things in  
terms of rewrite rules doesn't complicate the language. The reason is  
that you need some notion of substitution in order to make sense of  
the language primitives in the first place.

Being able to work with objects directly also makes proofs possible  
without a ton of function-level axioms. Let's say, for example, that I  
want to prove that the program 'dip(swap)' is equivalent to the  
program '-rot swap rot'. In order to do this, we first need to know  
the semantics of these functions and functionals:

        $a dip($F) = $F $a
        $a $b swap = $b $a
    $a  $b $c -rot = $c $a $b
     $a $b $c rot = $b $c $a

The next step, of course, is to set the programs equal to each other:

    dip(swap) = -rot swap rot

At this point, if we're not allowed to deal with objects, we're stuck  
unless we have some additional set of function-level axioms. However,  
if we're allowed to deal with objects, this is easy. The first thing  
we need to do is employ one of the rules of "concatenative algebra" (I  
need to post something about this eventually) that says we can prepend  
or append any expression to both sides of the equality:

    $a $b $c dip(swap) = $a $b $c -rot swap rot

Now, we just simplify both sides using the rewriting semantics for  
these function(al)s:

    $a $b $c dip(swap) = $a $b $c -rot swap rot
         $a $b swap $c = $a $b $c -rot swap rot
              $b $a $c = $a $b $c -rot swap rot
              $b $a $c = $c $a $b swap rot
              $b $a $c = $c $b $a rot
              $b $a $c = $b $a $c

While Backus does talk much about how FP's pointfree nature makes  
proofs simpler, it's really the second order nature of the language  
that is responsible for most of the easy manipulatability. Of course,  
pointfree manipulations are still possible in many cases even if the  
programmer is allowed to deal with objects directly.

Anyway, I hope that shows that it's beneficial to be able to  
manipulate objects, at least in proofs (if that wasn't already  
obvious). If the language is defined in terms of rewrite rules, I  
don't think it adds much complication to allow programmers to use the  
same system to define new functions and functionals. The only  
unfortunate thing is that you *need* to express programs in terms of  
rewrite rules in some cases to get around the lack of first-class  
functions. That said, I see this neither as a major theoretical issue  
nor a major practical issue.

- John