6
$\begingroup$

Agda is said to be based on Luo's unifying theory of dependent types while Coq is based on the Calculus of Inductive Constructions. Both of these as I understand it extend the impredicative polymorphic Calculus of Constructions with a hierarchy of predicative universes, and inductive types as a built in concept (although they are definable already in CoC, I understand this approach is deficient in some ways.)

I have two questions:

  1. How does UTT differ from CiC on paper?
  2. How does the core type theory of Agda (which I presume differs in some ways from the original system of Luo) differ from the current best approximation to write down the core type theory of Coq, pCuIC?
$\endgroup$
7
  • 1
    $\begingroup$ Agda does not extend the Calculus of Construcitons. $\endgroup$ Feb 12 at 15:45
  • 1
    $\begingroup$ Thank you. To explain my confusion on this matter, Luo's book "Computation and Reasoning" cited by Ulf Norell in his PhD thesis spends most of the book developing a system called the "Extended Calculus of Constructions". In the last chapter it develops UTT which "can be seen as a further extension of ECC by a large class of inductive data types" and thus CoC. If you are able to clarify the relationship I will be grateful. $\endgroup$ Feb 12 at 16:02
  • 2
    $\begingroup$ I think digging up historical names for type theory is not particularly helpful for beginners. A lot of the times old names get reassigned to new objects, and so old papers will look confusing. $\endgroup$
    – Trebor
    Feb 12 at 16:59
  • 1
    $\begingroup$ I think “how does UTT differ from CIC?” is a worthwhile question to ask in its own right, but it probably has little to do with the difference between the theories Agda and Coq implement. I don't actually know anything about UTT other than that it extends CoC with universes and some inductive types (which sounds like a description of pCIC), and that Agda is (supposedly) based on it, but these facts are contradictory. Agda has many many extensions and experimental features, meaning that the resulting theory is far removed from any easily studied core language. $\endgroup$
    – James Wood
    Feb 13 at 10:07
  • 1
    $\begingroup$ I don't think that there really is such a thing as "core theories" of Coq either. We do advertise pCUIC from e.g. MetaCoq as being "some idealized Coq" but even pCUIC is a moving target. $\endgroup$ Feb 14 at 11:08

1 Answer 1

6
$\begingroup$

I will answer the headline question and ignore UTT (I believe thinking of Agda as UTT causes more confusion than it solves). There are very many differences between the theories Agda and Coq implement, and I do not have the time to explain every point. This list is also surely incomplete.

  • Coq has Prop (impredicativity + restricted elimination), for which Agda has no equivalent.
  • Both experimentally have strict propositions (Coq's SProp; Agda's Prop). Coq's are impredicative, while Agda's are predicative.
  • Coq optionally (but not by default) supports an impredicative Set universe, which Agda does not.
  • Coq's universes are cumulative. Agda has an option --cumulativity to turn on cumulative universes, but it is experimental and little used in practice.
  • Agda has an erasure modality, allowing for similar erasure as Coq provides for Prop, but also for indices (which is not possible in Coq).
  • Agda has a definitional irrelevance modality, which Coq does not have, but the use cases are very similar to those of strict propositions.
  • Agda has inductive-recursive definitions, which Coq does not have.
  • Agda has η-laws for all non-(co)inductive record types. Coq experimentally (option Primitive Projections) has η-laws for all non-(co)inductive record types with at least one field. This means that Agda has some definitionally contractible types, while Coq does not (outside of strict propositions).
  • Coq separates named definitions from recursion (hence the fix construct), making it more flexible than Agda in some cases.
  • Similarly, Coq separates pattern matching from top-level definitions, where in Agda, pattern matching structure is associated with named functions. In simple cases, this makes little difference, because in Agda we can introduce where definitions or extended λ-expressions wherever we need to match. However, sometimes the difference is visible to the user because Agda's pattern matching for a top-level function happens all at once, whereas in Coq, one can do matching step-by-step, and see intermediate states that would not occur in Agda.
  • Agda has support in the core language for dependent pattern matching, where Coq relies on the Equations package elaborating dependent pattern matching to simple pattern matching. Again, this usually makes little difference except for intermediate states and goal printing.
  • Agda (optionally, but by default) supports dependent pattern matching with K computationally – i.e, definitional clauses of functions give rise to definitional equations. Coq requires either an axiom or sethood proofs, both of which can affect the computational behaviour.
  • Coq and Agda have different solutions for coinduction.
  • Agda has a cubical mode, implementing a version of cubical type theory.
  • Agda provides various other optional extensions, like two-level type theory, guarded type theory, and spatial/crisp/cohesive type theory.
  • Agda provides more control over computation in the kernel, with both safe opaque definitions and unsafe REWRITE rules.
$\endgroup$
10
  • $\begingroup$ Agda has --cumulativity $\endgroup$
    – ice1000
    Feb 15 at 0:13
  • $\begingroup$ I think that this answer is a bit confusing. Some of the items are options changing the type theory of the considered proof assistant, so we cannot really talk anymore about the "core theory" of Agda or Coq. $\endgroup$ Feb 15 at 8:08
  • 1
    $\begingroup$ @ice1000 Thanks; I have edited this in. $\endgroup$
    – James Wood
    Feb 15 at 11:01
  • 1
    $\begingroup$ @Pierre-MariePédrot In reality, both implement a range of core theories, but I think we can still sensibly describe the range each tool achieves – where they overlap and where they don't. Do you think this comment is sufficient clarification? If so, I will edit it in. $\endgroup$
    – James Wood
    Feb 15 at 11:04
  • $\begingroup$ It should also be noted that Agda's pattern-matching, just like fixpoints, are in some sense second-class: like fix, Agda also has no match, only top-level definitions can do pattern-matching and recursion. $\endgroup$ Feb 20 at 10:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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