# Do Self Types make the Calculus of Inductive Constructions obsolete?

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?

• Maybe I'm missing something but why aren't self types just general recursive types (eg unsound?) This isn't a goal for all dependently typed things but it certainly is import to CiC to be sound. The linked presentation has type in type as well but I don't think that's related/necessary. – Daniel Gratzer Nov 18 '15 at 14:09
• @jozefg Indeed: “Will be inconsistency as logic, but no problem for programs.” You should post this as an answer. – Gilles 'SO- stop being evil' Nov 18 '15 at 21:52
• Isn't that comment addressed for * : *, @GIlles, not for Self? – MaiaVictor Nov 18 '15 at 21:54
• @srvm with the typing rules they wrote, both are sources of unsoundness. Do you have a link to the paper? – Daniel Gratzer Nov 19 '15 at 1:20
• @jozefg I suppose it's this one: staff.computing.dundee.ac.uk/pengfu/document/papers/… – gallais Nov 19 '15 at 16:18

• 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).