cicada-lang/inet-cute

An implementation of interaction nets. -- ASCII art inspired syntax. -- Pure postfix expression. -- Using a stack-based low-layer language to build nets.

iNet Cute

[ Website | iNet JS ]

An implementation of interaction nets.

• ASCII art inspired syntax.
• Pure postfix expression.
• Using a stack-based low-layer language to build nets.

Usage

Command line tool

Install it by the following command:

npm install --global @cicada-lang/inet-cute

The command-line program is called inet-cute.

inet-cute repl         # Open an interactive REPL
inet-cute run [path]   # Run an inet program
inet-cute help [name]  # Display help for a command

Examples

Please see tests/ for some example code.

Nat

type Nat -- @Type end

node zero
  ------------
  Nat :value!
end

node add1
  Nat :prev
  ------------
  Nat :value!
end

node add
  Nat :target!
  Nat :addend
  ------------
  Nat :result
end

rule zero add
  (add)-addend
  result-(add)
end

rule add1 add
  (add)-addend
  (add1)-prev add
  add1 result-(add)
end

claim one -- Nat end
define one zero add1 end

claim two -- Nat end
define two one one add end

claim three -- Nat end
define three two one add end

claim four -- Nat end
define four two two add end

two two add
two two add @run $result

List

type List @Type -- @Type end

node null
  --------
  'A List :value!
end

node cons
  'A :head
  'A List :tail
  --------
  'A List :value!
end

node append
  'A List :target!
  'A List :rest
  --------
  'A List :result
end

rule null append
  (append)-rest
  result-(append)
end

rule cons append
  (append)-rest (cons)-tail append
  (cons)-head cons
  result-(append)
end

import zero from "https://code-of-inet-cute.fidb.app/tests/datatype/Nat.i"

null zero cons zero cons
null zero cons zero cons
append

null zero cons zero cons
null zero cons zero cons
append @run $result

DiffList

import List from "https://code-of-inet-cute.fidb.app/tests/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 @Type -- @Type end

node diff
  'A List :front
  -------
  'A List :back
  'A DiffList :value!
end

node diffAppend
  'A DiffList :target!
  'A DiffList :rest
  --------
  'A DiffList :result
end

node diffOpen
  'A DiffList :target!
  'A List :newBack
  ----------
  'A List :oldBack
end

rule diff diffAppend
  (diff)-front diff result-(diffAppend)
  (diffAppend)-rest diffOpen back-(diff)
end

rule diff diffOpen
  (diff)-back newBack-(diffOpen)
  (diff)-front oldBack-(diffOpen)
end

import zero from "https://code-of-inet-cute.fidb.app/tests/datatype/Nat.i"
import cons from "https://code-of-inet-cute.fidb.app/tests/datatype/List.i"

(diff) @spread $front $back $value
back zero cons zero cons front @connect value
(diff) @spread $front $back $value
back zero cons zero cons front @connect value
diffAppend

// By using one less local variable `$value`,
// we can simplify the above code:

(diff) @spread $front $back
back zero cons zero cons front @connect
(diff) @spread $front $back
back zero cons zero cons front @connect
diffAppend

// By using one less local variable `$back`,
// we can further simplify the above code:

(diff) @spread $front zero cons zero cons front @connect
(diff) @spread $front zero cons zero cons front @connect
diffAppend

@run $result

Development

npm install          # Install dependencies
npm run build        # Compile `src/` to `lib/`
npm run build:watch  # Watch the compilation
npm run test         # Run test

References

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.

Contributions

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.

License

GPLv3

inet-cute's Issues

Can't use let binding in expression twice?

Hi, thanks for creating this project!

I'm running into an error in code that, as far as I can tell, should work.

(define-cons thing 0)

(define-cons nil 0)
(define-cons cons 2)

(define-elim double 1)
(define-rule (nil double) nil)
(define-rule (cons double) (let head) double head cons head cons)

(define-net doubled-list
  nil thing cons thing cons thing cons thing cons double)

I'm trying to write code to double the length of a list.

However I'm getting the error Undefined name: head, which doesn't make much sense to me, since

1. I've defined head
2. If I use head only once in the expression it works fine

Is there some kind of linear typing at work here, where you can't use a let binding more than once in the rewritten graph? Or is this a compiler error?