Re: [stack] sweetening concatenative syntax

William Tanksley, Jr wrote:

> That's a cool paper; thank you. However, that's not what the paper
> appears to mean by "compositionality".

Ah, you're right. Maybe that wasn't the paper I was thinking of... scratch
that then.

>>> 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)!

I've hinted at the reasons in previous emails. I'll try and write up
something more detailed soon. I'll take a stab at it briefly below...

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

Perhaps it's just a case of having "strong concatenative" and "weak
concatenative" languages? Different levels of purity are certainly useful
when talking about other paradigms.

> 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 that example, there'd be no way to even create such lists in the first
place without type classes (where Int and Float are instances of some Num
class) or intersection types. You could of course always wrap things up in
a sum (union/variant) type.

Anyway, what I meant is something like this:

   foo = 0 "hi" [pop] dup dip i

Here, the same pop function is applied to both an integer and a string.
Without a notion of generic (aka "free") type variables, this function is
not typeable. This is because the variable in the type of the quotation
(pop :: a -> ) gets instantiated to 'String' for both functions because
the variable in the second function is not free with respect to the first.

Here's the evaluation of the above function on the type level which may help:

   Int                        -- 0
   Int String                 -- "hi"
   Int String [a -> ]         -- [pop]
   Int String [a -> ] [a -> ] -- dup
   Int [String ->]            -- dip

At this point, we'd get a type error when composing 'i' as we can't unify
the types Int and String. Now here's the same thing allowing variables to
be free:

   Int                        -- 0
   Int String                 -- "hi"
   Int String [a -> ]         -- [pop]
   Int String [a -> ] [b -> ] -- dup -- note the difference!
   Int [b ->]                 -- dip
                              -- i

Hopefully that makes some sense. Now, let me briefly explain why the
second system (the one with free type variables) breaks concatenativity
with the function '[swap] dup i'. First, without generic type variables:

   [a b -> b a]               -- [swap]
   [a b -> b a] [a b -> b a]  -- dup

At this point, we get a type error when composing 'i' as we fail an occurs
check. Here's the derivation:

   -- initial composition
   R -> R [S a b -> S b a] [S a b -> S b a]
        T                  [T     -> U    ] -> U

   -- unify 'S b a' and 'U'
   R -> R [S a b -> S b a] [S a b -> S b a]
        T                  [T     -> S b a] -> S b a

   -- unify 'S a b' and 'T'
   R -> R   [S a b -> S b a] [S a b -> S b a]
        S a b                [S a b -> S b a] -> S b a

   -- fail! cannot unify 'b' and '[S a b -> S b a]' due to infinite type

Not sure if that makes any sense. Probably not. I'll explain how to do
these compositions by hand when I eventually write this up. If it does
make sense though, then great.

Now, here's the same thing with generic variables:

   [a b -> b a]               -- [swap]
   [a b -> b a] [c d -> d c]  -- dup -- note the difference!

And here we can compose 'i' properly without running into the occurs
check. Again, here's the derivation:

   -- initial composition
   R -> R [S a b -> S b a] [V c d -> V d c]
        T                  [T     -> U    ] -> U

   -- unify 'V d c' and 'U'
   R -> R [S a b -> S b a] [V c d -> V d c]
        T                  [T     -> V d c] -> V d c

   -- unify 'V c d' and 'T'
   R -> R   [S a b -> S b a] [V c d -> V d c]
        V c d                [V c d -> V d c] -> V d c

   -- unify '[S a b -> S b a]' and 'd' -- oh line wrap...
   R -> R   [S a b -> S b a] [V c [S a b -> S b a] -> V [S a b -> S b a] c]
        V c [S a b -> S b a] [V c [S a b -> S b a] -> V [S a b -> S b a]
c] -> V [S a b -> S b a] c

   -- unify 'R' and 'V c'
   V c -> V c [S a b -> S b a] [V c [S a b -> S b a] -> V [S a b -> S b a] c]
          V c [S a b -> S b a] [V c [S a b -> S b a] -> V [S a b -> S b a]
c] -> V [S a b -> S b a] c

   -- final type
   V c -> V [S a b -> S b a] c

   -- or more nicely
   a -> [b c -> b c] a

Right. So what I've shown is that the system without free type variables
cannot type '[swap] dup i' and the system with free type variables can.
However, neither system can type 'dup i' by itself. In order to type
'[swap] dup i', you need free type variables and you *must* compose types
left to right in order to gather the necessary constraints. Hence, the
system is not purely concatenative.

Languages like ML and Haskell work exactly the same way. For example, this
is untypeable in Haskell:

   \x -> x x

However, this is fine as we're letting it know what the type of 'x' is:

   let x = flip in x x

There are ways to lift such restrictions. One is equi-recursive types,
although all you tend to get out of this is are valid types that you can't
do much with (and hence the system will still not be purely
concatenative). The other is to allow rank-n polymorphism. Unfortunately,
systems with rank-n polymorphism are undecidable and require type
annotations for all higher rank functions (except perhaps rank-2 depending
on your particular system). This is something I'd like to tackle
eventually but will not be dealing with in earlier versions of the
language.

- John