[stack] Re: Concatenative Research

--- In [email protected], John Nowak <john@...> wrote:
>
> 
> On Jan 30, 2011, at 7:20 PM, Justin wrote:
> 
> > I have a few partial results: (i) an operational semantics,
> 
> The semantics are quite simple, aren't they?
> 
>  - 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.

> > (iii) a type system
> 
> 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.

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.

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. Cat's type inferencer gives the correct type for 'dup apply',
  (A (A self -> B) -> B)

But on the program 'dup dig dup bury true bury if', it gives the type,
  (A (A (self -> B) self -> B) (A self (self -> B) -> B) -> B)
First, there is ambiguity as to which enclosing quotation each 'self' refers to. Second, there seems to be a kind error in the subexpression '(self -> B)'. Like you said, '->' has kind 'Stack_K -> Stack_K -> *'. But 'self' has kind '*', unless I am mistaken. Any thoughts?

The type I get (by hand; it's easy enough to verify) is
  (A (S -> B) (S -> B) -> B, with S = A (S -> B) (S -> B)