1. Jesper Cockx has a new paper out with students of his at ICFP that involves, presumably, Agda and dependent types
2. I have only ever presented papers at reading group in which he is one of the authors
3. 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.

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

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ω

@ionchy oh yeah I've read that

@ionchy Set$$\omega$$ is bonkers I don't understand it.

@wilbowma already?? he announced it like yesterday

@wilbowma oh right you're ICFP VIP

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

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.