What is Axiom K?

Question

I've noticed the discussion of "Axiom K" comes up more often since HoTT. I believe it's related to pattern matching. I'm surprised that I cannot find a reference in TAPL, ATTAPL or PFPL.

• What is Axiom K?
• Is it used for ML-style pattern matching as in SML (or just dependent pattern matching)?
• What's an appropriate reference for Axiom K?

Answer 1

Axiom K is also called the principle of uniqueness of identity proofs, and it is an axiom about the nature of the identity type in Martin-Löf's dependent type theory. This type doesn't exist (and in fact cannot be defined) in simpler type theories such as System F, so that is probably the reason why you haven't encountered it in the books you mention.

The identity type is written as Id(A,x,y) or also x = y and encodes the property that x and y are equal (under the Curry-Howard correspondence). There is one basic way to give a proof of the identity type, and that is refl : Id(A,x,x), i.e. the proof that x is equal to itself.

When investigating the identity type in his thesis, Thomas Streicher introduced a new eliminator for the identity type which he called K (as the next letter in the alphabet after J, the standard eliminator for the identity type). It states that any proof p of an equality of the form x = x is itself equal to the trivial proof refl. From this, it follows that any two proofs p and q of any equation x = y are equal, hence the alternative name "uniqueness of identity proofs". What's remarkable is that he proved that this does not follow from the standard rules of type theory. I recommend reading Dan Licata's article on the homotopy type theory blog if you want to understand why not, he explains it much better than I could.

To answer the second part of your question: ML-style pattern matching is unrelated to K, since ML doesn't have an identity type and hence cannot even formulate the K axiom. On the other hand, K is required for dependent pattern matching as introduced by Thierry Coquand in "Pattern matching with dependent types (1992)". The reason for this is that it is very easy to prove K by pattern matching on the constructor refl of the identity type:

K : (p : x = x) -> p = refl
K refl = refl

In fact, Conor McBride showed in his thesis ("Dependently typed functional programs and their proofs (2000)") that K is the only thing that dependent pattern matching really adds to dependent type theory.

My own interest in this subject is to understand exactly why dependent pattern matching requires K and how it can be restricted so it doesn't anymore. The result was a paper and a new implementation of the --without-K option in Agda. The basic idea is that the unification algorithm used for case analysis during dependent pattern matching shouldn't delete equations of the form x = x, because doing so requires K. I recommend you read the (introduction of) the paper if you want to know more.