10
$\begingroup$

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?

[1] http://staff.computing.dundee.ac.uk/pengfu/document/talks/mvd-2012.pdf

$\endgroup$
  • 2
    $\begingroup$ 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. $\endgroup$ – jozefg Nov 18 '15 at 14:09
  • $\begingroup$ @jozefg Indeed: “Will be inconsistency as logic, but no problem for programs.” You should post this as an answer. $\endgroup$ – Gilles Nov 18 '15 at 21:52
  • $\begingroup$ Isn't that comment addressed for * : *, @GIlles, not for Self? $\endgroup$ – MaiaVictor Nov 18 '15 at 21:54
  • $\begingroup$ @srvm with the typing rules they wrote, both are sources of unsoundness. Do you have a link to the paper? $\endgroup$ – jozefg Nov 19 '15 at 1:20
  • $\begingroup$ @jozefg I suppose it's this one: staff.computing.dundee.ac.uk/pengfu/document/papers/… $\endgroup$ – gallais Nov 19 '15 at 16:18
5
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.