- ACL
- Ait
- Aocla
- Breeze
- Cat
- Cognate
- colorForth
- CoSy
- Deque
- DSSP
- Elymas
- Enchilada
- ETAC
- F
- Factor
- Forth
- Freelang
- Gershwin
- Joy
- Kitten
- lang5
- Lviv
- min
- mjoy
- Mlatu
- Ode
- Om
- Onyx
- Plorth
- Popr
- Porth
- PostScript
- Quackery
- r3
- Raven
- Retro
- Staapl
- Stabel
- Trith
- Worst
- xs
- XY
- 5th
- 8th

Other languages

Computer Science

Meta

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} -- first-class stacks stack = 0 -- the empty stack | stack * -- juxtaposition denotes "cons"

Example types:

swap : forall (s : stack) (a b : *), s a b -> s b a drop : forall (s : stack) (a : *), s a -> s 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 empty : forall (s : stack), s -> s {0} push : forall (s t : stack) (a : *), s a {t} -> s {t a} pop : forall (s t : stack) (a : *), s {t a} -> s a {t} infra : forall (s t u : stack), s {t} [t -> u] -> s {u}

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), s (list integer) -> s integer sum = [0] [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:25:34 by johnnowak
*