Mastodawn

@jcreed Very nice post! Btw, T -> (-) and the functor U (which can be defined as T v (-)) are used in the setting of "synthetic phase distinctions", eg https://dl.acm.org/doi/pdf/10.1145/3776673.

(I have yet to find a use case for √ in this setting, but maybe this isn't surprising because I care about models with T = 0, where √ doesn't exist.)

@HarrisonGrodin thanks for the reference! Although: I would have thought T v (-) would turn A -> B into A -> B + 1 rather than A -> 1. But I did have the idea earlier (that didn't make it into the blogpost) that U(X) could be expressed as the pushout of X <- X x T -> T. Does that sound right to you? Are we starting from different assumptions somehow?

@jcreed Oh yes, that's what I mean by v - the "join" (pushout you described), not the coproduct. (I believe it's written this way because for h-props P and Q, this P v Q is still an h-prop.)

@HarrisonGrodin great, then that sounds exactly right and I agree. Btw, is it a coincidence that the notation in your paper lines up with the mathoverflow question here https://mathoverflow.net/questions/424346/internal-language-of-the-sierpi%C5%84ski-topos ? I imagine it's entirely possible if so, ∙ and ∘ are not exactly very exotic symbols, but it is an amusing coincidence in that case :)

Internal language of the Sierpiński topos

What is an internal language of the Sierpiński topos, which is defined as arising from the category $\mathsf{Set}^{\to}$, the category of arrows in $\mathsf{Set}$? Or more generally, is there a rough

MathOverflow

@HarrisonGrodin oh wow and I am getting pretty excited reading your paper here, this sounds like it might be exactly the thing I was hoping would work out

@HarrisonGrodin hmmm but now I am racing ahead to see if you have an internalization of the ?? in abs × — ⊣ ◯ ⊣ ?? ⊣ ●
...maybe this will become clear if I keep reading...

@jcreed Oops, race condition, correctly guessed you might want this on another subthread 😅 No, we don't have this, and Shulman's no-go theorem says you can't have it without additional judgemental structure. So if you care to have √, I think you have to start with that adjoint triple in cohesive type theory (or maybe just √ -| Closed in spatial type theory), and then define abs as Closed(0).

@jcreed From the perspective of AFAT, √ lets you isolate "concrete" data, which would have to be judgmentally quarantined off to preserve the noninterference property. However, the existence of √ would mean that you couldn't set abs to false, which is how we extract the efficient "concrete" code...

@HarrisonGrodin right ok that's familiar, I think, it's the thing that fundamentally requires flat-like custom judgemental machinery, yeah?

https://www.jonmsterling.com/0094/

Jon Sterling 3d ago

@jcreed @HarrisonGrodin Some further thougths about the additional adjoints that might interest you…

Lately, the ideas from this blog post seem to have led to a very interesting paper by Theocharis and Brady: https://arxiv.org/abs/2605.00655

On the relationship between QTT and STC

Jon Sterling 3d ago

@jcreed @HarrisonGrodin Regarding synthetic phase distinctions (without \sqrt), perhaps it will be helpful for me to give a little history. This stuff goes back to Bob Harper's and my attempts in early 2020 to re-understand the Harper–Mitchell–Moggi 1990 model of ML modules without an explicit phase separation. We wrote this up in "Logcial Relations as Types" (https://www.jonmsterling.com/sterling-harper-2021/), and I quickly realised that this would be useful for many more things than ML modules and parametricity.

1. "Synthetic Tait computability" for doing metatheory and other logical relations proofs. With this, @carloangiuli and I solved the normalisation conjecture for cubical type theory: https://www.jonmsterling.com/sterling-angiuli-2021/, which was expanded into my PhD thesis https://www.jonmsterling.com/sterling-2021-thesis/.
2. In the final chapter of my PhD thesis, I suggested that this language should be used as a basis for refinement types & erasure, though it was not until my linked blog post that I noticed the use of the amazing right adjoint. I am very glad that people have finally taken up this suggestion.
3. Continuing with PL applications, Bob and I did an interpretation of information flow control: https://www.jonmsterling.com/sterling-harper-2022/. Please note that while the denotational semantics is good, the adequacy proof in this paper is bogus (see errata). I believe there is another proof, but I haven't got around to it. (1/2)

Logical relations as types: proof-relevant parametricity for program modules

Jon Sterling 3d ago

4. With Yue Niu, @HarrisonGrodin, and Bob Harper, we proposed to use the synthetic phase distinction to model cost, in the "cost-aware logical framework”: https://www.jonmsterling.com/niu-sterling-grodin-harper-2022/. Harrison has led the way with many further developments in this direction, including Decalf (https://www.jonmsterling.com/grodin-niu-sterling-harper-2024/), and the Abstraction Functions as Types paper (https://arxiv.org/abs/2502.20496) which in my view really elegantly closes the loop back to LRAT in a way that greatly exceeded my expectations and imagination at the beginning of this line of work.

I don't exactly work on this stuff anymore because one does not want to be buried by one's PhD thesis. But I still find it interesting, and I do think there remains some possible untapped potential for using this structure to give simpler alternatives to existing theories in a number of areas. (2/2)

A cost-aware logical framework

@jonmsterling @HarrisonGrodin this historical context is great, thanks! I think the punchline that's exciting to me coming across in the recent paper is that you don't even *need* sqrt to accomplish glue and fracture. That's pretty cool. I was rabbit hole-ing in a different direction under the tacit (but unjustified!) assumption that it was needed

@jonmsterling @HarrisonGrodin ok, now my question is: is it also possible to prove internally the functoriality (or maybe the right thing to say is "faithfulness"?) of the glue/fracture equivalence? that the maps Glue(X_•, X_∘, χ) → Glue(Y_•, Y_∘, γ) are exactly the same as the pairs of maps f_• : X_• → Y_• and f_∘ : X_∘ → Y_∘ such that we get a commutative square
χ
X_• → ●X_∘
f_•↓ ↓●f_∘
Y_• → ●Y_∘
γ
?

