I've just solved a problem using a concept from my thesis that I rejected as useless at least 10 years ago. So that's nice...
-
Show this thread
-
If you're interested: The concept being "detaggability" of constructors, and the problem being how to know whether an argument is erasable even if we're pattern matching on it.
3 replies 1 retweet 18 likesShow this thread -
Replying to @edwinbrady
This here that caught my eye earlier in a Github notification?: https://github.com/edwinb/Idris2/commit/04e4ebf80e4464c87c578739aa5d91fa0dd1a509 … It’s interesting for sure!!
1 reply 0 retweets 0 likes
Replying to @kristleifur
I really need to write this up. I might even have accidentally done some research on the way.
1:30 PM - 21 Jan 2020
0 replies
0 retweets
2 likes
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.