12
$\begingroup$

I'm working up from elaboration zoo and noticed that you don't use fixed point if you've got type level computation. It causes unification/equality check to hang up. Now, this means that I need inductive data structures of some kind if I want to compute on type-level.

What would be the easiest way to introduce inductive types?

W-type has a description that could be interpreted, but it is potentially cumbersome in practice.

W : {A : Set} → (B : A → Set) → Set
sup : (a:A) → {B} → (B a → W B) → W B
elim : {B} → (C : W B → Set) → ((a:A) → (f : B a → W B) → (c : (b : B a) → C (f b)) → C (sup a f)) → (w:W B) → C w

For instance, with nat we'd have:

Nat : W 2 {empty, unit}

zero : Nat
zero = sup 0 absurd

succ : Nat → Nat
succ n = sup 1 (λ_. n)

Elimination without pattern matching would be inconvenient, but doable.

I have a hunch that there's not many ways to put this together. It's some variation of W-type that I would have to implement. But which variant?

$\endgroup$
3
  • 1
    $\begingroup$ What is important for you? Convenience of use? Consistency? Efficiency? First-order data? $\endgroup$ Mar 8, 2022 at 13:40
  • $\begingroup$ @AlberttenNapel I have focused on the ease of implementation and some level of convenience. $\endgroup$
    – Cheery
    Mar 8, 2022 at 14:22
  • $\begingroup$ I'd suggest looking at github.com/sweirich/pi-forall. $\endgroup$ Mar 8, 2022 at 16:17

1 Answer 1

16
$\begingroup$

In principle, every indexed inductive type can be defined from $\bot$, $\top$, $\mathsf{Bool}$, $\Pi$, $\Sigma$, $\mathsf{W}$, $\mathsf{Id}$ and universes, with exactly the expected eliminators and computation rules: https://jashug.github.io/papers/whynotw.pdf. But this has a lot of encoding overhead.

If we want ergonomic support for inductive types, that's not simple at all and we have a number of design choices. There's a basic trade-off between ergonomics and implementation complexity.

  • A very basic choice is between eliminators and recursive definitions (including fixpoints). Eliminators are formally the easiest, but can be very inconvenient in practice. Recursive definitions tend to require a lot more effort to implement.
  • Coq has inductive signatures, case splitting and fixpoints. As you mention, fixpoints diverge if we try to naively compute them. In Coq, termination checking marks an argument of a fixpoint as decreasing, and fixpoints only compute when applied to a canonical value in the decreasing argument position.
  • Mini-TT allows recursive definitions, without termination checking. The obvious downside is that users have to perform termination checking instead (when necessary), but it's much easier to implement. However, we still have to avoid divergent unfolding. The Mini-TT solution is essentially to disallow unfolding of recursive names in certain contexts, so that e.g. we can't prove that a renamed version of a recursive function is convertible to the original version. Compare Coq, where fixpoint bodies can be compared for conversion. However, comparing recursive function bodies is not super useful in practice, because $\beta\eta$-conversion of definitions is far less common than extensional (pointwise) equality of functions. We usually want function extensionality, and richer $\beta\eta$-conversion by itself is not sufficient.
  • Agda has recursive definitions and termination checking, and no fixpoints and no conversion checking for recursive function bodies. Agda has by a fair margin the most powerful termination checker and the most powerful pattern matching elaboration. This is often very convenient, but the implementation is not for the faint of heart: https://dl.acm.org/doi/10.1145/3236770

Another variation is the range of allowed inductive types. Here, the easy choice is to stick to the inductive types which are reducible to W-types; these are roughly Dybjer's classic inductive families: https://www.researchgate.net/publication/226035566_Inductive_families.

Going beyond this is another way of complicating implementations. Induction-recursion and induction-induction are the most notable generalizations. These can be also implemented using eliminators or recursive definitions, but right now only Agda supports them. In Agda, induction-recursion and induction-induction arise as a "side effect" of positivity checking, termination checking and mutual definitions, but nothing prevents us from doing an eliminator-based implementation which is more amenable to small core syntaxes.

$\endgroup$
2
  • $\begingroup$ Your link to Mini-TT is incorrect. $\endgroup$ Mar 8, 2022 at 16:07
  • $\begingroup$ Thanks, fixed it. $\endgroup$ Mar 8, 2022 at 17:36

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.