Hi Stefan
I hope you don't mind me copying this reply to the Epigram list: you've
raised an interesting topic, and I expect that others may also have
useful things to say. (Also, sorry to be slow in response: TYPES and
MSFP business are taking up most of my time these days.)
Stefan Karrmann wrote:
Dear Mr. Conor McBride,
you have suggested the notion of a level parameter for declarations. E.g.:
Level n
data nat = zero | succ nat
How should this be used?
Has nat the type 'forall n:nat, Type n' (in Coq notation)?
Can we apply nat only to constants or to arbitrary nats?
The key thing to achieve is /polymorphism/ in universe levels. My
favourite example of the problem is that certainly in Lego and Cayenne
(and I believe in Coq also) you may write
cons Nat (cons Bool nil) : List Type
and List's node in the universe graph will rise higher than that of Nat
or Bool, but
cons (List Nat) (cons (List Bool) nil)
can never typecheck. This isn't just an artificial problem: Yorck Hünke
and I tripped over it whilst trying zipWith: map List ts just didn't
work; we had to introduce 'big' and 'small' lists, duplicating
functionality. The point is that we dont 'want Lists at /some/ level, we
want /every/ level to be closed under formation of List types, just as
every level is closed under forall.
How to achieve this? Well, I'm not exactly sure, and I don't have a
viable system of rules just yet, but I think the key idea comes from
Harper and Pollack and it's to make definitions 'Hindley-Milner'
polymorphic in universe levels. The good news is that Epigram 2 no
longer has generative datatype declarations; like in Cayenne, 'data' is
just sugar for a common pattern of definition, so universe polymorphism
for definitions covers datatypes as well.
Now, at least in the first instance, this polymorphism will not be
expressed by the ordinary 'forall' or quantify over the ordinary 'nat',
in much the way that ML type schemes are not types. So it will be the
case that 'nat : Type n' for every n, but not that 'nat : forall n :
nat. Type n' (which does rather beg the question, anyway).
The bad news: cumulativity and polymorphism don't play so well together.
It's not impossible, but maintaining a global graph of universe
constraints and checking for cycles can become a lot of hard work. I'm
interested to investigate a more restricted, hopefully more tractable,
perhaps more explicit system. I'm not in a position to be precise just
yet, but I think it's worth considering making each universe level
closed under forall /on the nose/, rather than by taking the max level
of the domain and range, then introducing an explicit embedding from one
level to the next. I'd argue that /relative/ universe distinctions are
actually quite significant and do deserve some notation. This would make
types behave quite like the /names of types/ in UTT with Tarski-style
universes. It simplifies the polymorphism immensely: every definition is
polymorphic in its base level, level unification is just 'max'.
I don't know if that's too restrictive; I think we should be willing to
experiment with various approaches, and I'm keen to hear what other
people have been doing. I don't know exactly what needs to be explicit
and where, but I strongly suspect that our new explicitly bidirectional
approach to typechecking will shed some light on this. Epigram 2's core
theory explicitly separates the terms for which we infer types from the
terms whose type can only be checked. Elimination forms still require
head-normalisation of the target's type (eg, application happens to
functions, projection to pairs,...) but the full conversion rule happens
/only/ when the direction changes and we need that the inferred type of
a term coincides with the type we are trying to check. It is here that
we know both the inferred and required types of something, so we could
very well allow lifting coercions, rather than an exact match.
Some readers may be disappointed that I'm not talking about using the
datatype of natural numbers in all its computational for universe
levels, let alone more exotic well-founded orderings. I think we should
walk before we run. I'm not opposed to level-generic programming in
principle, but we've got enough work to do if we even want
level-parametric programming to work well. What we need is not just
theory, but /design/.
All the best
Conor
