More linguists botching mathematical definitions 

We've now reached the point where they present a substructural logic, and proceed to assume structural rules they don't write down or describe informally but seem to suggest aren't supposed to be in the system... (and contextually the rule they're using silently shouldn't be here, because word order)

I need to stare at this more when I'm not being inundated with announcements of late trains, but I'm reasonably sure their example of two proofs modeling different evaluation orders have proof terms with the same normal form...

It occurs to me then when academic books are published, there are usually technical reviewers who are supposed to look for these kinds of things before the book is published... I guess they didn't get broad enough expertise in their reviewer pool? I guess that's one of the risky parts of interdisciplinary research, is if you're way off base there aren't many people who can notice and help with course corrections. I don't even know that much category theory and classic substructural logic and I'm finding these issues, which makes me slightly concerned I'm going to miss more important problems later. Or maybe they all just sorta skipped these intro/background chapters and focused attention on the later stuff, and the main part of the book is fine?

Show thread

More linguists botching mathematical definitions 

They are now taking about the scope of a monoid multiplication extending as far as possible to the right, because they're applying it to terms in a lambda calculus (they mean the scope of the binding introduced by the lambda).

Years of PL pedantry may have ruined this book for me.

In my defense I think it's reasonable for me to be upset about having to explain in papers for years to come that the primary sources in this area give incorrect terminology for standard concepts.

Show thread

*in their first example...

Hurray autocorrect

Show thread

I'm reading a book on using category theory as a basis for linguistic semantics, and just a few pages in they're defining the terminal object incorrectly (what they call terminal is initial) and they're silently assuming the existence of partial morphisms in theory first example of a category (in a category theory for linguists chapter). :blobcatsadpleading:

I'm starting to see why the grammar and semantics communities bifurcated into logic-focused and linguistics-focused.

I'm in for a rough read. :blobcatsweats:

Few meals are as satisfying as a good ma po tofu (the real stuff with chili oil and Szechuan peppercorns, not the food court stuff that came out of a packet).

This book on blockchains assumed at the business management industry is free for the next couple weeks as a new release promo. I'm simultaneously terrified of what sorts of nonsense I might find inside, and also morbidly curious and it's only 84 pages. Should I read it?
cambridge.org/core/elements/bl

Just noticed the brand of this portable car jumper we picked up: TYPES

I have discovered that Gmail classifies all email from a prominent "contrarian" in the TYPES community as spam. I am pleased.

I've got termux and a Bluetooth keyboard set up now on my e-ink tablet, which has a warm yellow (basically amber) backlight, and it has some real retro computer vibes. I'm having flashbacks to messing around on a digital word processor with its dedicated amber CRT screen as a kid (I'm a bit too young to have used and early PC or proper terminal with the amber screen)

New Humble Book Bundle is up from No Starch Press: humblebundle.com/books/linux-n Mostly Linux and general UNIX stuff, but the middle tiers include Absolute and Absolute from @mwlucas !

I am installing stuff in a Debian chroot on my e-ink tablet and... the clang-13 package depends on gcc8?

More LaTeX cross platform Unicode nonsense 

Okay I had chalked this up to some stupid naming trick in one library or the other, but I had forgotten that this works just fine on FreeBSD... Does FreeBSD have better Unicode support than Linux? Quite possible but weird and should irrelevant since I'm using pdfTeX under the hood on both... the Linux version I'm using is one 0.01 versions higher than what I've got installed on FreeBSD...

Show thread

omg, using the inline version of the \todo command from the todonotes package breaks the typesetting from the Lean theorem prover listings package 🤦‍♂️ how is this even possible?

Show thread

Ugh, what fresh LaTeX hell is this? This paper now compiles with ```latexmk -pdf -bibtex blah.tex``` just fine on , but I take the same LaTeX file over to a machine and it fails with messages like:
```
Argument of � has an extra }.
<inserted text>
```
(yes, the diamond with the question mark in it is actually there in the message, verbatim)

Rust editor/IDE setup 

I've been writing some Rust lately, and have been fighting to get a good tooling setup. VSCode's Rust plugin is excellent, but the memory consumption is unbelievable... it will lock up a machine with 16GB of RAM 😭​ (I don't have this issue with other plugins for VSCode).

I tried and failed *hard* to set up neovim rsdlt.github.io/posts/rust-nvi

And then I discovered this new Helix editor, which is just magic. github.com/helix-editor/helix Installed in a flash, built-in Rust support once you install rust-analyzer... it's fantastic. Vim-like though, I know there are some who might not like that...

Also looked at lapce.dev/, which is also excellent and is not Vim-like, but a brief effort to make it run on did not go well...

Colin boosted
Colin boosted

#Tusky nightly updates via Google Play are delayed because Google chooses to continue to be as annoying as possible. They think we as client developers have any control over content on Mastodon instances and violate their "user generated content policy". 🙄
We also have a repository you can add to F-Droid in oder to get nightly updates completely Google-free: releases.nailyk.fr/repo/

Oh look, another university IT upgrade broke virtually everything in Firefox... again....

I guess nobody tests on anything but Chrome anymore?

> There will be no entrance testing at the start of the academic quarter.

I've been pretty happy with how Drexel has managed COVID stuff up to this point, and I even accept masking becoming optional in classroom settings at this point (they'd be between a rock and a hard place with current societal views). But this particular choice seems like a recipe for a huge pile of COVID cases this term (and presumably, future terms unless things change).

Show older
types.pl

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