[lisper]

I didn't say it was impossible. I said it was nearly impossible, which is a synonym for "hard" for some value of hard.

Case in point: I looked into Agda and ended up in a deep rabbit hole that involved something I had never heard of called "Walther recursion." Whether this qualifies as "nearly impossible" or merely "hard" is quibbling over terminology, not substance.

[gnulinux]

I've been writing programs in Agda for years (since when they didn't have sized types or cubical theory) but I never heard "Walther recursion" before. If this is your day 0 I doubt you need to know about it to understand the language.

[JonChesterfield]

Corresponding paper is probably http://people.csail.mit.edu/kostas/papers/CADE1996.pdf. Thanks for the name drop, looks great