Practical Generic Programming over a Universe of Native Datatypes
Induction–recursion with functions to universe levels?????
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)
A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.