16
$\begingroup$

In the concluding statement of "universe hierarchies", Conor McBride calls it

[...] that key lesson which I learned from James McKinna: never resort to polymorphism when initiality will do.

How can you recognize when you could use initiality instead of polymorphism, and why should you prefer to use initiality?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
24
$\begingroup$

Initiality comes with a powerful universal property which allows you to, internally, prove statements about the constructions you perform. If you give me an element of data Nat = Z | S Nat, I can perform induction on it.

Polymorphism on the other hand requires you to appeal to external principles such as parametricity (*) to recover similar reasoning principles. If you give me a function of type (a -> a) -> a -> a, I will know it is bound to be a natural number in disguise but will be powerless to exploit that fact.

Additionally in predicative systems with a tower of universes, initiality is typically size-respecting whereas an encoding via polymorphism will land you a definition that lives one level up in the hierarchy due to the universal quantification. If you want to iterate these constructions, that's bad news.

(*) caveat: there are type theories attempting to internalise parametricity

Improve this answer
$\endgroup$
3
  • 4
    $\begingroup$ Wish I could up-vote multiple times. This answer is so incredibly obvious (post facto) I'm kind of ashamed that I didn't see it myself. I think the deep explanation (prefer size-respecting internal reasoning over external, potentially size-increasing reasoning) is one that can likely be instantiated multiple times to good effect. $\endgroup$
    – Jacques Carette
    Commented Mar 25, 2022 at 12:35
  • $\begingroup$ In the third paragraph, do you mean "in predicative systems"? $\endgroup$
    – Mike Shulman
    Commented Mar 25, 2022 at 15:06
  • $\begingroup$ @MikeShulman Good catch. Fixed it now. Thanks! $\endgroup$
    – gallais
    Commented Mar 25, 2022 at 16:26

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