5th5th 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 HindleyMilner. Functions were always unary. Stacks were represented as nested pairs with a kind restriction such that pairs were always leftnested and functions were always from stacks to stacks. kind = *  stack * = integer  types of values  boolean  [stack > stack]  quotations  {stack}  firstclass stacks 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 = [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:15:15 by johnnowak 

All content is © 20082010 by its respective authors. By adding content to this wiki, you agree to release it under the BSD license. 