Re: [stack] Re: Concatenative Research

On Feb 1, 2011, at 9:22 PM, Justin wrote:

> --- In [email protected], John Nowak <john@...> wrote:
> 
>> - juxtaposition is just function composition
>> - all functions operate on lists (e.g. dup = \s@(x:_) -> x:s)
>> - quotation of 'f' is just '(:) f'
> 
> Except that you have not dealt with runtime exceptions (e.g. stack underflow) or program non-termination.

Sure, but there's no reason any special work needs to be done for concatenative languages, is there? Concatenative languages have the same bottom-preserving semantics any partial higher-order language with eager evaluation and lambda abstractions would have.

I guess my point is that you can see concatenative languages as "just" your usual higher-order eager language with a different syntax for composition and lambda abstraction (e.g. '[f g] == (:) (\s -> (g . f) s)', with the eta-expansion there to delay evaluation). Since the difference is simply syntax, I'm not sure why the semantics would require special treatment.

I should mention that I assume quotations form a proper opaque abstraction (as in lambda calculus) and are not dissectible (as in Joy). My above semantics for quotation doesn't work for Joy and instead describing the semantics for 'i' would be the interesting part. I've been on the record many times now though as saying those semantics are undesirable for a programming language; the ability to form new abstractions is critical.

>> Typing a concatenative language is straightforward. You introduce a new kind 'Stack_K' and an inductively-defined type 'Stack' of kind 'Stack_K' that's either 'Empty' or a 'Cons' of a value with kind '*' and another 'Stack'. Your arrow constructor then has kind 'Stack_K -> Stack_K -> *' and quotation is kinded '* -> *' with type 'forall a b (c :: Stack_K). (a -> b) -> c -> Cons (a -> b) c'.
> 
> Aha, that is a good way of looking at it. Have you written anything along these lines? I would be interested in reading it.

I've not, although I probably should before someone else does! Then again, there are only about 3 people interested in this problem...

> My type system also has polymorphic data types (not too unusual), and what I'll call "cyclic types". A cyclic type is one that violates the occurs check and refers to itself. For instance, the correct type of 'dup apply' is
>  (A x -> B), with x = (A x -> B)
> Notice that x occurs in its own definition.

I think the cyclic types you're proposing, commonly called "equirecursive types", are unnecessary. The 'dup apply' combinator is basically equivalent to the 'm' combinator in lambda calculus (i.e. '\x -> x x'). This is ill-typed in most typed systems. O'Caml will permit it with the "-rectypes" flag (which enables equirecursive types), but that flag is disabled by default and for good reason: It adds little utility and makes for some ugly type errors.

> Christopher Diggin's type system for Cat is actually very close to this, but it doesn't admit polymorphic types (as far as I'm aware), and I don't think it handles cyclic types correctly.

I'm not sure that Diggins has a sound system. As you've discovered, it returns some strange results.

If you're interested in typing combinators like 'dup apply', I think intersection types are a more interesting approach:

   dup apply : for all a b c d. Cons ((b -> c) /\ (Cons (b -> c) a -> d)) a -> d

If you read that carefully, it should make sense. I believe Slava put the basis of the idea in my head originally. Of course, the problem with this approach is that you now have intersection types to contend with.  Again, for a practical system, I don't think it's worth it.

The last thing I'll point out with respect to the type system is that, due to recursive function calls working on a list that represents the entire program state (and not just its "arguments"), you have quite a lot of polymorphic recursion; any recursive function where the recursive call occurs on a stack that has "grown" is polymorphic recursive. You could try to infer some cases of this (Milner-Mycroft), but the problem is undecidable in general. I think requiring type signatures on many recursive functions would therefore be a requirement. It's not one that I consider particularly onerous however.

- jn