Re: [stack] sweetening concatenative syntax

On Mar 7, 2008, at 4:45 PM, William Tanksley, Jr wrote:

> John Nowak <[email protected]> wrote:
>
>> William Tanksley, Jr wrote:
>>
>>
>>> Well, technically if your typesystem was "concatenative" you could
>>> factor it out.
>>
>> This is true. The original type system I had was concatenative (well,
>> really "compositional" is the correct term).
>
> Why? I'm going to start pushing back hard on this.

Ah, I should be more careful here. This has nothing to do with the  
concatenative versus compositional discussion from awhile back. I use  
the word "compositional" as it already has an established meaning with  
respect to type systems. (See http://www.cs.ioc.ee/~ando/publications/cats06.pdf 
  for one example). Compositional also implies that that we're talking  
about a language where programs are expressed in terms of the  
associative operation of composition. This isn't necessarily the case  
with all concatenative languages. Regardless, my primary insistence on  
the term was due to it already being established. I've no interest in  
calling Joy "compositional" instead of "concatenative" or anything  
like that.

>> Unfortunately, this property gets lost quite quickly as you
>> expand the power of the type system.
>
> Or more accurately, it gets lost when you change the type system and
> inferrer without regard for maintaining associativity.

I'd argue that you need to drop associativity if you want a more  
powerful system.

> I don't mind that, but a nagging question remains: is it possible to
> infer types for a concatenative language?

A Cat-like language without generic type variables does allow a  
compositional type system (even with the addition of first-class  
stacks and parameterized types). The downside is that you can't apply  
a single polymorphic function to arguments of different types. (This  
is often called let polymorphism.) My original system worked as such.  
As I've expanded it, I've had no choice but to drop the compositional  
nature of the system. I should note the current system types all  
functions that the original compositional system did, occasionally  
with more general types, so no expressivity is lost.

Perhaps this isn't answering your question. If not, could you be more  
clear?

>>> If your typesystem isn't concatenative, then the resulting language
>>> is no longer strictly concatenative
>>
>> This all depends on your definition of concatenative.
>
> And on your definition of "language", and "type", and "is". I think
> we've got an excellent definition; let's go forward with it. Or
> propose a new one.

Well, my point is this: If a concatenative language is one where  
concatenation denotes function composition, then the language is still  
concatenative. If a concatenative language also requires that you be  
able to extract any portion of a program and replace it with a name  
that represents that portion, then no, it wouldn't be concatenative.  
For example, if 'a b c d e' must be equivalent to 'a f e' where 'f ==  
b c d', then it isn't concatenative.

There may be a solution to this. Functions could be annotated to  
indicate that it is okay if they fail to type check in certain ways.  
When they are used in another function, the body of the first function  
would be substituted in directly and would make use of the additional  
contextual information. This would allow you to write a function like  
'm = dup i' provided that it produces a valid type in the contexts in  
which it is used. Of course you could always just do this with the  
macro system as well, so it isn't clear that there's an additional  
need for such annotations in practice.

Perhaps the system could be smart enough to detect that a function  
that fails to check could be checked if more information were given  
and then would appropriately delay checking. This isn't such a weird  
idea: ML does something similar with overloaded operators, albeit in a  
more limited form. It isn't clear that this is worth the additional  
complexity however (especially as macros can be used to compensate),  
or that it would be able to cover all cases, or even that the cases it  
could cover would be useful functions you'd want to have anyway.

If you really want to preserve the simplicity of Joy and its  
compositional nature, and yet also get some of the benefits of static  
typing, I have a strong suspicion that you'll need a soft type system.  
Of course, practical soft type systems introduce entirely new levels  
of complexity...

- John