Project Bewl

A DSL for the internal (Mitchell-Benabou) language of a topos.

Bewl is an ambitious and quixotic attempt to enable new techniques for manipulating set-like objects (permutations, musical objects, graphs, fuzzy sets, etc) as if they were sets. This involves a mix of advanced Scala and ludicrously abstract math. The most likely applications (still some way down the line) are to music theory or to the continuing quest for a proper explanation of permutation parity. It is also possible to use Bewl as an aid to learning category theory or as a computational algebra package where you can easily define your own algebraic structures.

To see the current to-do list and state of play, you can view this Trello board. There's also a continuous integration setup which runs all the tests on each commit.

Presentations explaining the project

Some of these are more accessible than others: pick one that's right for you.

In May 2018, I gave a talk about Bewl for S-REPLS 9 at the University of Sussex (slides, video) Requires some math.

My attempt at explaining Bewl for a general audience on cruft.io : Towards an arithmetic of sets

Using Bewl to do musical calculations - putting the chord of C major under the microscope

Overall state of play as of January 2016.

See this presentation for an attempt at "the internal language for dummies"

I've had to keep re-implementing Bewl in successively more powerful programming languages (Java, Clojure and now Scala). Now learning Idris, which is an amazing language and may be the next logical step.

This presentation explains the new "intrinsic" Bewl 2.0 DSL and why it's better than the previous "diagrammatic" 1.0 one.

Here's a presentation about Bewl's universal algebra capabilities.

This animated video was an initial attempt to explain Bewl (back when it was called Bile)

Notes on some promising breakthroughs re speeding up the topos of actions

Parity

This presentation describes my simplistic but ambitious plan to solve the mystery of permutation parity by calculating the double exponential monad for ¬, the permutation interchanging true and false. Here's one about the topos of automorphisms, another chapter in the ongoing parity quest. Here's an update. (Since then, I've decided it would be easier to generalize the transfer using the theory of Coxeter groups, but that's another story.)

Music

Here I relate Bewl to Thomas Noll's paper about music theory and topoi

Category theory tutorials

Refresher on strong monads.

If you want to use Bewl as a learning aid to study category theory, start here.

Intended applications

• Explore music theory via the triadic topos (see The Topos of Music)
• Explore parity in other topoi (as it's so poorly understood for sets). Easier now that the "topos of permutations" is implemented.
• Explore the topos of graphs. Bewl will let us talk about graphs as if they were sets
• Explore fuzzy sets (using the more careful definition that makes them into a topos)
• Explore Lawvere-Tierney topologies (and perhaps save these music theorists from having to calculate them by hand)

Done so far

• Created Topos API as a trait
• Implemented FiniteSets as a topos
• Added 'generic topos tests' which use fixtures for the given topos
• Can define and verify algebraic laws. Only 'monotyped' laws as yet - can't define monoid and ring actions
• compact notation for elements / lambdas / uniform operators
• adapter for diagrammatic layer
• Separated BaseTopos from its extra layers (Algebra, AlgebraicStructures) which are now traits
• Universal and existential quantifiers
• Strong binding: a new layer with stars/quivers concreting over dots/arrows ; stars bound to classes ; quivers/functions interchangeable
• Specialized element types: e.g. product has left, right ; exponential can apply
• Adapter that makes a dots-and-arrows topos look like a stars-and-quivers one
• Implementation of FiniteSets using new DSL
• Defined quantifiers in new DSL
• Construct the initial object 0
• Coproducts
• predicates isMonic, isEpic, isIso
• enumerate morphisms / global elements
• Partial arrow classifier
• walkthrough for using Bewl as a learning aid for studying category theory [NEEDS UPDATING]
• universal algebra: can define algebraic structures, using existing ones as parameter spaces (for monoid actions)
• implemented topos of monoid actions
• implemented topos of automorphisms
• traits for monads and strong monads
• implement double-exponential (continuation) monad
• endow the subobject classifier with a Heyting algebra structure
• removed legacy DiagrammaticTopos code
• images
• quotients and lifts
• more algebraic structures: now include all the classical ones
• coequalizers

To do

• construct the monad of monoid actions
• construct the reader monad
• construct 'pitchfork' for algebras over a strong monad
• construct 'pitchfork' for 'informal' (operator) algebras
• construct the topos of coalgebras, and so (maybe a slow implementation of) the slice topos
• Can extend and remap algebraic structures, e.g. ring extends abelian group remaps group with an extra law
• More algebraic constructions: endomorphism ring, transfer
• separate out the language, have an independent first-order grammar, in which there can be proofs?
• have a concept of 'models' and streamline construction constellation/scalars
• language in which class ::== a theory
• implicit objects, follow Odersky concept of 'context' used in Dotty
• make =?= be a binary operation on (extra rich) elements
• tell if an object has an injective hull
• Optimize algorithm enough to construct triadic topos and its topologies
• Construct the slice topos. Use McLarty's construction, NOT the one in Moerdijk/Maclane which requires you to first construct the power object for exponentials