## Contents

Front Page

Main:

Concatenative languages:

Interesting languages:

Computer science:

External:

Meta:

# 5th

5th was a typed concatenative programing language in development by John Nowak.

For those interested in the type system, it was basically just a mildly augmented Hindley-Milner. Functions were always unary. Stacks were represented as nested pairs with a kind restriction such that pairs were always left-nested and functions were always from stacks to stacks.

``` kind  = *
| stack
*     = integer           -- types of values
| boolean
| [stack -> stack]  -- quotations
stack = 0                 -- the empty stack
| stack *           -- juxtaposition denotes "cons"```

Example types:

``` swap   : forall (s : stack) (a b : *), s a b -> s b a
apply  : forall (s t : stack), s [s -> t] -> t
apply1 : forall (s : stack) (a b : *), s a [0 a -> 0 b] -> s b
map    : forall (s : stack) (a b : *), s (list a) [0 a -> 0 b] -> s (list b)
each   : forall (s : stack) (a : *), s (list a) [s a -> s] -> s```

For algebraic data types, I generated eliminators. For example, declaring the usual 'list' data type would get you the following constructors and eliminator:

``` null   : forall (s : stack) (a : *), s -> s (list a)
cons   : forall (s : stack) (a : *), s a (list a) -> s (list a)
unlist : forall (s t : stack) (a : *),
s (list a) [s -> t] [s a (list a) -> t] -> t```

You could use these to write familiar functions:

``` sum : forall (s : stack) (a : *), s (list a) -> s integer
sum =  [nip sum 1 +] unlist```

I should note that, because you're often recursing on a stack of a different size, you probably want to support polymorphic recursion. Without it, the type system will force you to stick to strictly iterative functions. A conservative rule would just be to require a type signature on all recursive functions (as inference for polymorphic recursion is an undecidable problem).

This revision created on Wed, 7 Dec 2011 05:14:18 by johnnowak