Max S. New ⚜️

Real name: Max S. New

Assistant Professor in Computer Science & Engineering at University of Michigan.

Programming language theorist, categorical logician

Public Key

npub1dmn630rgl55pt7vgee6l930wfqjq6jry973hqf90fs6kgxztzd8qrg9dey

NIP-05 Address

maxsnew@types-pl.mostr.pub

Profile Code

nprofile1qqsxaeagh35062q4lxyvua0jchhysfqdfpjzlgmsyjh5cdtyrp93xnspz3mhxue69uhhyetvv9ujuerpd46hxtnfduqs6amnwvaz7tmwdaejumr0dsfp2nk3

Publishing to

relay.primal.net

nos.lol

relay.damus.io

Author Public Key

npub1dmn630rgl55pt7vgee6l930wfqjq6jry973hqf90fs6kgxztzd8qrg9dey

Show more details

Last Notes

2026-05-21 13:36:03 UTC

I've found a lot of people in PL don't know the relationship or difference between algebraic effects and effect handlers. This is somewhat understandable to an outsider because they came out of the same line of work.
Algebraic effects are based on the observation that we can describe many monads we use for effects as being the monad of free algebras for an algebraic theory. One of the most basic observations is that the state monad is the free algebras for an algebraic theory of read and write operations. This theorem is only true because of the equations imposed on the interaction between reading and writing.
Effect handlers are based on the observation that exception handling can be generalized from exceptions to any monad generated by a signature but *no equations*. This is basically because the free algebras of a theory are just trees so you can pattern match on the structure of that tree. So you can talk about read and write operations but you don't get the state monad you get "read+write trees" that you can pattern match on and write handlers that violate the equational theory of state e.g. computing not just the final state but the trace of all intermediate states of the computation.

2026-02-07 00:59:37 UTC

- reply

@nprofile…7slc does HOTT do that? I thought it currently doesn't it just makes univalence compute well

2026-01-28 22:27:15 UTC

Friendship ended with cubical Path now inductively defined identity is my best friend

2025-12-21 17:42:21 UTC

Hurry-Coward Isomorphism

2025-12-20 06:10:49 UTC

- reply

@nprofile…rrqe what is the simplest example of a presheaf on sets that comes up in semantics that isn't a COFE ?

2025-12-19 20:54:51 UTC

