30 Sep 2014
I gave a talk
Papers We Love, Boston
on the 18th where I discussed Martin-Löf type theory from a historical
and programming context. The goal was to motivate and inspire reading
the (notably long) 1983 Martin-Löf lectures
On the Meanings of the Logical Constants and the Justifications of the Logical Laws. The video was just posted and the slides are available here.
24 Sep 2014
When studying sets in mathematics you learn a number of seemingly arbitrary constructions like, for instance, the so-called Cartesian Product. It's natural to ask why these constructions are so privileged... and while the answer is not exactly straightforward, it is very revealing! (An answer to a question posed on Quora.)
22 Aug 2014
10 Aug 2014
There's been a little flurry of activity around analyzing Clojure's upcoming transducers
using Haskell types. This post outlines an isomorphism between one such representation and list "binding functions"
a -> [b]
. This suggests that
is central to the idea of transduction.
08 Aug 2014
The technical concept "type safety", and even the underlying technical concept "type", is often misunderstood due to being conflated with marketing terms or given undue technical weight. This post enumerates some useful intuition pumps for better understanding, talking about, and consuming material related to type safety.
04 Aug 2014
Modern programming has something that was often talked about but never formalized throughout much of modern mathematics, codata
. This post sketches a constructive proof of diagonalization using codata in Haskell notation.
30 Jul 2014
Enumeration of container types is a very important programming technique. In immutable languages, one mechanism for this is to have a generic "left view" interface. This interface corresponds exactly to
codata and Swift is powerful enough to (almost) implement all of the above directly.
27 Jul 2014
A reimplementation of my lazy, infinite Calkin-Wilf enumeration of rationals post in Swift. Some commentary here talks about how to make heavily self-recursive data types compile in early betas of Swift.
26 Jul 2014
Swift is a new functional language developed by Apple. It has sufficiently nice types to directly represent most of what I discussed in The Types of Data
. Let's see what they look like!
23 Jul 2014
If you think of programming as arising as something natural from the structure of our world—and there's good reason to do so—then we can see the types of data which correspond to basic, universal logic as fundamental. This post describes these types and hints heavily at why they are so basic and universal.