glaebhoerl @glaebhoerl@schelling.pt

heyooooooo new article: "A world to win: WebAssembly for the rest of us" https://wingolog.org/archives/2023/03/20/a-world-to-win-webassembly-for-the-rest-of-us

Of interest if you wonder: why does it seem like only rust and C are winning with WebAssembly? what is the deal with garbage collection? how would you compile scheme to wasm? how can I win with my weirdo altlang? also, is WebAssembly haunted? guaranteed success or your money back!

Susan Kare
https://www.moma.org/artists/38483
https://www.moma.org/collection/works/188382?artist_id=38483&page=1&sov_referrer=artist
https://en.wikipedia.org/wiki/Susan_Kare

"Susan Kare is an American artist and graphic designer best known for her interface elements and typeface contributions to the first Apple Macintosh from 1983 to 1986. She was employee #10 and Creative Director at NeXT."

via
https://www.readjpeg.com/

#Marchintosh

for your consideration

In Utrecht, NL people have been falling into a pond because duckweed has been stressed by the cold and turned it red an looks exactly like a cycle path.

I'm far from an AI enthusiast, but I can see why Google is worried...

Number theorists love mutant versions of the integers with extra numbers thrown in. For example, 'Gaussian integers' are just numbers like

a + bi

where a,b are integers and i = √−1. It's fun to think about primes in the Gaussian integers. Some ordinary primes stay prime in the Gaussian integers, like 3. But others don't, like

2 = (1 - i)(1 + i)

and

5 = (2 + i)(2 - i)

Cool fact: an odd prime stays prime in the Gaussian integers if and only if it's 1 less than a multiple of 4.

(1/n)

How did Russian cosmonauts know where they were? The Globus INK (1967) showed the position of their Soyuz spacecraft on a rotating globe. It is an analog computer built from tiny gears. I reverse-engineered the wiring (which inconveniently had been cut) and we powered it up. 🧵

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?