Briefly - Logics, FP, and Systems

After reading A Taste of Linear Logic by Philip Wadler today, I got to daydreaming. It’s a very interesting read. Expressed at a tutorial level, it guides the reader through the basics of intuitionistic logic (IL) and linear logic (LL). It explains the syntax of logic clearly, as well as the rules.

Summary of Logics

IL is akin to what one might see driving the type systems at the heart of Haskell and Ocaml. This is the heart of Propositions as Types. The fundamental operations are;

• Product × (logical: Conjunction ∧)
• Sum + (logical: Disjunction ∨)
• Function → types (logical: Implication →)

Here’s a little Haskell to connect it to the realm of types:

-- Person: a Product type represented by two Strings
data Person = Person String String

-- Maybe: a Sum type representing two possibilities
data Maybe a = Just a | Nothing

-- id: a Function type returning what was given to it
id :: a -> a

Here’s the grammar:

A, B, C = X ∣ A → B ∣ A × B ∣ A + B

Implicit in the typical presentation of IL are the theorems of Contraction, Weakening, and Exchange.

• Contraction: duplicated terms in a proof can be pruned
• Weakening: adding new information to a proof that was already proven doesn’t change the judgment
• Exchange: the order of evidence doesn’t change the judgment.

LL discards Contraction and Weakening in order to track the number of times a resource has been referenced. In turn, this changes the fundamental operations from IL quite a bit!

• Implication → becomes “consume and yield”  − o
• Conjuction ∧ becomes “both” ⊗ or “choose” &
• Disjunction ∨ is as before, but represented as “either” ⊕.

Here’s the grammar:

A, B, C = X ∣ A − o B ∣ A ⊗ B ∣ A & B ∣ A ⊕ B ∣ !A

Functional Programming and Linear Logic

Part of what made this paper striking for me is that it explains how to utilize both IL and LL in a type system. With my limited understanding of this area, I didn’t realize you could have both. It explains the elimination and introduction rules for moving from IL to LL and back. In practice, what this appears to mean is that you can have the expressive power of Haskell with the ability to track resources like Rust in the same type system.

Part of the promise of this is that there can be portions of a program where garbage collection (GC) isn’t needed. Constructs expressed through LL are those that can be tracked and safely managed without depending on GC or reference counting. Rust comes to mind here. This would be very valuable for say, real-time systems, where GC might not be compatible (or perhaps that depends on the GC algorithm?). On the correction side of things, it’d make it easier to track that a file has only been opened once, and is eventually closed on every possible program path.

Closing

There’s a lot still to be explored in the design space of programming languages. It’s exciting seeing how all these ideas come together to give us the tools we need to reason about the development of our systems. Here’s to looking forward to days when we no longer depend on C to express the core of systems we expect to Just Work.