À la recherche du Inductive Datatypes

Inspiration

Proust is a proof assistant developed by Prabhakar Ragde (University of Waterloo) to be used in teaching CS 245e (Logic and Computation, Enriched). The name is a pun wherein saying proof assistant quickly (so as to elide a few syllables) is a near homonym of the surname French novelist Marcel Proust.

More recently, I used Proust in teaching MAT 250 (Introduction to Advanced Mathematics) at Stony Brook this past summer.

The one sentence pitch for why one would do this in a course that had been (in both Prabhakar's and my course) previously confined to pencil and paper is: an excellent way to figure out how math works is to put math on a computer.

Students are provided with bare bones starter code (written in Racket, a lisp dialect - my course began by teaching students the language) and students then implement by themselves most of the functionality and use the code that they just wrote to solve their proof-writing homework. This teaches the mathematics on a very deep level and, as a bonus, explain proof assistant in the best way possible - by writing your own proof assistant!

What it does

Booleans, natural numbers, lists, equality, and logical connectives (AND, OR, NOT) are just several examples of algebraic datatypes (ADTs) that may be handled under a uniform heading. A better name for ADTs is inductive types.

The best example of an inductive type is Nat, the type of natural numbers. A Nat is either Z or (S n) where n is a Nat. This describes how to construct Nats: Z is a Nat, (S Z) is a Nat, (S (S Z)) is a Nat, etc.

In order to define a function f on Nat, it suffices to define (f Z) and (f (S n)) in terms of (f n). From the perspective of dependant type theory, this also says how to prove theorems about Nat, such as commutativity of addition (and it allows defining addition in the first place).

This project is towards adding uniform support of inductive types in Proust.

Challenges I ran into

There's much less adrenaline involved in a remote hackathon and as such I did not work as effectively as I should have. I worked out the theory on paper, but did not complete the implementation.

What's next for À la recherche du Inductive Datatypes

Actually implementing the rules that I worked out.

Built With

• dependant-type-theory
• pen-and-paper
• proust
• racket