World's most popular travel blog for travel bloggers.

# [Solved]: Do Self Types make the Calculus of Inductive Constructions obsolete?

, ,
Problem Detail:

Self Types are an extension of the Calculus of Constructions [1] that allow the language to express algebraic datatypes encoded through the Scott Encoding. The Scott Encoding provides one the ability to pattern-match in O(1), which is one of the main motivators for the inclusion of inductive definitions on CC. Yet, Self Types are make for a much simpler and elegant base theory, and are seemingly no less powerful.

Do Self Types, under a theoretical point of view, make CIC obsolete, or is there still some aspect on which CIC is favorable in relation to Self Tyes?

I'm not an expert in this work, but it seems to me that the major current issue is a lack of SN proof, even with restrictions. These proofs are notoriously tricky though, even when the calculus is correct, so I'd give it a little time. The work is certainly very promising.

One thing to note is that these restrictions are actually quite non-trivial to express, which is a large part of the complexity of the formulation of the inductive families in the CIC. The real selling point of an approach like this would be to concisely formulate these conditions.

It's been a somewhat longstanding open problem to have a dependently typed language which is

• Consistent/Normalizing
• Can express all the type families from Coq (or even Agda)
• Allows for a simple expression of recursion over these families
• Simple or has a small number of core constructions ($\Pi,\Sigma,\mu$).

One such attempt that I know of is the Altenkirch & al $\Pi\Sigma$ language, which similarly lacks a full meta-theoretical study (and also isn't consistent without further restrictions).