The Calculus of Constructions is a very simple core functional language with dependent types. Per curry-howard isomorphism, it could, potentially, be very useful for writing programs and proofs. It, though, has a few problems: induction isn't derivable, it isn't possible to prove 0 != 1, and pattern matching on algebraic data structures take linear time. In order to solve those issues, practical languages such as Coq are based on the Calculus of Inductive Constructions instead, which add a layer of primitive datatypes on top of CoC. That, unfortunately, makes the core language very complex.

An alternative solution to those problems is a new primitive, self, which is a construction that allows a type to reference its typed term. This construct, together with the Parigot encoding, and a slightly weakened but still useful notion of contradiction, is sufficient to solve the problems above. The proposed language, though, is still somewhat complex. In particular, it has different Pi types, complex kind machinery and requires a restricted form of recursion (for the Parigot encoding).

Is it possible to be simpler? I.e., can the calculus of constructions with only self types and nothing else from this paper still be able to derive induction and employ the parigot encoding?

  • $\begingroup$ I feel like I answered a similar question here: cs.stackexchange.com/questions/49638/…. How is your current question different? Also, you seem to be asking 2 different questions in the title and the body. $\endgroup$ – cody May 1 '17 at 14:18
  • $\begingroup$ @cody I am so sorry. I spent some time googling and looking up to make sure I wasn't asking a repeated question (as I was fairly sure I had discussed something similar here), but I missed your answer to that post specifically covered this. It has none of the keywords I googled for... $\endgroup$ – MaiaVictor May 1 '17 at 16:27
  • 1
    $\begingroup$ No problem, and I actually vote for the question to stay open, since it may attract some interesting answers. $\endgroup$ – cody May 1 '17 at 21:32
  • $\begingroup$ You may want to look at guarded recursion. For example itu.dk/people/mogel/papers/lics2017.pdf $\endgroup$ – xavierm02 Jul 27 '17 at 15:05
  • $\begingroup$ I'm interested int this subject too. Have you got answers to your questions? Your quote "adding a new primitive, self" is incomplete. The paper states that you need to add mutually recursive definitions too, which break the analogy of types-as-proofs... Here is a newer work of same authors. The quote I'm talking about is in the penultimate paragraph of the first page. $\endgroup$ – user3368561 Jul 11 '18 at 14:41

Your Answer

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

Browse other questions tagged or ask your own question.