MathOverflow update to my guarded domain theory question (https://mathoverflow.net/questions/504840/cauchy-completeness-in-ordered-families-of-equivalences-constructively)
I got two nice proofs that the principle that every weakly complete OFE is strongly complete is equivalent to countable choice in ZF. The proofs make essential use of LEM: they both show that a certain OFE that is not weakly complete must therefore not be strongly complete and therefore it must be the case that there exists a Cauchy sequence with no limit point, and this sequence is a choice function.
So I think constructively this proof can be used to show that if every weakly complete OFE is strongly complete then every countable family of inhabited sets does not not have a choice sequence. But I don't think that that doubly negated version is equivalent because I don't think you can use it to actually construct a limit point. So the problem isn't completely solved.

2025-12-15 20:19:35 UTC

2-functors preserve adjunctions (!)

2025-12-14 00:38:17 UTC

Cartesian natural transformation

2025-12-11 03:46:01 UTC

- reply

@nprofile…ral2 ??? Intuitionistic linear logic with just tensor and unit is the internal language of symmetric monoidal categories

2025-12-09 15:21:58 UTC

- reply

@nprofile…rrqe when ur not sure if you're the one being criticized 😬

2025-12-07 15:56:04 UTC

- reply

@nprofile…ral2 my bigger worry is in computer science, where there is not really as prominent of a culture of theory building. If the problem solvers get automated away will anyone even care to keep the theory builders around

2025-12-01 14:42:06 UTC

- reply

@nprofile…rrqe I just tell the students to install WSL, it works quite well

2025-12-01 14:41:34 UTC

- reply

@nprofile…rrqe wrong thread

2025-11-29 19:40:36 UTC

Dead Posets Society

2025-11-25 21:52:28 UTC

- reply

@nprofile…w8t5 sorry Martin but no one is going to do this unless it's the default on whatever interface they are using

2025-11-25 16:12:58 UTC

- reply

@nprofile…9t3n people on here don't know the difference between engagement and hostility

2025-11-23 19:29:09 UTC

Getting back into basic guitar and piano and gotta say the software for this stuff does NOT spark joy lol. I need like idk emacs/vim for music notation not Eclipse

2025-11-22 18:56:47 UTC

- reply

@nprofile…rrqe @nprofile…a7rw
I see, so I guess what you are saying is that basically I shouldn't think of realizability semantics of recursion as a totally different notion than dcpo-based domain theory but rather a version of that same theory but built on realizability rather than classical set theory

2025-11-22 18:48:13 UTC

- reply

@nprofile…rrqe @nprofile…a7rw oof

2025-11-22 18:46:28 UTC

- reply

@nprofile…rrqe @nprofile…a7rw yeah for that reason I might only cover recursive functions for the realizability portion and cover recursive functions and types using DCPOs

2025-11-22 18:40:29 UTC

- reply

@nprofile…rrqe @nprofile…a7rw
Do you have a recommended reference for SDT? I definitely won't be able to get to it in class. Only 6 hours of lecture left and I'd like to do basic guarded domain theory as well

2025-11-22 18:01:18 UTC

- reply

@nprofile…rrqe @nprofile…a7rw no polymorphism. Ideally CBPV + recursive functions and recursive types

2025-11-22 17:41:19 UTC

- reply

@nprofile…rrqe @nprofile…a7rw
so modest sets are a subcategory of Asm? Do you have a reference I could dig into?
Edit: I found these notes by Streicher which look helpful on this topic: https://www2.mathematik.tu-darmstadt.de/~streicher/REAL/REAL.pdf

2025-11-22 17:34:43 UTC

@nprofile…a7rw I really like your realizability notes (https://raw.githubusercontent.com/tomdjong/MGS-categorical-realizability/refs/heads/main/MGS-categorical-realizability.pdf) and was looking at doing a lecture or 2 on realizability models of effectful lambda calculus.
Am I right that the category of assemblies is already enough to give a model of PCF (i.e., simple types and recursive programs) but that you need to move to the realizability topos to get a model of FPC (PCF + arbitrary recursive types)?

2025-11-21 17:22:50 UTC

All math is completely useless abstract bs cooked up by some wanker until I figure out how to use it in my own research and then it is the best shit on planet earth

2025-11-21 04:32:44 UTC

Code is cheap, don't be afraid to throw it away

2025-11-18 00:10:08 UTC

Beck-Chevalley

2025-11-09 16:53:07 UTC

- reply

@nprofile…rrqe this is to me the best motivation for univalence as someone not particularly interested in homotopy theory

2025-10-30 15:19:29 UTC

- reply

@nprofile…rrqe then why did you write/publish the note if you didn't want people to read it

2025-10-20 14:38:10 UTC

Being a professor means you become skilled at figuring out which deadlines are fake. But then service committees make deadlines even earlier because they know the profs will not do things on time. So we just get even more email reminders to submit things that are now overdue even though we all know they don't actually need to be done yet. Repeat ad infinitum

2025-10-15 16:16:55 UTC

- reply

@nprofile…rrqe I really did think it would become normal in America to wear a mask when you are sick just like in Asia but no too much freedom here

2025-10-01 15:44:38 UTC

Here is the “best” formulation of the Yoneda lemma. The one I will be teaching today.
Let x be an object of C and P be a presheaf on C.
Then for any element p : P(x) there exists a unique natural transformations [p] : Yo(x) -> P satisfying [p](id_X) = p.
The things I really like about this formulation:
1. It is very clear how to prove it: define [p] such that [p](id_x) = p and prove it’s unique.
2. It is, very clearly, a universal property, of which the student has probably now seen many concrete examples before they get to this. It says that the representable Yo(x) is the “presheaf freely generated from an element at x”.
3. It doesn’t mention a bunch of naturality side conditions that follow automatically (and in fact can be proven as consequences of this formulation of the Yoneda lemma itself). I.e., there’s nothing about naturality in x, naturality in P. I remember being quite overwhelmed by how many side conditions I had to prove when I first encountered Yoneda.

2025-06-26 15:51:54 UTC

- reply

@nprofile…6kk0 @nprofile…fcvf
yea looks like a simpler version of cubical to me: sacrifice definitional proof irrelevance and transport refl is identity to get extensionality principles

2025-06-26 15:28:48 UTC

Is the principle of unique choice provable in any flavor of Observational type theory? I saw in @nprofile…fcvf 's paper (https://hal.science/hal-03857705v2/) that it is not provable in that version

2025-03-13 20:25:38 UTC

I don't know why we all like Descartes so much. He was the first person ever to commit the sin of choosing a basis

2025-03-03 22:24:02 UTC

There's a terminological quirk that I really despise which is including the name of a bound variable in the name of a concept.
I think the most common one I encounter is "F-algebra". Wikipedia uses this terminology without bringing any particular "F" into scope: https://en.wikipedia.org/wiki/F-algebra which probably is one of the reasons this bad terminology propagates. nlab does better, only saying "F-algebra" when we are talking about an abstract functor called "F": https://ncatlab.org/nlab/show/algebra+for+an+endofunctor .
In one of my first papers in grad school we made this mistake in that we called some charts we came up with "L,M,N"-graphs because they were parameterized by variables which we arbitrarily called L,M and N.

2025-02-25 14:29:09 UTC

I didn't even know there was a SIGAda: https://www.sigada.org/

2025-02-21 17:08:13 UTC

Uh am I wrong or does the nlab page on propositional resizing have a completely bogus "proof" that propositional resizing is inconsistent: https://ncatlab.org/nlab/show/propositional+resizing#properties
Like literally the first sentence of the proof is wrong: it says if propositional resizing holds then...the universe of propositions contains itself?? Am I missing something?