The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

Dear Dan,

thanks for your answer and the pointer to the EPTS paper.  I had not  
seen it so far, I always refer to a paper by Barras and Bernardo  
published at the same conference (FoSSaCS 2008) with nearly the same  
content!

In MiniAgda, I am using EPTSs and I started implementing them for  
Agda, although there are some issues to clarify when you scale up from  
PTSs to a real dependent type theory with types defined by cases.

- PTS rules can be used to forbid your embed function, if you put  
Level outside of the Set tower.
If TLevel is the sort of Level, then just do not add rules like (Set  
i, Level, Level).

- Then, since there are no constructors for Level, you cannot match on  
anything of type Level, so there is no computational dependency on  
Level things.

- Additionally, we can make Level quantification

  (i : Level) -> A

irrelevant, .(i : Level) -> A in future Agda syntax, [i : Level] -> A  
in MiniAgda syntax, as long as A is something that is inhabited by  
terms only (meaning that we can be sure that A is not a universe).

Finding out whether something is a universe is not completely trivial  
in Coq or Agda, because of types defined by cases and cumulativity.   
Consider this little MiniAgda program (nothing specific to MiniAgda  
here):

data Bool : Set 0   -- Bool  is a type
{ true  : Bool      -- true  is a term
; false : Bool      -- false is a term
}

fun T : Bool -> Set 1 -- T is a type (scheme)
{ T true  = Bool      -- T true is a type
; T false = Set 0     -- T false is a universe
}

-- cannot erase T x argument, even though T x : Set 1 and Bool : Set 0
fun weird : (x : Bool) -> T x -> Bool
{ weird false A     = false
; weird true  true  = false
; weird true  false = true
}

While T false is a universe, T true is just a data type.   
Consequently, T x, even though it is in Set 1 (and not in anything  
below), cannot be marked irrelevant in the type of weird.  This is  
why, unfortunately, your idea

>  (_, Set i, Set j) -> Set j if i <= j
>  (c, Set i, Set j) -> Set i if i >  j


does not work.

I remember having seen somewhere [Augustsson's Cayenne? cannot find  
the reference] a system where each type gets both a minimum sort and a  
"maximum" sort (meaning a lub).  Then, T x would have sort [0,1]  
meaning it can be a type or a universe.  Marking arguments irrelevant  
seems to require the minimum sort rather than the maximum sort.

I would really like to work out a irrelevance inference, any help is  
appreciated.

Regarding the Set\omega:  It is forbidden in Agda, so some things  
cannot be expressed.  But if we add it to Agda and internally use a  
Set(\omega + 1) to type Set\omega, would there not again things you  
cannot express?

Of course, there is no reason why the hierarchy should stop at \omega,  
you could go to higher ordinals... :-)  However, maybe we should wait  
with this until practical applications appear that use more than 3  
levels. :-)

Cheers,
Andreas

On Sep 14, 2010, at 8:07 PM, Dan Doel wrote:

