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.

Show thread

I find myself, again, wishing for an English word quite as concise as the Go term "aji".

It means, more or less, possibilities that might come into play later depending on things that happen in the mean time.

I bet there's a German word for it...

The auto captioning software has turned "this semester" into "this mission" and honestly I don't want to correct it. (I did though).

Show thread

I've reached a point in lecture recording editing where I either no longer hate the sound of my voice, or I've just accepted that's what it is. Good, I think?

(Also I know what my students have to listen to now... sorry...)

"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."

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!

Show thread

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.

Show thread

Definitely not at all stressful for my internet connection to fall over in the middle of advising incoming students...

I've turned it off and on again lots, but the solution seems to be to balance everything so that gravity can't cause the cable to fall out by a nanometre.

Tricky language, French. It took me four goes to get this one right.

I think that's 2/3, in practice. I bet you can't guess who had an Idris submission rejected...

Show thread

Apparently Idris is among the topics with the highest acceptance rate at ICFP. So, better get cracking for next year :).

I seem to be shouting "Stop calling it an 'algorithm'" at the radio a lot at the minute.

If you're missing SPLV but want to follow along anyway, I'm putting materials up here:

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:

(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:

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...

Show thread

If you've more or less written the program in the type, you shouldn't have to write it again in a function. Here's an example I made earlier.

This (program search from type) might almost be starting to be useful... here's the bind operator for the continuation monad.

At least I hope it is. It type checks :).

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.

Show thread

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!

Show thread
Show more

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!