Types in High School: a Reflection

Posted on September 8, 2015

What’s this post about?

I’ve been in a reflective mood lately. I’m about to move to Santa Barbara for undergrad (I’ll be majoring in math in UCSB’s College of Creative Studies, a wonderful program that more people ought to know about), and I’ve been thinking a lot about the past year.

This post grew out of a conversation with Bob Constable at OPLSS, in which he asked me to write about my experience learning type theory in high school.

My story

Getting into type theory

I spent junior year immersed in functional programming, but I carefully avoided the world of dependent types. They sounded shiny, but I hadn’t yet sat down and read about them. This began to change when I was at the Mathematica Summer Camp, working on a project implementing different lambda calculi in Mathematica. After having extreme difficulty, I decided I should start learning about the theories behind the functional languages I so enjoyed. Thankfully, one of the instructors there also knew a fair bit about type theory, and on his advice I began to read the HoTT book.

At first, I found it to be impenetrable. Hoping to get a better understanding of the theory behind HoTT, I went searching for gentler intros. I toyed around with Oxij’s Brutal Intro to Agda, and this course from Conor McBride at Cambridge, but I still didn’t really know what I was doing. Eventually, I settled on working through Software Foundations. It took a long time, but SF was by far the most important book in my development as a mathematician. The interactivity, the pacing of the book, and the thoroughness of the material grew me both as a programmer and a prover. I still recommend it to programmers who haven’t done any serious proof-based mathematics and to mathematicians who want a more concrete intro than the HoTT book.

After Software Foundations, I read Adam Chlipala’s brilliant book Certified Programming with Dependent Types. I enjoyed the automated style of the book. Where SF taught me how to prove theorems, CPDT taught me how to do it elegantly. I was finally starting to get a strong intuition for how to actually use dependent types.

Becoming a type theoretic native

Somewhere around this point I decided I was ready to start learning about HoTT again. The correspondence hadn’t stopped being mysterious to me, and I was finally ready to change that. Lacking the general mathematical background it seemed to expect, it was a bit of a slog (and I still don’t really understand much of section 2). Most of my leaps in understanding came from catching the spatial meaning of concepts that I only knew abstractly. In particular, once I realized that path induction was just contracting paths, everything made sense.

I ended up giving a talk on HoTT for the SF Types, Theorems, & Programming Languages meetup in May. I had some experience teaching abstract math to non-mathematicians at my high school (an odd place that I ought to say more about at some point), but this was to be my first real lecture. Probably the most important thing I learned was the absolute necessity of giving people spatial intuition wherever possible. An algebraic characterization of path induction lacks the force of its spatial meaning - that segments are contractible. When I explained it that way, suddenly things made a lot of sense to people. In particular, it makes the unprovability of K obvious (a topic which I spent a long time confused about).

A month later I had graduated high school and was off to OPLSS, where I met a bunch of interesting people and learned a lot of interesting things.

OPLSS

I honestly don’t know where to start. It was the first time I met people who were doing active research in type theory, and it was an extremely valuable experience. Whether I was learning category theory (wonderfully complete lecture notes here), hearing about the foreign land of computational type theory, or pushing the limits of inductive recursive definitions, every minute was filled with interesting conversation and new things to learn about.

Part of the magic of the whole program had to do with the range of people there. The crowd ranged from people who’d never seen a dependent type before to professors doing research in type theory. No matter the topic, if you had a question about something type theory related there would be someone you could ask about it. I can’t recommend it enough to anyone interested in learning more about type theory.

It was at OPLSS that I began talking with Nate Thomas about applying type theory to work at MIRI.

A first real project

It didn’t take long for those conversations to turn into projects. A couple weeks after I got back from OPLSS I began an internship with MIRI working on systems for doing provability logic in type theory (some code for which you can find here). I was at once terrified and excited. I’d gotten very comfortable being the kid who knew more than people expected him to. It was the first time people expected me to do something new, not just to know things.

I’ve leveled up faster during the last few months than any other time in my life. If I had to guess why, I’d point to these reasons:

  1. A good project - working on reflecting type theory has required me to learn more about higher inductive definitions, induction recursion, provability logic, semantics, and different ways to push the capabilities of theorem provers, among other things.
  2. Collaborating - for most of my life, I’ve been self taught, and anything I’ve worked on has been similarly isolated. While at MIRI, I’ve still been fairly independent, but for the first time in years I’ve reliably had people to talk to about what I was doing and get feedback from. Which brings me to…
  3. The people - even on quiet days, the MIRI office is always filled with smart people who know a lot of things I don’t. There’s a lot to be said for learning by social osmosis, and I’ve been experiencing a lot of it.
  4. Scale - I’d never worked on a project of this size before. The closest I’d come was probably a scheme interpreter I wrote back in Junior year while learning Haskell, which, while probably larger in terms of sheer LoC, was also much more guided (by the excellent Wikibook tutorial, Write Yourself a Scheme in 48 Hours).

Today

My internship is wrapping up, and I’m preparing to move out. During the year, I’m hoping to continue working on reflective type theory in addition to some miscellaneous formalization projects for the Lean standard library.

What advice do I have for high schoolers?

Should you learn type theory?

I would say so. Type theory is like set theory in that the fundamental concepts are fairly simple, but their applications are deep and not yet fully understood. It doesn’t take much learning before you can start working on a formalization project, and I would contend that those are some of the best ways to get started in research.

What should you read to learn type theory?

Here are the sane defaults:

Another interesting perspective is Bob Constable’s not-quite-a-book Naive Computational Type Theory. It aims to do the job of Paul Halmos’ Naive Set Theory for type theory, and does a fairly good job. One interesting exercise that I haven’t tried yet is to work through all the exercises in JonPRL, a modern and fairly compact implementation of computational type theory.

General advice on learning math?

Don’t trust your math classes about what math is. Unless you’re in a very unusual situation (you’ll already know if you are) then your math classes are almost certainly not actually math.

Oh, also, don’t be afraid to not have a clue what’s going on. That never really stops happening.

Anything else?

We really, really need better introductory materials for type theory. I’m currently working on another post motivating this and sketching out some approaches for fixing this. Another useful thing would be something along the lines of Stephen Diehl’s What I Wish I Knew When Learning Haskell for type theory.