> On Tuesday 14 September 2010 8:56:30 am Andreas Abel wrote:
>
> > This ensures that levels remain irrelevant for
> > computation, they are only there to sort out the universe
> > stratification.  This is in analogy to sizes in the type-based
> > termination approach: sizes are only there to sort out the
> > termination, they are computationally irrelevant.
>
> Ah. I guess this solves the gotchas I'd thought of in this regard. I  
> knew that
> people weren't happy with Agda's having non-parametric  
> quantification over
> levels for use in Sets. However, I had thought that even without case
> analysis, you could do the following:
>
>  embed : Nat -> Level
>  embed zero    = zero
>  embed (suc n) = suc (embed n)
>
>  f : (n : Nat) -> ... embed n ...
>  ...
>
> and regain non-parametric quantification (by analysis on Nat), even  
> without
> eliminators for Level. But, if Level is always irrelevent, embed is  
> not a
> valid function (if this is anything like erasure pure type systems *).
>
> My own thoughts on the issue were a bit wackier. I've been  
> interested in
> EPTSes for a while, and came up with a way (I think), to extend them  
> to
> provide some solutions. The EPTSes in the linked paper are presented  
> as having
> function space rules like ordinary pure type systems. But, what if  
> we allowed
> them to know whether irrelevant or relevant quantification is being  
> performed,
> too (and for universe polymorphism, tell it what variable is being  
> bound)?
> Then rules are of the form (sticking to functional relations):
>
> (var, phase, sort, sort) -> sort
>
> (that may not be an ideal presentation of the rules, but it should  
> suffice)
> The ordinary part of the hierarchy would go:
>
>  (v, _, Set i, Set j) -> Set (lub i j) if v is not free in j
>
> And for universe polymorphism, we can add:
>
>  (v, c, Set i, Set j) -> Setω if v is free in j
>
> The important part being that this only allows computationally  
> irrelevant
> function spaces to be used for universe polymorphism. This means  
> that embed is
> now valid:
>
>  embed : Nat -> Level
>  Nat : Set 0, Level : Set 0
>
>  rule (_, r, Set 0, Set 0) = Set 0
>
> But, when we go to try and use it to enable non-parametric universe
> dependence, we fail:
>
>  f : (n : Nat) -> ... T : Set (embed n) ...
>  f zero    = ...
>  f (suc n) = ...
>
>  Nat : Set 0, T : Set (embed n)
>  rule (n, r, Set 0, Set (embed n)) = error
>
> So, appropriate behavior is not ensured by making Level itself  
> inherently
> irrelevant, but by ensuring that only irrelevant things (regardless  
> of type)
> are used in universe polymorphism. For instance, we could instead  
> write
> (using, I think, similar notation to the irrelevance stuff you've  
> proposed for
> Agda):
>
>  g : .(n : Nat) -> ... T : Set (embed n) ...
>  g n {- no case analysis -} = ...
>
> (I also have another idea of where the above style rules could be  
> useful. **)
>
> > Note that Setω is not part of the Agda syntax, it is used
> > only internally, and plays the role of "Type" in the Martin-L"of
> > logical framework.
>
> I know. Although, I think it could be useful (and non-problematic)  
> to allow
> talking about it. I have my own simple interpreter for fooling with  
> Agda-like
> universe stuff (without the irrelevance stuff I mentioned above; I  
> haven't
> gotten around to implementing something with all that yet), and it  
> allows
> sigma types like:
>
>  (Σ i : Level. Σ T : Set i. T) : Ω
>
> (incidentally, I also think a type not of the form SetN is kind of  
> appropriate
> as a top, because Setω kind of makes ω look like a Level.) But you  
> cannot
> construct a similar type in Agda:
>
>  data All : Setω where
>    con : (i : Level) -> (T : Set i) -> T -> All
>
> because that "Setω" is an error. Yet for any All -> T, the  
> corresponding
> curried function is allowed.
>
> > I think we have a systematic and fairly simple solution to the  
> > problem
> > of universe polymorphism.
>
> I do like it. Making universe levels (roughly) ordinary, first-class  
> values
> seems simpler and more natural than a lot of other proposals I've  
> seen. But I
> can understand people being a weirded out by, essentially, Set being  
> a family
> that contains its own index/parameter type.
>
> -- Dan
>
> [*] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.156.2558
>
> [**] One redundancy of EPTSes is that quantification on Sets is  
> probably
> naturally parametric when doing (x : Set i) -> (T : Set j) i > j  
> stuff. It is
> in Agda, I believe. You could solve this redundancy by adding type  
> case as a
> language primitive. Then parametric quantification would ensure that  
> type case
> isn't used, and types could be erased.
>
> But, you could also use the above rules to disallow using the ordinary
> function space where it's necessarily parametric, like so (ignoring  
> variables
> for now):
>
>  (_, Set i, Set j) -> Set j if i <= j
>  (c, Set i, Set j) -> Set i if i >  j
>
> And now we can no longer write:
>
>  id : (A : Set) -> A -> A
>
> only:
>
>  id : .(A : Set) -> A -> A
>
> Forcing us to tag all the Sets that can be erased. I'm not actually  
> certain
> this is useful, since it imposes an additional burden on the  
> programmer to
> provide information the compiler could figure out, but it might be  
> interesting
> in an intermediate language.

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel AT ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/