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.

Get started Try it in your browser

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

not false 0 steps

Why disp?

The type system, the self-verifying kernel, and five byte-agreeing evaluators run today. The rest is what they were built to reach. FOUNDATIONS.md keeps honest score of which is which.

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.

Type-as-predicates

A type is a function that takes a tree and returns `true`, `false`, or `Err`. You can trivially implement new type theories by just writing new functions, but the best part is that you don't have to think about type systems in terms of confusing sequence 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.

The features, in code

Every block below passes the real compiler. The playground runs that same compiler in your tab, kernel self-verification included, so the code and the claims can't drift apart.

▶ 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"

No pre-checked kernel ships

When the playground boots the type system, your browser re-elaborates the kernel's fragments in dependency order and re-verifies every typed export through the kernel itself. The last thing checked is the universe, by the universe.

prelude →cut →engine →cells →base →positive →generic →universe ⟲ Type checks Type

Watch it happen How can that be sound?