Front Page All Articles Recent Changes Random Article

Contents

Concatenative language

  • ACL
  • Ait
  • Aocla
  • Breeze
  • Callisto
  • Cat
  • Cognate
  • colorForth
  • Concata
  • CoSy
  • Deque
  • DSSP
  • dt
  • Elymas
  • Enchilada
  • ETAC
  • F
  • Factor
  • Fiveth
  • Forth
  • Fourth
  • Freelang
  • Gershwin
  • hex
  • iNet
  • Joy
  • Joy of Postfix App
  • kcats
  • Kitten
  • lang5
  • Listack
  • LSE64
  • Lviv
  • Meow5
  • min
  • Mirth
  • mjoy
  • Mlatu
  • Ode
  • OForth
  • Om
  • Onyx
  • Plorth
  • Popr
  • Porth
  • PostScript
  • Prowl
  • Quest32
  • Quackery
  • r3
  • Raven
  • Retro
  • RPL
  • SPL
  • Staapl
  • Stabel
  • Tal
  • Titan
  • Trith
  • Uiua
  • Worst
  • xs
  • XY
  • 5th
  • 8th

Concatenative topics

  • Compilers
  • Interpreters
  • Type systems
  • Object systems
  • Quotations
  • Variables
  • Garbage collection
  • Example programs

Concatenative meta

  • People
  • Communities

Other languages

  • APL
  • C++
  • Erlang
  • FP trivia
  • Haskell
  • Io
  • Java
  • JavaScript
  • Lisp
  • ML
  • Oberon
  • RPL
  • Self
  • Slate
  • Smalltalk

Meta

  • Search
  • Farkup wiki format
  • Etiquette
  • Sandbox

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}           -- 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

Latest Revisions Edit

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