Software engineer, dilettante type theorist, syntactician, and philologist. Student of Ancient Greek, Sumerian, Hittite, Akkadian, Latin, Old English and German. I also compose music; hit me up if I can help on one of your projects!
Here I present an idea for a type theory which retains the benefits of wholesale adherence to the realizability interpretation1 à la Nuprl2, and yet seems to maintain a better division of labor between operator and machine.
In my recent post I demonstrated a type-theoretic formulation of non-dependent record types as presheaves on a particular topological space \(X\) of keys given an assignment \(El_X : X\to\mathbf{Type}\). Today, I’ll construct more interesting records by endowing the key space with a non-discrete topology.
Family union types have existed for a few years in Extensional Type Theory à la Nuprl;1 here, I demonstrate a lightweight approach to adding them to Intensional Type Theory as an extension of Altenkirch, McBride, Swierstra’s OTT.2
Let us define a record type as being given by a type \(X\) of keys and an interpretation function \(F\) which maps every key \(x:X\) to a type. We assume the existence of a powerset functor \(\mathcal{P}: \mathbf{Type}\to\mathbf{Type}\), which endows the discrete topology on \(X\). Then a record type is the product of the image of \(F\) over a subset of \(X\): \[ \mbox{for}\ U\subseteq X,\quad \mathsf{Rec}(U,F) :\equiv \prod_{s:U} F(s) \]
To those of us without a background in topology, it may have initially been surprising that the unit circle \(S^1\) is not contractible. In this post, I’ll outline a homotopy type-theoretic proof for why this is in fact the case.
It is well known that generalized algebraic data types (a sort of phase-locked inductive family) suffice in languages like Haskell1 and OCaml to be used as a deductive system for intuitionistic logic. I’ll demonstrate how type-level axioms can be given and used in Standard ML, using only signatures and functors.
The issue of verbs which appear to take multiple arguments has long been a sticking point for Chomskyan grammarians, with various proposals having taken shape. Here, I’ll describe current approaches in transformational grammar, and demonstrate another approach in Multi-Modal Combinatorial Categorial Grammar. Finally, I’ll discuss the pros and cons of each approach.
As I read Bell’s A Primer of Smooth Infinitesimal Analysis, I thought it would be useful for me to write down my workings of the exercises as I went. The proofs are in the language of Intuitionistic Type Theory; according to common practice, I will sometimes omit arguments from application which can easily be inferred from the others.
