iiinova — where your digital self keeps evolving

In fact, you never even need any syntax for terms. So, my understanding about the double-negation monad above was wrong. Still, the `>>=` seems quite central. Is it quite central?

100

Wow! Without any unsafe coerce? Very impressive. The price you seem to pay is to have to use `>>=` in a double-negation monad (I haven't actually figured out why it comes up). Does the explicit context help? The traced category via recursive do is quite the flex.

100

I think you want to think of it as the ability to do crazy functions. Also combined with intersections and union types, it could let you specify more behaviour. Finally, maybe it can be read as “tell me if there's definitely a bug” (as opposed to “tell me if it isn't definitely correct").

It captures a common duality in formal method (guarantee of correctness vs guarantee of a bug). Though it leaves me wondering: what is A? An actual value of type A, maybe?

100

[ICFP SRC'26] Better Safe and Sorry: Tabular Types for Dynamic Languages

I quite like the idea in this talk (I couldn't find a matching paper) www.youtube.com/watch?v=5bHR... to distinguish type □ A (computes a value of type A) and type ◇ A (computes a value of type A OR has a type error).

youtube.com

Better Safe and Sorry: Tabular Types for Dynamic Languages (Video, ICFP 2026 SRC) Vincent H. Chan, Matías Toro, and Qianchuan Ye (University at Buffalo, SUNY; University of Chile; University at…

120

So the actual question is: is there a way to arrange LensFL and TravFL so that defining a lens or traversal is essentially the same as the van Laarhoven style? I'm willing to specialise the category to Hask (or, as a random non-specific example, to LinHask).

110

I think (but I'm not sure) that your definition of flavours LensFL and TravFL don't seem to allow for (approximatively) the same definition. LensFL looks close to what's needed but TravFL looks quite far, and closer to traditional profunctor style optics. Admittedly, my head isn't yet fully wrapped.

100

Serious question: the “right way” to define a particular lens or traversal, in Haskell, is using the van Laarhoven style. In both case it has the least amount of ceremony and of allocations. The traditional profunctor style is quite bad at that, especially for traversals.

110

This is quite elegant. I've got a trivial remark and a serious question. Trivial remark: I believe you forgot to include a definition of MonTravFL in your list of definition (you refer to it below, but it's not there).

110

Most of the time, I feel that they diminish the game. Not here though. I found myself relishing almost every single line. Looking forward to more lines of dialogue. What a treat! 4/4

000

It's well worth playing: the presentation is truly excellent. The visual design is good, the animation is good, the writing is excellent, the VOICE ACTING is excellent. If you know me, you probably know that I constantly complain about voice acting in game. 3/4

100

I would describe it as an interactive detective novel; it's not a true detective game like Obra Dinn, as the game is in charge of most of the exposition. It has a bit of a old-style Point&Click adventure game feel (but it's not really one such either).

100

It's game day apparently. I want to shout out the Mermaid's Mask. It's the third Detective Grimoire game (I haven't played the two first ones).

100

This is unfortunate, but mostly I wanted to share this rather peculiar bug, which I found rather funny.

000

But when I launched the game again, the game crashed before even reaching the title screen. So I can't even attempt the superboss which is behind the platforming challenge (and in fact, the only way to play the game at all is to erase my entire save data).

100

It wasn't happening at first, somewhere along the way, my save got corrupted (probably) and I stopped getting achievement and got crash instead. So when I completed the hardest platforming challenge, the game crashed, as expected.

100

I eventually figured it out: the game had started crashing every time it would give me an achievement (and I wouldn't get the achievement, but the game was saved, so I could continue from there).

100

Anyway, I decided to sit down and finally do a 100% playthrough (on the Switch 2). When I started reaching close to the end, I started hitting a peculiar bug, whereby the game would crash at the end of some fights.

100

Arnaud Spiwack @aspiwack.bsky.social · 02/10/2026

The first time I played Worldless, I didn't do anywhere near a 100% run. Aside: if you're intro metroidvanias at all, this game is a must play: it's a very unique and delightful take on the genre (and did I mention gorgeous?).

100

But it's really becoming uniquely strong now, leveraging the multi-language support for new features. To the point that it may eventually be worth moving to Topiary even if you already have a dedicated formatter for your language. (and, to be clear, I've got nothing to do with it, congrats team!)

030

Arnaud Spiwack @aspiwack.bsky.social · 02/10/2026

When we came up with Topiary our goals weren't too ambitious: make it cheap to write decent formatters for new languages, reducing the amount of stuff you have to maintain.

100

Arnaud Spiwack @aspiwack.bsky.social · 01/10/2026

One year later. I found this proposal dl.acm.org/doi/full/10.... . Idea: add a rule e⇓e to big-step semantics. Except you can't do that, because most rules only make sense when you evaluate to a value. So you do the dual thing: allow big-step under (unevaluated) evaluation contexts.

dl.acm.org

Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment | Proceedings of the ACM on Programming Languages

As is evident in the programming language literature, many practitioners favor specifying dynamic program behavior using big-step over small-step semantics. Unlike small-step semantics, which must dwe...

Arnaud Spiwack @aspiwack.bsky.social · 30/09/2026

Certainly a challenge is to make this observation less handwavy. The program doesn't blow up if you use a seed several times. It just doesn't have the desired distribution. But… what is the desired distribution? Does linearity show up in the semantics of probabilistic programs?

000

Arnaud Spiwack @aspiwack.bsky.social · 30/09/2026

“Of course”, the order on relations falls from the decategorification of squares, which are oriented. So it is, indeed, free in the formalism. What's added on top of proarrow equipments, in the nlab page, is the involution on relations.

001

Arnaud Spiwack @aspiwack.bsky.social · 30/09/2026

Something popped back up from the back of my mind. Splitting random-number generators seem to be an example of linear comonoid. In that it's imperative that you don't use the same seed twice. And the natural associated monad is a linear reader monad.

000

Arnaud Spiwack @aspiwack.bsky.social · 29/09/2026

Quick life update. After 11 years almost to the day, I no longer work for Tweag. It's a rather emotional moment for me, but it was time to move on.

3140

Arnaud Spiwack @aspiwack.bsky.social · 28/09/2026

I didn't. I saw it more as a theoretical device.

Arnaud Spiwack @aspiwack.bsky.social · 28/09/2026

Over 10 years ago, I wrote a sweet little article entitled “The tree machine” arxiv.org/pdf/1507.04589 (it was rejected for not being novel enough, but I still like it). Anyway, it wasn't until today that I realised that these machines are more or less a first-order system L.

arxiv.org

https://arxiv.org/pdf/1507.04589

111

Arnaud Spiwack @aspiwack.bsky.social · 24/09/2026

In my – somewhat vain – attempt to understand what's going on in these days with remakes which often seem to be slightly worse that the original I found this video. It doesn't really help, but it's still rather interesting (if quite long) www.youtube.com/watch?v=mIHO...

youtube.com

Un-Artistic Game Remakes

Video game remakes offer a mixture of emotions from excitement to skepticism. Because while we love to see our favourite games reborn into the modern era, sometimes the delivery is...…

Arnaud Spiwack @aspiwack.bsky.social · 22/09/2026

Maybe “the late 19-naughties”. It's a little awkward, but it's somewhat regular.

000

Arnaud Spiwack @aspiwack.bsky.social · 22/09/2026

So language is more of a topology on the set of people. And choosing a set of languages is committing, somewhat arbitrarily, to a particular partition (and subpartitions if you want to include dialects)

000

Arnaud Spiwack @aspiwack.bsky.social · 22/09/2026

As a complement to this excellent (as always) video by the Map Men, linguists recognise that each individual speaks slightly differently. Your particular way of speaking is called your idiolect. www.youtube.com/watch?v=hX21...

youtube.com

Why a Language Map of the World is Impossible

🦈 Go to https://surfshark.com/mapmen or use code MAPMEN at checkout to get 4 extra months of Surfshark VPN! See new episodes early and exclusive bonus content https://patreon.com/mapmen 📕…

130

Gro-Tsen @gro-tsen.bsky.social · 21/09/2026

I'm not allowed to work out maths for another week or so. So just recording the question that this left me with: are operation which are independent from a choice of base (i.e. natural in the category of vector spaces) the same as those stable by invertible matrix (group) conjugation. Sounds likely.

000

Reposted by Arnaud Spiwack

I'm not sure what the best answer is, but one thing I am sure about is that this is a great question, and we should encourage students to ask these sort of things. Definitions in mathematics have reasons: don't accept them blindly, but be willing to ask “why did we do this and not that?”!

393

Reposted by Arnaud Spiwack

lpora.bsky.social @lpora.bsky.social · 21/09/2026

Les questions importantes : tous les kebabs tournent-ils dans le sens direct ? Sinon quelle est la répartition des sens de rotation ? Y a-t-il des gens capables de reconnaître au goût un kebab trigonométrique d’un kebab horloger ?

10466

But if someone speaks for too long, I eventually lose track as my buffer fills up. I suppose I have to apply some back pressure in the form of asking people to repeat. 2/2

000

When I speak Japanese, I experience the same sort of limits that computers have. E.g. I understand slower than people speak (when I understand at all), but I eventually understand. The longer the sentence, the later I understand. I'm being CPU bound. 1/2

100

Arnaud Spiwack @aspiwack.bsky.social · 20/09/2026

Dans la série aussi: chouiner que Google a plus de capacités d'espionnage que l'État. Et demander à avoir pareil...

020

Enola Holmes 3. Well, it's about as well put together as the first two. However, the screenplay is significantly weaker (dare I say lazier?). So while it's still quite pleasant a watch (the children loved it), it doesn't have the charm of its predecessors. Ah well…

001

Arnaud Spiwack @aspiwack.bsky.social · 20/09/2026

By the way, “effable machine” is the name of my next punk rock band.

011

Arnaud Spiwack @aspiwack.bsky.social · 20/09/2026

You scared me for a minute. That being said Echos of Wisdom isn't really taking the series in a good direction. Aonuma direct have a lot of appreciation for what made the series good. So the series that I loved Matt very well be truly dead and buried for me at this point.

Arnaud Spiwack @aspiwack.bsky.social · 19/09/2026

And, yes, of course I'll watch Hercule. Who do you think I am? Someone with any willpower at all?