4 ms·
Not true at all. It is hard, but not impossible. Technologically it's very challenging because we don't have non-TC programming languages that are able to keep
by gnulinux 5y ago
Not true at all. It is hard, but not impossible. Technologically it's very challenging because we don't have non-TC programming languages that are able to keep up with modern ones. But, for example, we have (safe) Agda which is not TC (all programs marked --safe should prove to halt) and you can write useful programs. Here, "useful" is a subjective qualifier, but I personally implemented many parsers in Agda (including a json parser) so for my definition of useful, Agda is one such language.
- lisper 5y agoI 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.
- JonChesterfield 5y agoCorresponding paper is probably http://people.csail.mit.edu/kostas/papers/CADE1996.pdf http://people.csail.mit.edu/kostas/papers/CADE1996.pdf. Thanks for the name drop, looks great
- gnulinux 5y agoI'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.