This is an implementation of interaction nets. It introduces you to the bizarre world of graph-based computation and linear logic, using a familiar JavaScript-like syntax :)
Install it by the following command:
npm install --global @cicada-lang/inet-js
The command-line program is called inet-js
.
inet-js repl # Open an interactive REPL
inet-js run [path] # Run an inet program
inet-js help [name] # Display help for a command
type Nat
node zero(
------
value!: Nat
)
node add1(
prev: Nat
----------
value!: Nat
)
node add(
target!: Nat,
addend: Nat
--------
result: Nat
)
rule add(target!, addend, result) zero(value!) {
@connect(addend, result)
}
rule add(target!, addend, result) add1(prev, value!) {
add1(add(prev, addend), result)
}
function one(): Nat {
return add1(zero())
}
function two(): Nat {
return add(one(), one())
}
function three(): Nat {
return add(two(), one())
}
function four(): Nat {
return add(two(), two())
}
// TEST
eval @inspect(@run(add(two(), two())))
eval @inspect(add(two(), two()))
type List(Element: @Type)
node null(
--------
value!: List('A)
)
node cons(
head: 'A,
tail: List('A)
--------
value!: List('A)
)
node append(
target!: List('A),
rest: List('A)
--------
result: List('A)
)
rule append(target!, rest, result) null(value!) {
@connect(rest, result)
}
rule append(target!, rest, result) cons(head, tail, value!) {
cons(head, append(tail, rest), result)
}
// TEST
type Trivial
node sole(-- value!: Trivial)
function sixSoles(): List(Trivial) {
return append(
cons(sole(), cons(sole(), cons(sole(), null()))),
cons(sole(), cons(sole(), cons(sole(), null()))),
)
}
eval @inspect(@run(sixSoles()))
eval @inspect(sixSoles())
import { List } from "https://code-of-inet-js.xieyuheng.com/docs/std/datatype/List.i"
// Concatenation of lists is performed in linear time
// with respect to its first argument.
// Constant time concatenation is possible
// with difference-lists: the idea consists in
// plugging the front of the second argument
// at the back of the first one.
type DiffList(Element: @Type)
node diff(
front: List('A),
-------
back: List('A),
value!: DiffList('A),
)
node diffAppend(
target!: DiffList('A),
rest: DiffList('A)
--------
result: DiffList('A)
)
node diffOpen(
target!: DiffList('A),
newBack: List('A)
----------
oldBack: List('A)
)
rule diffAppend(target!, rest, result)
diff(front, back, value!) {
let newBack, value = diff(front)
@connect(value, result)
diffOpen(rest, newBack, back)
}
rule diffOpen(target!, newBack, oldBack)
diff(front, back, value!) {
@connect(back, newBack)
@connect(front, oldBack)
}
// TEST
import { cons } from "https://code-of-inet-js.xieyuheng.com/docs/std/datatype/List.i"
type Trivial
node sole(-- value!: Trivial)
function twoTwoSoles(): DiffList(Trivial) {
let front, back, value1 = diff()
@connect(front, cons(sole(), cons(sole(), back)))
let front, back, value2 = diff()
@connect(front, cons(sole(), cons(sole(), back)))
return diffAppend(value1, value2)
}
eval @inspect(@run(twoTwoSoles()))
eval @inspect(twoTwoSoles())
npm install # Install dependencies
npm run build # Compile `src/` to `lib/`
npm run test # Run test
Papers:
- Interaction Nets, Yves Lafont, 1990 (the founding paper).
- Interaction Combinators, Yves Lafont, 1997.
Books:
- Models of Computation -- An Introduction to Computability Theory, Maribel Fernández, 2009.
- Chapter 7. Interaction-Based Models of Computation.
To make a contribution, fork this project and create a pull request.
Please read the STYLE-GUIDE.md before you change the code.
Remember to add yourself to AUTHORS. Your line belongs to you, you can write a little introduction to yourself but not too long.