Related: "aji keshi" eliminating possibilities needlessly early.
Kind of like (tech analogy) committing to a design before you know what all the requirements are.
I'm just going to have to start using these phrases in everyday conversation.
The auto captioning software has turned "this semester" into "this mission" and honestly I don't want to correct it. (I did though).
"So," said the technician, "what seems to be the problem?"
"My batteries are drained much faster than normal."
"Ah. That's common these days."
"Is it a virus?"
"Input overload. Too much news to process."
"But I can't stop caring!"
"No. But care for yourself and limit your input."
#MicroFiction #TootFic #SmallStories
Thanks to @aaisp for shipping me a new router straight away, so I no longer have to rely on Lego to keep myself connected to the world!
This was what I had handy. I've no idea if this is helping but I'm terrified to touch anything now in case it is.
I used to know about computers, you know.
I think that's 2/3, in practice. I bet you can't guess who had an Idris submission rejected...
If you're missing SPLV but want to follow along anyway, I'm putting materials up here: https://github.com/edwinb/SPLV20/
Videos will come soon (though with the warning that it's the first time I've tried teaching this... if I'm allowed to try again at some point, it'll be better :))
Sometimes people complain that without type inference you need to annotate every subterm. Well... this is what happens if you need to annotate all the variables: https://gist.github.com/edwinb/029dd3e8e78855e47110fd6f9d27f696
(This is TinyIdris, for next week's SPLV course. It will get slightly nicer by lecture 4 :))
To appear in ICFP, @id1660 explains erasure and dependent types: https://dl.acm.org/doi/10.1145/3408973
Hopefully also to appear in Idris 2+n in some form. We'll see :).
I am naturally tuning this for specific examples, but I guess if it works for those specific examples, then it'll work for some of the things I haven't though of too...
Thanks to a suggestion by @Augustsson (generate some candidates then sort by fraction of bound variables used) it gets the right answer much quicker now.
It's interesting to see where it goes if you make the lists linear. The first answer is the right one here...
In other news, TIL you can record and edit your screen in Linux. What is this sorcery!
CS Lecturer at University of St Andrews
Server run by the main developers of the project It is not focused on any particular niche interest - everyone is welcome as long as you follow our code of conduct!