- Jesper Cockx has a new paper out with students of his at ICFP that involves, presumably, Agda and dependent types
- I have only ever presented papers at reading group in which he is one of the authors
- There is one last reading group left before I leave
What if... What if...
I suppose I could skim it over a bit rn to see if it's something I could decently understand well enough in a week
Oh this sounds very cool
I was gonna say NoConfusion looks v handy for the ordinals stuff I was doing, but I just remembered I didn't need it in Agda, only in Coq, since pattern matching takes care of things for me
Practical Generic Programming over a Universe of Native Datatypes
Wait wait wait. What about inductive–inductives
Practical Generic Programming over a Universe of Native Datatypes
Me: it's so annoying when reviewers ask about things clearly outside the scope of the paper
Also me: immediately starts asking about things clearly outside the scope of the paper
Practical Generic Programming over a Universe of Native Datatypes
oh it's not true that I've only presented papers with Cockx on them. I did TTobs I think
Practical Generic Programming over a Universe of Native Datatypes
Induction–recursion with functions to universe levels?????
Practical Generic Programming over a Universe of Native Datatypes
I just noticed that universes are basically cumulative with respect to Set omega, like every Set is in Set omega despite then being predicative otherwise
Like. What.
re: Practical Generic Programming over a Universe of Native Datatypes
I'm spending so much time on telescopes bc this is so confusing lol
re: Practical Generic Programming over a Universe of Native Datatypes
Okay this ConDesc thing is on clever. It took me way too long to figure out what it was doing but somehow this is indeed the correct grammar for describing strict positivity
I think it would've been helpful to give a little... diagram? Illustrating how it looks nondependently
Like my notes rn look like
A ::= X (var)
| S -> X (pi)
| A -> A (otimes)
where X is the recursive argument and S is an arbitrary type (not incl. X since it's not in scope technically)
re: Practical Generic Programming over a Universe of Native Datatypes
The interpretation of datatype descriptions is incredibly confusing omg. What's going on
re: Practical Generic Programming over a Universe of Native Datatypes
ω×ω WHAT is this thing. what is it. Agda explain yourself
re: Practical Generic Programming over a Universe of Native Datatypes
I literally don't know how to search for this lmao
re: Practical Generic Programming over a Universe of Native Datatypes
It's a Setω pair type. ok
re: Practical Generic Programming over a Universe of Native Datatypes
I'm still not sure why Agda needs Set2ω
re: Practical Generic Programming over a Universe of Native Datatypes
@ionchy Set\(\omega\) seems illegal
re: Practical Generic Programming over a Universe of Native Datatypes
@wilbowma one day I'll know enough to finally understand Kovacs' LICS 2022 paper to convince myself that all this kind of universe trickery is legal but today still isn't that day
Practical Generic Programming over a Universe of Native Datatypes
Great now I gotta focus enough to read it through without getting distracted by how much levels look like sizes