disp

abbr.

disp is an aspiring general-purpose programming language with and , and a based on that models hardware as imperfect interaction-net reduction. Based on Barry Jay's tree calculus.

Read the Docs

$ git clone github.com/libdither/disp && npm i && npm test

Why disp?

Because when AGI comes and our code isn't formally verified yet, we're gonna be screwed.

Programs are data are trees

Disp is homoiconic like lisp, except there is no quote/eval border to deal with. Programs can just take other programs as input and use the `triage` reduction rule to inspect them.

Types you can run

A type is a predicate: a function that takes a tree and returns a verdict, and applying it is the type check. You can implement new type theories by just writing new functions, and you don't have to think about type systems in terms of confusing sequent calculus diagrams, they're just programs.

You should be able to just define the parser

I've never understood why programming languages don't just allow you to entirely replace the parser. Well, I guess lisp and some ML languages (Haskell, Agda) allows you to do this kinda but not super well or not completely. Disp doesn't have this feature yet, but its pretty much just a matter of time at this point. The goal is to be able to literally change syntax or program representation with a simple dropdown menu. Users can make their own by defining a parser |- pretty-printer adjoint functor pair.

Optimize ZA WARUDO (with a self-optimizing optimizer)

Idea: have tree programs compile to interaction nets, and have another interaction net search the original interaction nets to find-and-replace certain nets with native operations. Possibly using e-graphs. Then buy a dedicated hyper-parallel chip that basically runs a cellular automata specialized to simulate agent reduction where agents are connected by other agents through the physical space of the chip and reduce at a billion parallel reductions per second or something.

Examples

Click open in playground to check them out!

▶ Open in playground

// Below the type system: the tree calculus itself. Five rewrite rules over
// binary trees grown from a single leaf `t`. No kernel load needed — this
// runs immediately.

open use raw "../prelude.disp" {}

// Three of the five rules dispatch on the SHAPE of a tree (leaf / stem /
// fork), so case analysis over arbitrary data is a rewrite rule, not
// library code:
let shape_of := t (t "leaf" ({u} => "stem")) ({u, v} => "fork")
test shape_of t = "leaf"
test shape_of (t t) = "stem"
test shape_of (t t t) = "fork"

// Numbers are trees too — 3 is sugar for succ (succ (succ zero)):
test tree_eq 3 (succ (succ (succ zero))) = true

// Programs can take programs apart — this is the reflection the whole
// language is built on (and the kernel exists to police):
test shape_of shape_of = "fork"