24
$\begingroup$

In the theory and design of proof assistants based upon dependent types, I feel like there’s a somewhat cultural divide between the "MLTT" world (with Agda as the main representative proof assistant) and the "CIC" world (with Coq). For instance, there are two presentations in annex A of the HoTT book, the first one presenting conversion as the equivalence relation generated by computation rules (this is I believe the traditional "CIC" presentation), while the second uses a typed conversion judgment (I would relate this to the "MLTT" culture).

What would you list as the features most representatives of each side, be it in the theoretical presentation or in the implementations? Or do you think this view of two different cultures is not accurate, and if so why?

$\endgroup$
0

4 Answers 4

19
$\begingroup$

I do not think I would align typed conversion with CiC versus MLTT. From my perspective, the move from untyped to typed conversion is simply an example of technology improving over time. While it wouldn't be trivial, producing a version of CiC with typed conversion seems like a fairly routine effort.

IMO, the serious difference in design lies in the treatment of Prop. Coq (and Lean) have an impredicative sort of propositions, and this really fundamentally changes the logical strength of the theory.

You can formalise the normalisation of System F in Coq/Lean, and you just can't in predicative systems like Agda. Conversely, the metatheory of predicative systems like Agda is much simpler to establish than that of CiC-style systems.

One thing which does seem like a cultural difference to me is that Agda/Idris favour top-level clausal definitions, whereas Coq has a more traditional expression-oriented design. (E.g., Agda doesn't even have a case expression AFAIK.)

There might be a slight technical basis to this choice (polarised presentations of type theory tend to lead one towards clausal definitions), but it mostly seems to be based on whether the proof assistant was implemented in Haskell (lots of clausal definitions) or ML (lots of expressions).

$\endgroup$
6
  • $\begingroup$ Agda has case-lambdas, which can be used to emulate case expressions. Maybe people just think that's enough. $\endgroup$
    – Trebor
    Feb 10 at 16:36
  • 1
    $\begingroup$ Re typed conversion, I'm going to agree with the OP and disagree somewhat with NeelK (despite all my admiration for NeelK!) — while "CiC with typed conversion" might be routine mathematically, and theoretically better, implementing it in Coq has been rejected multiple times for performance concerns. So the connection exists in practice. $\endgroup$ Feb 15 at 10:53
  • 2
    $\begingroup$ Do most people consider typed conversion to be an improvement over untyped conversion? I was under the impression that it was just another design decision you'd make depending on your needs (e.g. performance, as @Blaisorblade mentions) and deciding between them would be as reasonable as, say, choosing whether you want cumulativity or not. $\endgroup$
    – ionchy
    Feb 18 at 19:49
  • $\begingroup$ @ionchy Actually, a technical correction: technically Coq does use typed conversion to perform eta-expansion. But that's just bolted on untyped conversion, which blocks support for some eta-rules (IIRC, those on unit), so the core point stands. $\endgroup$ Feb 19 at 14:30
  • 4
    $\begingroup$ @Trebor Agda does have case-lambdas, but they desugar to top-level definitions. The implication of this is that two identical case-lambdas defined in different places are not definitionally equal, because they desugar to different top-level definitions, each of which is given a different machine-generated name. I think Idris does the same thing. $\endgroup$ Mar 11 at 15:10
17
$\begingroup$

The short answer is: $\mathbf{MLTT}$ relies on $\Pi$, $\Sigma$, $\mathbf{Id}$, $\mathbf{0}$, $\mathbf{1}$, $\mathbf{2}$, $\mathbf{W}$, and $\mathbf{CiC}$ relies on $\Pi$, $\Sigma$, $\mathbf{Id}$, General Inductive Schemes. They are slightly different systems, e.g. $\mathbf{0}$, $\mathbf{1}$, $\mathbf{2}$, $\mathbf{W}$ basis lacks of mutual recursivity which can be added separately. There are also a list of flavours of MLTT: MLTT-72 with $\Pi$, $\Sigma$ only, MLTT-73 with Id-types and predicative hierarchy of universes $\mathcal{U}_n$ and more recent developments up to HoTT which is also MLTT-80 based. The other option is $\mathcal{Prop}$ universe such that $\mathcal{Prop} \prec \mathcal{U}_n$. It is aded to CiC, but also could be added to MLTT. The pure formulas are following:

  • MLTT-72¹ = $\Pi$, $\Sigma$, $\mathcal{U}$

  • MLTT-73² = $\Pi$, $\Sigma$, +, $\mathbb{N}$, $\mathbb{N}_n$, $\mathbf{Id}$, $\mathcal{U}_n$

  • MLTT-80³ = $\Pi$, $\Sigma$, $\mathbf{0}$, $\mathbf{1}$, $\mathbf{2}$, $\mathbf{W}$, $\mathbf{Id}$, $\mathcal{U}_n$, derivable: +, $\mathbb{N}$, List

  • CiC⁴ = $\Pi$, $\Sigma$, $\mathbf{Id}$, $\mathbf{Ind}$, $\mathcal{U}_n$, $\mathcal{Prop}$

Among these systems CiC is most powerful as implements general inductive schemes with mutual recursivity, termination checking, and strict positivity checking.


[1]. Martin-Löf. An Intuitionistic Theory of Types. 1972
[2]. Martin-Löf. An Intuitionistic Theory of Types: Predicative Part. 1975
[3]. Martin-Löf. Intuitionistic Type Theory. 1980
[4]. Christine Paulin-Mohring. Introduction to the Calculus of Inductive Constructions. 2015

$\endgroup$
12
  • 1
    $\begingroup$ IIUC, the general inductive scheme is not responsible for the increased logical power of CIC (as general inductive types can pretty much be encoded with Sigma, Nat, and Id). However Prop, along with its singleton elimination rule, does add a tremendous amount of computational and logical power. $\endgroup$
    – Loïc
    Feb 10 at 17:17
  • $\begingroup$ You can't express mutual recursive types neither in MLTT-80 nor in MLTT-73. Also you will have all induction rules for free (definitional $\beta$) in inductive schemes. $\endgroup$ Feb 10 at 17:19
  • $\begingroup$ As I said you can add $\mathcal{Prop}$ to MLTT but won't have tremendous amount of computational and logical power to express even mutual recursive even-odd. $\endgroup$ Feb 10 at 17:25
  • 1
    $\begingroup$ The paper "A Syntax for Mutual Inductive Families" by Kaposi and Raumer explains the folklore fact that mutual inductive definitions can be encoded with indexed W types. Some reduction rules are not preserved by the encoding, but since they are propositionally derivable, this does not change the logical expressivity. $\endgroup$
    – Loïc
    Feb 10 at 17:31
  • $\begingroup$ You shouldn't equate them. W-types from MLTT are different thing that W-types in this paper. These are special kind of W-types addressed exactly described problem with mutual recursivity. They are neither W-types nor part of MLTT. $\endgroup$ Feb 10 at 17:34
11
$\begingroup$

The technical answers are correct, but they completely overlook the philosophical differences between the two formalisms. Martin-Löf type theory closely reflects Arendt Heyting's explanations of the logical signs and is intuitionistic by construction. CIC is a formal calculus based on string substitution with no underlying philosophy that I can detect.

I have personally heard Martin-Löf criticise CIC, in particular because it is impredicative. The habit of using CIC to do constructive mathematics has never made sense to me.

$\endgroup$
6
  • 5
    $\begingroup$ Thanks for the answer! Could you expand a little more on why using CIC to do constructive mathematics doesn't make sense? $\endgroup$ Feb 10 at 15:02
  • 1
    $\begingroup$ Constructive and predicative do not coincide, so I'm confused by the confusion :-). $\endgroup$ Feb 15 at 10:50
  • 3
    $\begingroup$ Impredicative systems such as CIC, or for that matter F with inductive types, satisfy both canonicity and strong normalization. This is enough for me to consider them to be constructive. I know there is a philosophical stance against impredicativity, but part of it is due to the Type : Type debacle. $\endgroup$ Feb 16 at 9:43
  • 1
    $\begingroup$ Let's turn this around and ask, why are you doing constructive mathematics? Is it out of a philosophical belief or with a technical objective such as obtaining executable code? I've read countless papers referring to constructive proofs as if it were an obligation, like saying grace before dinner. Sometimes they were proved over a classical axiomatisation, which is like having a starter of foie gras with your vegan meal. And I have been waiting 40 years for a convincing demonstration of executable code from a proof. People need to make their objectives clear. $\endgroup$ Mar 16 at 11:16
  • $\begingroup$ @LawrencePaulson Many (most?) of the people currently doing serious constructive mathematics are doing t for neither of the reasons you bring up: we neither care about extraction nor about philosophy. The reason is that we want to get a result that is valid over a topological space, or a topos. I agree with you that the "executable code" thing is not a convincing motivation of constructive math, and personally I believe the philosophical angle is not to convincing either. $\endgroup$ Mar 30 at 17:59
11
$\begingroup$

Apart from judgmental equality, MLTT and CIC also differ in the following:

  • The existence of an impredicative universe. CIC has Prop, and that's what makes it a part of the lambda cube. This universe can be useful in stating some theorems. MLTT is fully predicative.
  • Due to typed conversion, MLTT supports more eta laws.
  • The "preferred" underlying models are different. In my impression, CIC people prefer a domain theoretic model, while MLTT is based on Martin-Löf's so-called "substitution calculus" which has a very nice categorical model (with many different but similar presentations, like CwF, CwA, etc.).

For the last point, I would say it's more like a cultural diversity instead of a theoretical difference (but it's still worth mentioning).

$\endgroup$
0

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.