MadMode

Dan Connolly's tinkering lab notebook

Rosetta Stone: Taking propositions-as-types to the next level

The Rosetta Stone paper by Baez and Stay has been on my to-read list since a conversation with Stay on a bus a few years ago. The scope is a bit intimidating:

Category Theory Physics Topology Logic Computation
object system manifold proposition data type
morphism process cobordism proof program
Table 1: The Rosetta Stone (pocket version)

But in Fun with Categories, the Statebox folks laid the groundwork for grokking category theory with idris in their idris-ct library.

And the RChain community includes a #computational-calculi channel where people get together to study such things... I get to fill in gaps from skipping grad school without all the tuition and tests :). Jake and several other people there immediately agreed when I suggested we read this paper together. Jake dug up Mike Stay's slides and notes and it took just a little work to get the details into the calendar. Jake connected us to the statebox folks via a Category Theory chat group started by Christian W.

Quantum Physics Gap

Of the five domains in the Rosetta Stone, Quantum Physics is definitely the most indimidating, to me. The Quantum Physics Sequence by Yudkowsky in 2008 is the closest thing I have found so far to something my speed, but I think I made it only 1/3rd of the way thru.

I had to look up Hilbert space; fortunately my linear algebra and topology is fresh enough that "a real or complex inner product space that is also a complete metric space with respect to the distance function induced by the inner product" only took a few minutes to grok.

I just watched a lecture by Edward Witten about knots and QM, a recommended Tomaslov passed along from Greg. Quantifier noted A Quantum Mechanics Primer by D.T.Gillespie as highly regarded. Jake sai Baez has a good list of recommend resources.

Fab from Statebox recommended Picturing Quantum Processes. Here's hoping...

Intro to Idris

I gave an intro to idris this week:

Idris is a programming language designed to encourage Type-Driven Development.

In type-driven development, types are tools for constructing programs. We treat the type as the plan for a program, and use the compiler and type checker as our assistant, guiding us to a complete program that satisfies the type. The more expressive the type is that we give up front, the more confidence we can have that the resulting program will be correct.

In Idris, types are first-class constructs in the langauge. This means types can be passed as arguments to functions, and returned from functions just like any other value ...

We have a recording, though it was a pretty informal session.

Installing Idris

Idris docs recommend cabal install idris but that's a pain; nix support for idris reduces installation (and use!) to just[^1]:

$ nix-shell -p 'idrisPackages.with-packages (with idrisPackages; [ contrib pruviloj ])'

I like to combine it with direnv support for nix so that when I cd into an idris project directory, it all Just Works.

[^1]: if you get idris-modules/build-builtin-package.nix:23 is marked as broken, refusing to evaluate, your nix installation may be out of date; nix update-nix worked for me.

There seems to be good vs-code support for idris, but I don't know how to get it to look at the contrib package, so for today, I tried emacs, though even that showed some rough edges.

Formalizing Knowledge with Idris

LaTeX is fine for typesetting knowledge, but my goal is to formalize knowledge such that the machine can help exploit it.

The example I gave in my Feb 29 tweet was a 2016 paper on capabilities and confused deputy attacks.

The first definitions I captured were:

We assume two countable sets, $Loc$ of mutable references and $Prin$ of principals. ... Values consist of integers ($n$), booleans ($tt$, $ff$) and pointers or mutable references $R_r$ and $W_r$.

In idris, this takes the somewhat familiar of a haskell / ML data type:

data Loc = MkLoc Nat
data Prin = MkPrin Nat

data Value =
    IntVal ZZ
  | True
  | False
  | Read Loc
  | Write Loc

This allows the idris compiler to, for example, let me know when I neglected to handle all kinds of Value later in my transcription to code.

Extending idris-ct for the Rosetta Stone

On page 5 of the Rosetta Stone paper we find this nice diagram relating definitions in category theory:

idris-ct already formalizes monoidal categories and symmetric monoidal categories but not closed categories and cartesian categories. Jake started laying the ground work for CartesianCategory.idr and such.

In discussion of cup and cap, Fabrizio answered a question by way of a figure from some of his work on petri nets. He also mentioned Samson Abramsky's work; Computational interpretations of linear logic has been on my list since Greg said it "changed the direction of his career." Here's hoping for time to study that one closely too.