Arnaud Spiwack

Il se trouve qu'en l'occurrence, les leap seconds ne changent rien au propos. Parce qu'en temps POSIX un jour fait exactement 86400s. Qu'il y ait eu une leap second ou pas dedans.

After 6 years of sitting on the GHC steering committee, my second term is officially over and I haven't sought re-election. It's been a demanding engagement, certainly, but one that I enjoyed a lot. 🙇

A figure demonstrating the different aspects of the corpus described in the tweet. There is a main isomorphic 3D view of a level in the Portal 2 co-op game, with some portals, lasers, and the blue and orange players. Inset, there are first-person captures of the blue and orange player views. There is also a box containing the transcribed dialogue with timestamps and labels for the discursive acts. Finally, there is a box containing a task and a list of subtasks. Some subtasks are already crossed out, with the time that they have been completed. The last subtask ("Player 2 places portal 4 on wall 4") is marked incomplete. The dialogue is as follows: Blue: Can you put your other portal up here? (tagged as directive) Orange: Where? (tagged as request for clarification) Blue: On uh, on this wall. (tagged as directive) Blue: So that it uh points at the circle. (tagged as directive) Orange: Okay. (tagged as commit) The full list of subtasks is: Task: Redirect lasers Subtask: Player 1 places portal 1 on wall 1. (completed) Subtask: Player 1 polaces portal 2 on wall 2 or 3. (completed) Subtask: Player 2 places portal 3 opposite of portal 2. (completed) Subtask: Player 2 places portal 4 on wall 4. (incomplete)

A couple years (!) in the making: we’re releasing a new corpus of embodied, collaborative problem solving dialogues. We paid 36 people to play Portal 2’s co-op mode and collected their speech + game recordings.

Paper: arxiv.org/abs/2512.03381
Website: berkeley-nlp.github.io/portal-dialo...

1/n

Indefinite Hyperbolic Numerals
forty-leven
squillion
umpteen
steen
umpty
umpty-ump
umpty-steen
zillion
skillion
jillion
gillion
bazillion
umptillion
kazillion
gazillion
kajillion
gajillion
bajillion
Collected by Stephen Chrisomalis
www.futilitycloset.com/2025/12/05/e...

Le pilier bizarre à Massy. Photo : voie d'autoroute au-dessus de laquelle passent 2 autres voies. L'un des piliers a des bras en trop. Commentaire : L’autoroute A10 devait se prolonger jusqu’à la gare Montparnasse et croiser l’autoroute A87 qui aurait relié Versailles à Évry. L’échangeur n’a jamais existé, mais les piles du pont de l’A126 le prévoyaient : d’où ces « bras » inutiles pour une future bretelle.

#Avent2025 2/24 À la recherche des traces des Trente Glorieuses, toujours présentes dans le paysage... Avez-vous déjà vu le pilier bizarre à la sortie de l'A10 à Massy? Maintenant, oui :-)

Bref: ne soyez pas déçu. Presque or otherwise.

Je pense que vous ne vous rendez pas compte… 7m³ d'or c'est 135 *tonnes* d'or.

C'est vraiment gros un mètre cube.

Yet, I think that with a little bit of elbow grease, we could make this work for us. 11/11

…presheaves where all the restrictions are the identity); not sure if there's an issue when we need to apply a modality (like (,Δ)*) to the bottom row (e.g. intuitionistic variable rule); I don't even know how to phrase the linear variable rule in this setting. 10/11

Dubious stuff: this is new and we'd need to build an understanding of what's permissible and what's not, lest we resort to low level reasoning all the time; u v `let x=u in v` aren't actually terms, they're local sections (possible solution restrict ourselves to… 9/11

Good stuff: most redundant context is gone, structural rules are handled quite formally; structural rules and subtyping of context are preserved by definition (like a declarative system), yet the rules are syntax directed (like an algorithmic system) 8/11

The category of presheaves has enough limits and colimits that such recursive definition should make sense. 7/11

