Oh fuck that. I'll not be sending them my business, and I suggest yourselves do the same.

Why have I never cooked sized types with ornaments? I'm a numpty!

shop talk

Today I got around to writing
UNION : Products ((THIN ^op) \\ ga)
and
INTERSECTION : Products (THIN // ga)
I challenged myself to a dual.

I don't know what's going on with the Stranger Things thing. Yes, it's funny. But I struggle to believe it's even an anachronistic reference to Epigram as in me and Jimmy Mac.

"In the Lubyanka, the KGB guards wake up the political prisoners every morning with a fresh bucket of cold urine. When you email me, you piss in that bucket."

Programming language design works by the recognizable postmark on your Dear Santa letter.

Ahh so that's how Agda is designed

If you want to be clear about the quantifier alternation in a theorem represented by a categorical diagram, consider it to be built stepwise, where even steps are universal and odd steps existential.

Minimally write step number labels on things which arrive strictly later than their boundaries.

E.g., to illustrate the existence of composites, draw a triangle with A -> B -> C (phase 0 poses the problem) and A -[1]> C (phase 1 delivers the solution).

MSP101 tomorrow 1300 UTC+1

Plans are laid: msp.cis.strath.ac.uk/msp101.ht

There will be binomial coefficients, bit twiddling, and double categories for beginners like me. All happening live in LT1310 and on zoom if you know where to find us.

Binomial coefficients (m choose n) can be seen as the types of bit vectors with length m, exactly n of which are 1. You can see them as string diagrams from bottom to top, where 1 denotes a wire and 0 connects up but not down. I use them to keep a vice-like grip on variable scope.

Am distracted by laughing my tits off at the Stormont elections. It may take me some time to recover.

Night, folx!

Every US state gets two senators. Can states subdivide?

Your satnav never says (out loud) "If you're going to ignore me, I don't see the point of persisting with this relationship.".

That whole other voice that says what your polite satnav is really thinking.

Do we have a standard written convention for quoting stilted, stitched-together utterances composed by machines from snippets recorded by humans?

"We are/sorry/to announce that/the/six/thirty-seven/CrossCountry/service to/Penzance/is currently running/eleventy/twelve/minutes late./We are laughing our/socks/off."

this is a test

and this is the meaning of the test

The price one must learn to pay for proof irrelevance is, funnily enough, not caring what the proof is.

The trick, when you can work it, is to replace inspecting the proof by inspecting the proposition it allegedly justifies. If that proposition is sufficiently plausible, perhaps you can make progress without looking at the proof. Coercion between structurally equal types works just fine on that basis, because "plausibility" is types having the same type constructor.

When is a termination proof plausible enough to allow computation to proceed?

I'm now wondering whether it's worth trying to be clever with some codeBruijn piggery-jokery. Once you cease to be indiscriminately anxious, you might be correspondingly discriminate in your search for reassurance.

By way of further displacement, I rewrote my anxiety-based Boolean prover in Haskell, with a fancy representation for anxiety. github.com/pigworker/Samizdat/



humpty :: (Newtype n o, Monoid o) => n
humpty = pack mempty

(<^^>) :: (Newtype n o, Monoid o) => n -> n -> n
x <^^> y = pack (unpack x <> unpack y)


Show older

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.