glaebhoerl @glaebhoerl@schelling.pt

New blog post! Learning Jai via Advent of Code.

This is a pretty lengthy summary of my early impressions.

https://www.forrestthewoods.com/blog/learning-jai-via-advent-of-code/

I'm a little nervous posting this one because it's the kind of topic where people have, ahem, strong opinions. Be kind y'all.

Dear everybody re ChatGPT etc,

The word you need that you don't know you need is CONFABULATION.

What y'all are calling "hallucination" is, in neurology and psychology (where it means two slightly different things) called "confabulation".

I means when somebody's just making up something and has no idea that they're making things up, because their brain/mind is glitching.

A lot of folks are both trying to understand the AI chatbots and are trying to grapple with the possible implications for how organic minds work, by speculating about human cognition. Y'all should definitely check into the history of actual research into this topic, it will make your sock roll up and down, and blow your minds. And one of the key areas will be surfaced with that keyword.

There have been a bunch of very clever experiments that have been done on humans and how they explain themselves which betrays that there are parts of the mind that are surprisingly - and even alarmingly - independent.

Frex...

There are several very closely related calculi which have the same or very closely related models given by strong adjunctions or strong monads:

- Moggi's monadic metalanguage
- Filinski's Effect PCF
- Levy's call-by-push-value
- Egger-Møgelberg-Simpson's effect calculus and its extension to the *enriched* effect calculus
- There's probably an explicitly polarized L/mu-mu~ calculus that fits here but I'm not as aware of the literature there.

There are also things like Moggi's computational lambda calculus and some L calculi that are related but have implicit evaluation order.

The distinctions seem to be as follows:
- Moggi's monadic metalanguage has only value types, an abstract monad on them, and pure terms.
- Filinski's Effect PCF adds a value type-computation type distinction, but computation types are a subset of value types. So there is a coercion of value types into computation types but the reverse coercions is implicit. There is still only one term judgment, again pure terms
- Levy's CBPV adds to Effect PCF two new judgments: computations and stacks. Additionally, CBPV makes value and computation types disjoint: there are explicit coercions in both directions U B and F A.
- EMS's effect calculus has value and computation types, but two judgments rather than three: pure terms (~ values in CBPV) and linear terms (~ stacks in CBPV). Additionally, like with Effect PCF, computation types are a subset of value types, but there is an explicit coercion to make any value type into a computation type: ! A. The *enriched* effect calculus is just an extension to support the rest of the definable multiplicatives/additives that CBPV intentionally leaves out for operational reasons. For instance we get value types of pure functions and linear functions and an "action" of value types on computation types.
- L calculi are based on sequent calculus judgments, whereas the above are all natural deduction style, i.e., lambda-calculi. Not sure where they fall on the implicit coercions.

Unfortunately for me, this means that one of the variants of the calculi that I like doesn't have a name: explicit coercions like in CBPV, but supporting all of the multiplicatives and additives like in EEC. I can't call this CBPV because it doesn't have the simple operational semantics and I can't call it EEC because it is syntactically quite different.

The most natural term for this to me would be *unary Linear-Non-Linear Logic*, as it corresponds to restricting the linear judgments of intuitionistic Linear-Non-Linear Logic to always have precisely one linear variable. But I feel conflicted about using such a name because I would like to honor the prior work of especially Levy/EMS. There is also the additional subtlety that CBPV really corresponds to something like *stoup LNL* or in Shulman's terminology *sub-unary, co-unary LNL* where linear terms can have either zero or one linear variable, but without weakening: one variable corresponds to Levy's stacks, zero corresponds to Levy's computations.

But I think we should re-organize this terminology now that we have a better scientific understanding. In my opinion, we should give a name to the *judgmental structure* of a calculus, and then which choice of connectives should be given by modifiers.

New bloggery on Whippet, the garbage collector I have been working on for the last year or so ~~ https://wingolog.org/archives/2023/02/07/whippet-towards-a-new-local-maximum

bonus bag fact #2: if

list x = 1 + x + x^2 + x^3 + x^4 + ...

and the distinction between lists and bags is that in a bag you forget the order, i.e. you quotient out a permutation, then

bag x = 1 + x + x^2/2 + x^3/3! + x^4/4! + ...

so

bag x = e^x

and if you calculate the derivative of bag x (i.e. the one-hole context of bag x), it is indeed bag x.

....

but wait, bag unit ≅ nat, so,

does this mean that e is nat???

"A New Drug Switched Off My Appetite. What’s Left?" by @ftrain is well worth reading: https://www.wired.com/story/new-drug-switched-off-appetite-mounjaro/

Every online discussion of weight and obesity ends up being an argument about this: "But it’s a side effect of what I am, which is insatiable. Literally: I never seem to feel full."

It was a surprising realization to me, sometime in my teens, that some people stop eating when they are "full", rather than as an act of will or of running out of nearby food.

it looks like you have a cool new idea. have you tried thinking about it over and over again without actually implementing it?

@glaebhoerl a doodad is just a k-regular quasi-endo-thingamabob in the 2-category of spans, what's the problem?

@glaebhoerl @regehr @comex Also see Compilation On The GPU? A Feasibility Study[1], which is in some ways more conventional than co-dfns (it's a C-like language) and also in some ways more ambitious (the parsing handles arbitrarily nested depth without performance compromise).

[1]: https://dl.acm.org/doi/pdf/10.1145/3528416.3530249

".text" sections don't contain text. ".data" contains some but not all data. ".bss" stands for block started by symbol, a directive in one particular assembler for the IBM 704 (1954!) that just.. stuck around.

Object files are files but neither are nor contain objects (in the modern sense). Core dumps are memory dump but they've not been dumps of (magnetic) core memory since the 70s.

There are segments and sections, which mean slightly different things in every format.