My interest in Type Theory

Through the Oregon Programming Languages Summer School videos I became interested in Type Theory over a year ago, and in what little so-called spare time I have these days it has become my primary recreational interest.

I have presented a couple of different talks on the subject over the past few months. A presentation on Homotopy Type Theory which is derived from a prior talk I gave at Tachyus on Type Theory and Practical Application.

A note of caution to anyone diving into Type Theory through anything I have written. I have presented on Type Theory and Hott in particular because there is a lot of interest by programmers in this topic. Preparing and giving both talks was a learning opportunity for me. A lot of questions followed from the perspective of category theory, and fortunately there was usually someone with a background in that area willing to take them. There’s flagrant overreaching in my presentations. Calling path induction “the fundamental theorem of type theory” is way too provocative for a neophyte to attempt, and in introducing the axiom of univalence I did not set up nearly enough introduction for it to make sense. Specifically the equivalence operator needs quite a bit of introduction.

Both my presentations evoked lively discussion and stretched out to two hours. It is really too much to cover in one presentation, even for an introduction. Ideally a follow-up presentation (or two) would be outlined as follows.

  • Cover the formation, introduction, elimination, and computation rules for the primary types…and perhaps some of the later specific types introduced in The Hott Book.1
  • An in depth look at path induction.
  • What is equivalence?
  • Only then can function extensionality and univalence have the context necessary for introduction.
  • …and cover sets in type theory and mere propositions.


[1] The HoTT Book, §1.5. This is all math-speak. I will attempt to translate into programmer-speak.

Formation Rule: How one forms a type, the representation syntax.

Introduction Rule: The constructor(s) for forming elements of the type.

Elimination Rule: How to use an element of the type, the usage syntax.

Computation Rule: a.k.a. β-reduction to the theorists. Simply put, using the constructor in an expression.

Upcoming Events

Long time since last post. I’ve been having a great time, but very busy, working for Tachyus, the first Silicon Valley tech company devoted to the oil and gas industry. Working on technology solutions for the physical world is emotionally rewarding, and all the better that we code the software side almost exclusively in F#.

I’m participating in a lot of community activities in the next couple of months.

October 2 & 3 at the Progressive F# Tutorials NYC

I’m really excited about meeting old and new F# colleagues. Shout-out to for sponsoring. This is a great conference for anyone interested in F# at any level, with top notch beginners and advanced tracks. Fellow Tachyus engineer Will Smith (Twitter @tihan) is doing an advanced track presentation on his project for inlining C code in F#.

October 11 & 12 Silicon Valley Code Camp

The 9th annual edition of the world’s largest free software development conference. This year I helped put together an F# track of sessions on Saturday, as well as a Sunday session, Functional Programming for Production Quality Code, that I will present.

Big shout out to

Peter Kellner (Twitter: @pkellner) for being the guiding light of SVCC,

as well as

Mathias Brandewinder (Twitter: @brandewinder), (spiritual leader of the Bay Area F# community),

Will Smith (again),

Ryan Riley (Twitter: @panesofglass) (another Tachyon),

and Riccardo Terrell (Twitter: @TRikace)

for contributing talks to the F# track.

November 2 – 6 Microsoft MVP Global Summit

This event is not open to the public, but if you are an MVP or work for Microsoft, Ryan and I will be presenting the F# open source projects Tachyus uses and contributes to at the Sunday afternoon MVP Expo. We are also going to try to schedule an MVP to MVP talk on the subject.