iOS Engineer at Yardsale, armchair type theorist and syntactician. Student of Ancient Greek, Latin, Sumerian, Akkadian, Hittite, German and Old English.
I’m currently banging my head against a three-dimensional model of natural language syntax in Intuitionistic Type Theory, which I hope will help us generate word order for Greek with minimal incidental structure. My more ambitious goal is to demonstrate a clear distinction between lexically mandated intrinsic structure, and the incidental structure which arises from an inexpressive theory.
Below are some articles that I have written recently on various topics relevant to my interests.
The six speeches of the Symposium may be divided into two sets: on the one hand, there is Phaedrus’s speech and those which are derivative of his, and on the other hand, there are the novel speeches; and these are the ones which reject the previous approaches and propose unique theories of Eros.
In this paper, I demonstrate how, and to what degree, phrase projectivity corresponds with register and meter in Sophocles’s Antigone, by developing a quantitative metric ℘ for projectivity and comparing it across lyrics, trimeters and anapaests using the data provided by the Perseus Ancient Greek Dependency Treebank. In the appendices, the formal algorithm for the computations done herein is developed in Haskell.
We can define the STLC at the type-level in Haskell, and then provide a type of derivations (proofs of well-typedness) which is indexed by terms. Further, we can use Haskell’s type classes to infer typing derivations for well-typed terms in the STLC.
Vinyl is a general solution to the records problem in Haskell using type level strings and other modern GHC features, featuring static structural typing (with a subtyping relation), and automatic row-polymorphic lenses. All this is possible without Template Haskell.
It is trivial to prove type equality in Haskell (to the extent that anything is every “proved” in Haskell). As for proving type inequality, Conor McBride demonstrates that this is possible to do using type families. Today, I’d like to show some techniques for doing the same in C++ with templates.
Today, I hope to introduce a more lightweight approach to immutable objects in Objective-C that sidesteps some of the problems with class clusters (such as hostility to subclassing) by making some trade-offs. The class cluster approach provides the following fronts of protection against illegal mutation:
I’m going to argue that the first force of protection (that of types) is far more important than the second (that of runtime exceptions), and that if we are willing to give it up, we can have a vastly simpler notion of immutability and mutability. Finally, I’ll discuss ways we can recover runtime exceptions in the case of an unsafe cast, and finally how we can recover the functionality of -mutableCopy in a subclass-friendly fashion.
Perhaps the greatest sin in the common body of Cocoa design patterns is the pervasiveness of “stringly-typed” code:1 it frequently comes up in KVO and bindings, among other things. Various macros have arisen to allow type checking of keypaths, largely thanks to efforts by Justin Spahr-Summers and myself. Today, I’d like to talk a bit about some ideas for enforcing statically trusted boundaries for checked keypaths.
