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

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

Follow

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ω

Sign in to participate in the conversation
types.pl

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