One more piece of material. Contexts Γ can be extended with Γ,Δ (usually partial). Let's write Δ⊢u:A for (u,A)∈(,Δ)*T, where (,Δ)*T(Γ) = ∃Ω, Ω→(Γ,Δ) × TΩ.

So we can make sense of

u:A x:A⊢v:B
-----------------------
let x = u in v : B

6/11

The idea is that a rule
u:A v:B
----------
w:C

is interpreted as a partial natural transformation T⊗T->T.

If the category of context is Cartesian, then this is a Cartesian product too. In substructural logics, we will need some notation for additive hypotheses. 5/11

For typing, we write u:A for (u,A) ∈ T (itself a notation for local sections of the T presheaf that we're defining). 4/11

Then our typing rules, instead of defining a relation (i.e. a set of tuples), define a presheaf over contexts (i.e. a family of sets of tuples with one fewer elements). 3/11

The category of contexts encodes the structural rules (including subtyping if there's any). In particular for an intuitionistic calculus, it would be Cartesian (maybe partially so). 2/11

This whole presheaf story gave me an idea. Contexts, in inference rules, are distracting. Let's see if we can use presheafs to get rid of them.

Step 1: let's have a category of contexts. It needs a symmetric monoidal product (it's fine if it's a partial product I think). 1/11

Because wanteds' semantics is existentially quantified. There needs to be a G⊢W such that 1/ we can solve such problem 2/ if W is generated by the typechecker and G⊢W then there's a type assignment in a more declarative type system.

By using the presheaf toolbox, we can save ourselves a few lemmas.

Ultimately, I don't think we can extract big principles from that. Because we really care about wanteds' syntax for constraint solver to solve (e.g. the lhs and rhs of implication usually have different syntax).

What it can buy us is not having to define a semantics for wanteds.

Here's how I think you do scaling. You have a semiring of multiplicities and an action of multiplicities on the category of given constraints (in the sense of actegories).

Then you lift the action to presheaves with π.P(X) = ∃Y. (X -> π.Y) × P(Y)).

Day-convolution-like, but for an action.

I don't remember the 90s adaptation of Ranma½ very much. But I remember it being very slow. The new adaptation running these days is really good, I'm enjoying it a lot. The pacing is nice. And it's aesthetically quite interesting. It's a readaptation that has a reason to exist.

Case de BD A quoi pourrait ressembler une guerre entre les raies et les girafes ? (Des raies et des girafes qui se bastonnent)

Je lis une bédé de Sophie Guerrive à mon môme et elle répond vraiment aux vraies questions

Link to omni-tools for self-hosting. The presentation isn't quite as friendly but you may prefer it. omnitools.app

After sharing, I noticed that there was an English version of this website. A collection of convenience and conversion tools (such as pdf editing, image conversion, …) hosted by free software association Framasoft. Based on the omni-tools suite, apparently.

framatoolbox.org/abc/en/

Framatoolbox La boîte à outils libre et éthique

Vous avez déjà certainement utilisé des services bourrés de pubs pour découper un PDF, convertir une image ou supprimer l'arrière-plan d'une image.

Framatoolbox vous propose une énorme boîte à outils gratuite et sans pub

framatoolbox.org/abc/fr/

Maybe I should have clarified that I was speaking about programming language semantics, not about how you can see constraints within Haskell. The latter may be what you're thinking about?

Well, it's not unique a priori. It's just that in one given context, you only consider a subcategory that you require to be an order.

But semantically, any function Q->Q' is a proof that Q⊩Q', so entailment is really proof relevant.

Forgot to point out: while the papers all focus on entailment as a relation (an order) for simplicity of the exposition. In practice, entailment is proof relevant since it constructs dictionary passing. So it's really best to think of entailment as a category.

What we need to prove, then is a natural transformation between two presheaves (whereas without quantified constraints we wanted to prove C(G)). The Yoneda lemma gives us that this behaves as expected when givens/wanteds are simple.

I think.