Re: [stack] Concatenative Research

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'

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

- jn