Re: [stack] sweetening concatenative syntax

John Nowak <[email protected]> wrote:
> William Tanksley, Jr wrote:
>  > John Nowak <[email protected]> wrote:
>  >> William Tanksley, Jr wrote:
>  >> 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.

That's a cool paper; thank you. However, that's not what the paper
appears to mean by "compositionality". Look it up; compositional
appears to refer to the property that a program or statement can be
understood correctly by synthesizing the meaning of its component
phrases. The paper actually claims that the language it's studying is
"non-compositional" due to it not being composed of discrete phrases
-- which means that concatenative languages (by my definition) are
also non-compositional by his definition.

>  >> 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'd love to hear that argument. Go for it (although in a new thread)!
The implication would be that it's impossible to define a
strongly-typed and type-inferenced concatenative language (at least by
my definition).

To me, that implies in turn that my definition of 'concatenative' is
most probably wrong.

>  > 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.

I'm confused by "apply a single polymorphic function to arguments of
different types". Does that refer to, for example, mapping a
polymorphic function to a list containing two values of different
types, either of which is acceptable to the function's polymorphic
type?

So for example, let
[2.0f 2] [2.0f 2] [*] over-each == [4.0f 4].

In other words, it applies a dyadic function to a pair of lists.

I think you're saying that the simple type system can't infer the
types for that code snippet, right? And then you go on to say that
it's impossible to build a type system that can both infer the types,
AND remain associative, right?

>  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.

I would expect more general types to be helpful -- for example, in the
above example I would expect a union type into which both integers and
floats fit.

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

It's confirming my suspicion about what you meant, yes. And BTW, I
don't have any rebuttal or anything like that... I'd like to hear your
argument.

>  >>> 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.

Yes, the latter is an implication of associativity. Note that
concatenation is an associative operation, as is composition.

>  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.

This is exactly what I've been pondering over the last few days. And
yes, the fact that ML is the only type-inferencing language I know has
contributed to those speculations. I don't insist on the type system
performing the inference automatically, although I do think that if we
can't even guess at how it could be done we don't understand the
problem yet.

>  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...

After a brief google, I have to say that I'd rather not back up to a
soft type system quite yet... It may be necessary, but I'd rather
understand the static system first.

Note, by the way, that there's very few languages that can be fully
hard-typed. The only one I know is SPARK Ada, and it's hard to code
in; you have to code proofs in addition to your code. (IMO, a language
is fully hard typed ONLY IF it's possible to write serious programs in
it that don't require a runtime, i.e. exception handling.)

>  - John

-Wm