3
$\begingroup$

I've been reading and understand the design choices behind Agda not having a cumulative universe hierarchy by default. However, while tinkering with the language, I've noticed that, at least for Agda 2.6.3, --cumulativity as a pragma is marked as incompatible with the --safe pragma.

This didn't sound unreasonable, but I've not found any reference in either the documentation or any other question as to why this is the case.

I know that this pragma is quite new (from version 2.6.1, if I'm not mistaken), and it would be reasonable to me that this is due to it still being considered experimental; but it would also seem plausible to me that something in the type system of the language made this feature, (although less radical than stuff like --type-in-type), intrinsically unsafe.

I would like to know which one of these two options (or maybe a secret third one!) is behind the decision, in a way to know if it would be expected for this feature to be "safely" available at some point in the future of the development of the language.

Improve this question
$\endgroup$
4
  • $\begingroup$ You may be interested in skimming over this. $\endgroup$
    – Trebor ♦
    Commented May 5, 2023 at 6:48
  • $\begingroup$ "I've been reading and understand the design choices behind Agda not having a cumulative universe hierarchy by default" Where can I find these documents/resources/blogs/articles? $\endgroup$
    – ice1000 ♦
    Commented May 5, 2023 at 6:57
  • $\begingroup$ @Trebor I had not actually consulted all issues with it, while I understood it was still problematic. However, what I was more interested in is whether if there were any more "semantic" issues with the pragma, or it was just unsafe because it is buggy. As I said, I'm less concerned with if it is unsafe but will be considered safe in due time, or there is some aspect of Agda's type theory that makes it unattainable in its current form (as --type-in-type, which leads to paradoxes). $\endgroup$
    – Evaristo
    Commented May 5, 2023 at 14:10
  • $\begingroup$ @ice1000 There is some discussion on why cumulativity is not on by default here, I can't find now the materials specific to Agda I've been reading. The gist of them is that Agda treats Level "as any other type", in that other languages treat universes as simply indexed by natural numbers, but Agda's levels can depend on other parameters, which makes equality of levels tricky to implement. $\endgroup$
    – Evaristo
    Commented May 5, 2023 at 14:25

1 Answer 1

Reset to default
2
$\begingroup$

The --cumulativity flag is currently marked as unsafe because of the (quite poor) heuristic it uses for solving universe levels, which might lose solutions and hence lead to type errors even if your code is well-typed. However, if your code is accepted then there are no (know) issues with soundness or termination.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Thanks! Do you know if there's some place to read about the discussion regarding this feature? I could find specific problems with it in the GitHub page, but nothing else, neither there, nor in the language documentation. $\endgroup$
    – Evaristo
    Commented May 10, 2023 at 12:34
  • $\begingroup$ This screams "undecidable" to me, not "unsafe". $\endgroup$
    – effectfully
    Commented May 25, 2023 at 23:38

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