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.
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.
Comments
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.
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.
Corresponding paper is probably http://people.csail.mit.edu/kostas/papers/CADE1996.pdf. Thanks for the name drop, looks great