Jon Sterling 2d ago

@jcreed @HarrisonGrodin If I’m reading this right, that should be doable yes.

@jonmsterling @HarrisonGrodin nice! I was expecting/hoping it to be possible. It's pretty natural for me to imagine how you'd start the proof; like, surely you want to "extract" the f_• by hitting the Glue(X_•, X_∘, χ) → Glue(Y_•, Y_∘, γ) map with functoriality of ●, and then I guess it's obvious by the equivalence you've already shown that it gives you *some* map X_• → Y_•, so all I'm really asking is whether all the details work out nicely. I'm inclined to trust you that they do!

HarrisonGrodin 2d ago

@jcreed @jonmsterling Yes!! This is exactly what we use in AFAT.

jcreed

@HarrisonGrodin @jonmsterling well this has turned out to be a great example of my favorite strategy of reading research papers, to wit
1. Do not read the research paper; in fact, refrain from being aware that it exists
2. Bang your head against the wall trying to invent something
3. Find out about the research paper, which does it way better than whatever you were trying
4. Read the research paper
5. Delight in the fact that the accomplishments of the paper make a lot of sense thanks to #2

Jon Sterling 2d ago

@jcreed @HarrisonGrodin Somehow, for almost any X, this remains the most reliable way to become X-pilled 😂😂😂

@HarrisonGrodin @jonmsterling ok, *now* I have the following question. It seems plausibly consistent to do the following, if one is careful about universes:
- postulate the existence of *many* different subscripts that could go under ● and ◯; i.e. "colors" from Bernardy and Moulin 2013, different axes of abstractness/concreteness.
- postulate that for every types A, B there is some color i such that ●ᵢA → A is an equivalence ("A is i-concrete") and B → ◯ᵢB is an equivalence ("B is i-abstract").

@HarrisonGrodin @jonmsterling
Now we have enough wiggle room to take any function χ : A → B at all and reify it as a glue type. Do we get internalized parametricity and all the Wadler-style free-theorems our heart desires?

@HarrisonGrodin @jonmsterling oh wait no something is very suspicious about this since at the very least I'd need to impose some kind of distinctness of A and B. Which in itself seems suspect. However, *gestures vaguely at this sort of idea*.

HarrisonGrodin 2d ago

@jcreed @jonmsterling I think something like this could be made to work. If you think of an existential/coend as a dependent sum quotiented by representation independence, you can treat the injection Sigma -> Exists as an abstraction function and get something like parametricity. (The concrete implementation is a Sigma, but the abstract interface is an Exists, modding out by RI.) Maybe something dual would work too...

Constantine Theocharis 2d ago

@jcreed You might find Taichi Uemura’s work on internal languages of diagrams of logoses interesting. https://arxiv.org/abs/2212.02444

It is essentially the semantic version of this. How do you take a certain “mode sketch” which defines all the different i subscripts and their relationships, and get back (semantics for) a type theory with these modes. It includes things like disjointness of modes.

The nice thing is if you don’t care about the amazing right adjoint then the entire construction can be performed internally to type theory, presented as an indexed family of lex accessible modalities satisfying certain conditions.

@HarrisonGrodin @jonmsterling

Homotopy type theory as a language for diagrams of $\infty$-logoses

We show that certain diagrams of $\infty$-logoses are reconstructed in homotopy type theory extended with some lex, accessible modalities, which enables us to use plain homotopy type theory to reason about not only a single $\infty$-logos but also a diagram of $\infty$-logoses. This also provides a higher dimensional version of Sterling's synthetic Tait computability -- a type theory for higher dimensional logical relations.

arXiv.org

Lindsey Kuper 2d ago

@jcreed @HarrisonGrodin @jonmsterling I think that sometimes students do this and are unhappy that they're going about research "inefficiently" by "wasting" all that time on step (2), but (a) efficiency isn't all it's cracked up to be anyway, and (b) as you note, the time is in fact not wasted

@lindsey @HarrisonGrodin @jonmsterling yeah, strong agree!

@lindsey @HarrisonGrodin @jonmsterling I have to concede that it's a lot easier to have this positive attitude now that I'm "out of the game" of research --- like, there's no real professional stakes for me whether I get to publish a new idea or not --- and I do remember being a little stressed about it when I was a student, but nonetheless it *wasn't* time ill spent

Jon Sterling 2d ago

@jcreed @lindsey @HarrisonGrodin Yeah. I used to get stressed about it.

Nowadays, if I find out someone has done something satisfactorily it is kind of a relief because it means I can use it — or move on…

Rob Rix 2d ago

@jonmsterling @jcreed @lindsey @HarrisonGrodin sometimes there’s some cross-pollination, too.

Joshua Wise 2d ago

@jcreed I remember having dinner with @chrisamaphone and @simrob some months ago and discussing the class of "Tom-resistant problems", which I think they defined as problems that, roughly, required you to read the research paper *first*. I feel like Tom just accepted this methodology before I did, but I am very glad to have eventually come around to it. It has been extremely fruitful for my understanding of digital signals processing!

@joshua @chrisamaphone @simrob heh, yeah, Tom and I often joke about our respective levels of "ignore literature, invent it yourself"; if I compare myself to him I come off as *more* inclined to do careful literature review. This particular case wasn't an example of me deliberately avoiding spoilers so much as gently making fun of myself for not *succeeding* at keeping up with the research frontier on this topic.

@joshua @chrisamaphone @simrob (then again: I am super happy that mastodon is an effective "mention random blogpost" to "get the attention of world experts in topic" pipeline!)