The Topos of Programming | Yon

2 min read Original article ↗

The Topos of Programming

A topos-oriented programming language.

Syntax Reference Benchmarks

Native via MLIR & LLVMNo garbage collectorAGPL

The heap

The address of a value is its content.

Yon allocates into xleech2, a content-addressed heap whose geometry is the Leech lattice Λ24: exactly 196,560 slots per heap. Allocation hashes the bytes; identical content returns the existing slot, so same content ⇔ same slot. Equality of arbitrarily large values is one number comparison: O(1) structural equality, by construction.

String.equal: ~17 ns at 1 char and at 32,768 chars. Three orders of magnitude of size, the same per-comparison time.Benchmarks

hello.yon

fun main(): number {
  be greeting holds "ciao, mondo"   // interned on the heap
  be _ holds String.print(greeting)
  return 0
}

$ yonc hello.yon -o hello && ./hellociao, mondo

Every string literal is a section of the builtin String place, interned on that same heap, so two equal strings are one slot, however they were built.

The paradigm

Worlds are categories. Behaviour is arrows.

In Topos-Oriented Programming a world is a category, a place is an object in it, and a value is a section: immutable, identified by its content. All behaviour lives in arrows. Identity is the exception, requested only where you need it. Logic is internal: truth is the subobject classifier Ω, and unknown is a citizen of the Heyting core, not an error. From the Yoneda lemma, a thing is determined by its relations; the type checker, optimizer, and allocator act on that.

Read “Topos-Oriented Programming”

Execution model

What Yon does without.

Identity is explicit. Concurrency is the process. Failure is a value. The interface to a place is its arrows. Four mechanisms common elsewhere are absent:

No garbage collector

Slots are stable for the life of the process; the heap grows with distinct content only.

No threads

The unit of concurrency is the process. Spaces talk over a shared-memory wire.

No exceptions

Failure is data: a place, a declaration, or a process exit, never a thrown stack.

No typeclasses

Arrows are the interface: a place’s presheaf of observations.

Future work Source: OCaml, MLIR, C