<div dir="ltr">On Fri, Jun 28, 2013 at 5:04 PM, Martin Escardo <span dir="ltr"><<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>></span> wrote:<br><div class="gmail_extra"><div class="gmail_quote">
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
Uncomment to get the error "Setω is not a valid type".<br>
<br>
That is, the type "{l : Level} (n : ℕ {l}) → Set(newlife n)" is too<br>
big. But it is the type of the function f, which Agda accepts.<br>
<br>
The point I am trying to make is that it doesn't make sense to have a<br>
type of universe levels. Type levels ought to be meta-liguistic.<br></blockquote><div><br>I don't really think you've demonstrated that.<br><br>For one, the Setω handling in Agda is a little funky. It is inferred as a type for some things, but isn't allowed to occur in other places that would be expected based on that. I think that's wrong, but it's just a bug. I wrote a type checker a while back to experiment with Agda-like universe polymorphism, and it doesn't have this issue (or, wouldn't need to if I handled definitions more like Agda's; it would involve a special case somewhere, though). There is just a top type Ω for universe polymorphic types, and it's relatively normal as a type. You can even take sums over universes with sigma in my system, which is impossible in Agda, because it would require specifying that a data definition has type Setω, which is one of the things that is not allowed. But again, I think that is a _bug_ in the implementation, not a fundamental property.<br>
<br>Now, what you can't do in my system (as I recall; it's been a while since I wrote it) is quantify over Ω. Which also means you can't write functions Ω -> Ω and so on. But this is not out of the ordinary at all in type theory. The lambda cube is typically formulated with values which have types, types which have kinds involving * and arrow, and a box, which classifies all the kinds. But box is the only thing at its level; there are no function spaces between boxes, or quantification over box things.<br>
<br>So hierarchies with tops that don't have all the properties of the things below it aren't unusual in type theory. I just think Agda's a bit busted, and no one has spent the effort to fix it up (because it doesn't bite often). But, the statement:<br>
<br>> there is an Agda type that doesn't have any Agda type.<br><br>is not necessarily cause for alarm (in fact, Martin-Löf type theory as often presented does not have types for types at all; types are the top level, and there are only universes, which are types whose values represent types, but are not types; and original MLTT only had the one universe, which of course did not have a value representing itself).<br>
<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
I suggest that Agda should move to typical ambiguity, using Harper's<br>
algorithm. This would both solve this problem and make the Agda users'<br>
lives easier, and Agda programs much more readable.<br></blockquote><div><br>Does typical ambiguity allow you to do everything that Agda's current polymorphism does? Is it what Coq uses? I know that in the past people routinely ran into (erroneous) universe conflicts without getting very far into formalizing parts of category theory in Coq. So adopting a similar system might kill one of the largest developments currently in Agda.<br>
<br>I do think it's annoying to have to explicitly specify all the universe levels of everything in Agda. But I also know there's a fair amount of literature out there suggesting that having the opportunity (if not the obligation) to handle universes explicitly is important. Or at least, completely implicit systems tend to lack generativity necessary for certain examples.<br>
</div></div></div></div>