Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: deprecated: our papers

Topic: Native Type Theory

Christian Williams (Feb 10 2021 at 02:11):

Hello, I and @Mike Stay wrote a paper: https://arxiv.org/abs/2102.04672

Christian Williams (Feb 10 2021 at 02:13):

Native Type Theory is a method of generating logical type systems for a broad class of languages, to provide a shared framework of higher-order reasoning for the many languages and structures used in software.

Christian Williams (Feb 10 2021 at 02:15):

The idea is very simple - a programming language can be modelled as a theory, and its presheaves form a topos. The internal language of this topos is an intuitive and expressive type theory in which we have total expression of the structure and behavior of terms.

Christian Williams (Feb 10 2021 at 02:18):

In the paper we outline the construction as a functor from "higher-order algebraic theories" to "(nice) dependent type theories". We give the basics of the type system, and some first applications.

Christian Williams (Feb 10 2021 at 02:22):

The construction is probably closer to implementation than it may seem. The formal specification community has used K Framework to write languages such as C, Java, and Python as higher-order algebraic theories (with rewriting); and native type systems are the same kind as that of Coq.

Christian Williams (Feb 10 2021 at 02:24):

So, we are now looking to make it happen. If you are interested, just let me know.

Christian Williams (Feb 10 2021 at 02:24):

It would be great to use this space for thoughts about the paper, exploring applications, and anything else.

Christian Williams (Feb 10 2021 at 02:36):

If suddenly every programming language had an expressive logic built-in, what kind of things would you want to do? How do you think this could affect the practice of programming?

Christian Williams (Feb 10 2021 at 02:39):

A motivating example we like is searching codebases --- we imagine querying on GitHub "programs that implement this algorithm under these conditions" and pulling up all results to compare, plug and play.

Matteo Capucci (he/him) (Feb 10 2021 at 08:37):

That's really cool work! Kudos!

Morgan Rogers (he/him) (Feb 10 2021 at 10:07):

In Proposition 26, L and R have the same domain and codomain; which one is the wrong way around?

Morgan Rogers (he/him) (Feb 10 2021 at 14:20):

(sorry, that wasn't the most constructive remark :sweat_smile: )
I have more interesting questions now that I've read the paper a little more closely. First, I'll summarise what I understand from the paper:
You start with a certain notion of higher-order algebraic theory (I haven't studied HOL deeply enough to know whether your "base types exponentiable to order n" notion is equivalent to the more familiar one in terms of quantification over subobjects etc, but I can ignore that for now). You construct the syntactic category in a standard way, then note that it can be characterised by its canonical identity-on-objects functor from the free such category, so you can hide the syntax. Since the structure in these categories is defined in terms of limits and exponentials, which are preserved by the Yoneda embedding, you can pass to the presheaf topos without losing anything. Then you extract a type theory for the topos, most of the ingredients of which seem fairly standard.

So now I wonder:

1. (Most important) Is this extension conservative? If I prove a theorem which can be stated in the language of the original higher-order algebraic theory using the native type theory for the presheaf topos, is it provable in the original theory? I expect the answer is yes, but checking this is so amounts to verifying that passing to the native type theory isn't adding anything unexpected to the logic.
2. The notion of theory morphism in the category of higher-order algebraic theories is not especially well-motivated, and it is not clear how it results in functoriality of P:HOAT^op -> CCT when the latter is equipped with (co)continuous logical functors as its morphisms. Why is the subobject classifier or any non-representable exponential object preserved by composition with a cartex functor $F$?
3. Assuming that the preceding point all works out fine, it still seems unfortunate that you choose such restricted morphisms in the codomain. An ordinary (first-order) algebraic theory is classified by the topos of presheaves over its syntactic site, which means that its Set-models (or indeed its models in any Grothendieck topos E) correspond to the geometric morphisms from Set to that topos (resp. from E to that topos). To obtain the models of the higher-order theories you describe, it suffices to consider geometric morphisms whose inverse image functors preserve the defining exponentials. In particular, a locally connected geometric morphism which is not atomic (inverse image functor is cartesian-closed but not logical) would produce a model.

It's plausible that you won't care much about the details I'm pointing to above, since the many examples illustrate that you have thought hard enough about your set-up to know it does what you want it to, which is to say produce rich, typed languages for a suitably large class of theories, implementable using tools which already exist, and useably functorial. I'm looking at this purely from the categorical logic perspective that is accessible to me. In any case, taking my critical hat off, I'm happy to see toposes emerging in a new way in computer science, and hope applying this stuff will lead to new insights!

Jacques Carette (Feb 10 2021 at 14:27):

Question in a completely different direction: so programming languages are really bad, in the sense that their type theory is quite degenerate, in a wide variety of ways. [From Java getting variance of arrays wrong to Haskell's type system being inconsistent as a logic.] How does this "show up" in this construction? i.e. what are the symptoms that one started with a 'bad' language in the induced native type theory? I'm interested in seeing how this "shows up" in all steps of the construction, not just in the end.

Christian Williams (Feb 10 2021 at 19:44):

Morgan Rogers (he/him) said:

In Proposition 26, L and R have the same domain and codomain; which one is the wrong way around?

L is the wrong way around. Thanks! I don't know how that happened.

Christian Williams (Feb 10 2021 at 19:48):

Thanks for your thoughts, Morgan. Yes, we need to check for conservativity. I do not have much intuition for this --- it seems as though the native type system is so much more expressive than the original theory that there would surely be new provable facts, but I'm not sure. The logic of toposes has been thoroughly studied; I imagine someone has asked whether the presheaf construction is conservative. If anyone knows a reference, it would be appreciated.

Mike Shulman (Feb 10 2021 at 19:51):

Well, the Yoneda embedding is fully faithful. What more conservativity than that would you ask for?

Christian Williams (Feb 10 2021 at 19:56):

Ah, okay. But when you step outside of the image, like taking a coequalizer, and you prove that a term is of this type, is that not "proving something that isn't provable in the theory"?

John Baez (Feb 10 2021 at 19:59):

Usually in logic a bigger theory is a "conservative" extension of a smaller one if anything that can be stated in the smaller theory and proved in the bigger theory can actually be proved in the smaller theory.

Christian Williams (Feb 10 2021 at 19:59):

Ah yes, okay great.

John Baez (Feb 10 2021 at 19:59):

If something can't even be stated in the smaller theory, then of course the smaller theory has no hope of proving it.

Mike Shulman (Feb 10 2021 at 20:01):

In this case it's not even entirely clear to me what it means for the smaller theory to "prove" something, since it's just a (higher-order) algebraic theory without an associated "logic".

John Baez (Feb 10 2021 at 20:01):

For example in nonstandard analysis we add new infinitesimals to the real numbers and new rules for working with them, but it's a conservative extension, which is reassuring, because it means anything we can state about plain old real numbers and prove using nonstandard analysis could actually be proved using the ordinary axioms for real numbers.

Christian Williams (Feb 10 2021 at 20:04):

The theory's logic is equational logic in (nth-order) simply-typed lambda calculus.

John Baez (Feb 10 2021 at 20:04):

Mike Shulman said:

In this case it's not even entirely clear to me what it means for the smaller theory to "prove" something, since it's just a (higher-order) algebraic theory without an associated "logic".

Well, some composites of morphisms can equal some other morphism. And then your remark about Yoneda fully faithful embedding comes into play: if the analogous fact holds in the presheaf category, it held already in the original category.

(You know all this, I'm just saying it for the sake of the universe at large.)

John Baez (Feb 10 2021 at 20:05):

Christian Williams said:

The theory's logic is equational logic in (nth-order) simply-typed lambda calculus.

Yes, I'd say that counts as a "logic". I'm very generous about what counts as a logic.

Christian Williams (Feb 10 2021 at 20:05):

So, Morgan's concern is answered. I should've mentioned it in the paper, but the discussion here will make a better draft.

Nathanael Arkor (Feb 10 2021 at 20:06):

To expand further on @John Baez's comment (with the same caveat), seeing propositions as types, one would expect the "correct" generalisation of conservativity to demonstrate a bijective correspondence from every term $\Gamma \vdash t : A$ in the new theory, to one $\Gamma \vdash t' : A$ in the original theory, which corresponds precisely to the inclusion being fully faithful.

Mike Shulman (Feb 10 2021 at 20:09):

Oh right, of course equational logic is a logic.

John Baez (Feb 10 2021 at 20:11):

And there's even the null logic where you can't say or prove anything! :upside_down:

Christian Williams (Feb 10 2021 at 20:11):

I use that one myself sometimes.

Christian Williams (Feb 10 2021 at 20:13):

As for point #2, ultimately the definition of theory morphism does not play much role in functoriality, because it is just a certain kind of cartex functor, and we're basically just including HOAT into Cat. My understanding is that precomposition is a classic example of a logical functor, which should preserve everything in sight.

Christian Williams (Feb 10 2021 at 20:15):

For point #3, I don't fully understand what you're saying. I get that there is a connection to the classifying topos, but I don't have any use for it in mind. What we care about for this paper are morphisms between type theories, which need to preserve all of that structure. But if you expand on what you're saying I can understand better.

John Baez (Feb 10 2021 at 20:16):

My understanding is that precomposition is a classic example of a logical functor, which should preserve everything in sight.

By the way: if that's true, let's add it as an example to logical functor. Maybe it's hiding in the stuff before the examples?

Christian Williams (Feb 10 2021 at 20:18):

Jacques, thanks for your thoughts. The formal verification community has used K Framework to specify many real-world languages: https://github.com/kframework. They are basically higher-order algebraic theories with rewriting. So the fact that some popular languages don't have much in the way of type systems is reflected in their representation simply as sorted theories. But from the construction, they get a dependent type theory that's as rich as the one used in Coq.

Jacques Carette (Feb 10 2021 at 20:46):

Well, Haskell has quite a lot in terms of a type system... But perhaps I am not asking the right question. It's not clear what the difference is between Haskell's type system (a variant of System F, if I remember well) and the type system that this construction gives it. Is there a way to understand that?

But still, odd languages like C, which make it legal to lie to the compiler (they call it 'casting'), the operational semantics ends up untyped. Yes, there is a 'core language' that's decently behaved, but that's not what most people use. So the question is, when the operational semantics allows you to collapse everything, what does the construction do with that?

Note that being able to specify a language (which indeed has been done in K, but in many other systems too) doesn't mean that what's specified isn't degenerate. There are many very complicated ways to 'specify' the empty set too... [I'm being colourful here, not facetious].

So I guess I have 3 questions:

1. if you start with something very well-behaved, like say Martin-Loef type theory, what do you get using your construction?
2. if you start with something well-behaved but with a naturally weak type system (like simply-typed lambda calculus), what do you get?
3. if you start with something really awful (like the fully untyped lambda calculus, or worse, something entirely inconsistent), what do you get?

I think you've partially answered the second question: you get a dependently-typed system.

Nathanael Arkor (Feb 10 2021 at 20:57):

As I understand it, you start with a simple type theory (with possibly higher-order operators), and then extend it to a dependent type theory. There is no attempt to restrict to well-behaved languages. So (1) isn't valid, because the original language has to be simple. If you start with (2), you get a variant of MLTT (namely, the internal language of a presheaf topos). If you start with (3), you get an inconsistent language.

Christian Williams (Feb 10 2021 at 21:06):

What do we mean by inconsistent here?

Nathanael Arkor (Feb 10 2021 at 21:13):

In the sense of Curry's paradox, for instance.

Morgan Rogers (he/him) (Feb 10 2021 at 21:56):

Mike Shulman said:

Well, the Yoneda embedding is fully faithful. What more conservativity than that would you ask for?

Although it was straightforward, I'm glad that it ended up being discussed :grinning_face_with_smiling_eyes:

Morgan Rogers (he/him) (Feb 10 2021 at 22:06):

Christian Williams said:

As for point #2, ultimately the definition of theory morphism does not play much role in functoriality, because it is just a certain kind of cartex functor, and we're basically just including HOAT into Cat. My understanding is that precomposition is a classic example of a logical functor, which should preserve everything in sight.

The definition of theory morphism for HOATs does include a cartex functor, but it also includes a relation and a mapping of signatures. Is "a relation of orders $i:n_1 \to n_2$" in Definition 12 just saying that $n_1 \leq n_2$? Is $\mathbb{T}_i(f)(T_1,\tau_1)$ equivalent to $T_1$ as a category? If so, is this supposed to follow from Proposition 10 (there's a missing reference in the proof of that Proposition, btw)? If not, why does composition with $F$ give a functor between the presheaf categories?

Morgan Rogers (he/him) (Feb 10 2021 at 22:14):

Christian Williams said:

What we care about for this paper are morphisms between type theories, which need to preserve all of that structure.

That's only true if you want the morphisms to preserve everything on the nose, which might not actually be what you want, considering that you're building these native type theories to extend a strictly smaller class of theories. For example, a functor which is merely cartesian-closed will preserve all of the types coming from the original HOAT, even if it doesn't preserve the extra types which were added in the process of passing to the presheaf topos and extracting the native type theory.
The point I was trying to make originally is that if you do end up caring about the models of these theories (or if someone else does because they're interested in HOATs for another reason), choosing a class of morphisms between HOATs large enough to recover "models as induced geometric morphisms" could be neat.

Christian Williams (Feb 11 2021 at 01:00):

Morgan Rogers (he/him) said:

The definition of theory morphism for HOATs does include a cartex functor, but it also includes a relation and a mapping of signatures. Is "a relation of orders $i:n_1 \to n_2$" in Definition 12 just saying that $n_1 \leq n_2$? Is $\mathbb{T}_i(f)(T_1,\tau_1)$ equivalent to $T_1$ as a category? If so, is this supposed to follow from Proposition 10 (there's a missing reference in the proof of that Proposition, btw)? If not, why does composition with $F$ give a functor between the presheaf categories?

Good point. You're right, this needs to be made explicit. There is a canonical map $T_1\to \mathbb{T}_i(f)(T_1,\tau_1)$ (the opcartesian morphism), and this modified presheaf construction precomposes with the composite $T_1\to T_2$.

Christian Williams (Feb 11 2021 at 01:55):

As for the point about models, I think I understand and I agree. The precise structures involved are subject to some change as needed.

Morgan Rogers (he/him) (Feb 11 2021 at 09:33):

Christian Williams said:

My understanding is that precomposition is a classic example of a logical functor, which should preserve everything in sight.

It took me until this morning to remember why this isn't accurate. An arbitrary functor between categories induces an essential geometric morphism between the corresponding presheaf categories. You may have been thinking of composition with a morphism in a topos, aka a base change geometric morphism, which does have logical inverse image functor.
In order to show that (or whether) the functors you describe do produce logical functors, there is non-trivial work to do.

Morgan Rogers (he/him) (Feb 11 2021 at 09:35):

I hope that's helped. Thanks for taking all my comments on board in such good faith :grinning:

John Baez (Feb 11 2021 at 16:54):

Morgan Rogers (he/him) said:

Christian Williams said:

My understanding is that precomposition is a classic example of a logical functor, which should preserve everything in sight.

It took me until this morning to remember why this isn't accurate. An arbitrary functor between categories induces an essential geometric morphism between the corresponding presheaf categories. You may have been thinking of composition with a morphism in a topos, aka a base change geometric morphism, which does have logical inverse image functor.
In order to show that (or whether) the functors you describe do produce logical functors, there is non-trivial work to do.

I felt embarrassed that I didn't know whetherthe inverse image along an arbitrary functor is a logical functor between their presheaf categories. I knew it produced an essential geometric morphism.

So when do they give logical functors? Hardly ever? (Obviously equivalences do.) Often?

Morgan Rogers (he/him) (Feb 11 2021 at 16:58):

The canonical projection from a Grothendieck construction (so, the relevant kind of fibration) is an example of a functor which produces an étale geometric morphism (a localic geometric morphism with logical inverse image functor), since those correspond to the canonical gms from slice toposes over presheaves over the codomain.

Morgan Rogers (he/him) (Feb 11 2021 at 17:03):

Generally speaking, the inverse image functor of an essential geometric morphism does inherit some properties from the functor generating it. You can use the Frobenius reciprocity condition to work out how far cartex functors induce cartesian-closed inverse image functors, but I see no reason why subobject classifiers should be respected by these functors.

Mike Shulman (Feb 12 2021 at 05:40):

Morgan Rogers (he/him) said:

The canonical projection from a Grothendieck construction (so, the relevant kind of fibration) is an example of a functor which produces an étale geometric morphism

That would be the Grothendieck construction on a functor to Set, i.e. a discrete fibration, right?

Mike Shulman (Feb 12 2021 at 05:41):

In general, a geometric morphism whose inverse image functor is logical is called atomic. I don't know an exact characterization of the functors between small categories that produce atomic geometric morphisms, but they're more general than the etale ones. For instance, the functor $BG\to 1$ has this property, for any group $G$.

Christian Williams (Feb 20 2021 at 02:41):

Wrote a first blog post, about the language of a topos. https://golem.ph.utexas.edu/category/2021/02/native_type_theory.html

Christian Williams (Feb 20 2021 at 02:52):

comments and questions are welcome.

Morgan Rogers (he/him) (Feb 20 2021 at 09:51):

The presentation of dependent type theory is nice, I think @Jason Erbele would benefit from reading it after the discussion in #learning: questions yesterday. The monoid example you give is appealing, but it's a bit scary that in the presentation of "the type of monoids",
$\mathrm{Monoid}:= \Sigma M:\mathrm{Set}.\Sigma m:M^2\to M.\Sigma e:1\to M...$
you have to index over the universe, $\mathrm{Set}$, of basic types. You say that the rich language of dependent types is available in any topos, but this particular example is not expressible in the topos of sets (unless you get into the universe business) because it's not indexed over a type! It's still a conceptually good example for illustrating dependent types, just beware of the dragons :wink:

Morgan Rogers (he/him) (Feb 20 2021 at 10:05):

Mike Shulman said:

In general, a geometric morphism whose inverse image functor is logical is called atomic. I don't know an exact characterization of the functors between small categories that produce atomic geometric morphisms, but they're more general than the etale ones. For instance, the functor $BG\to 1$ has this property, for any group $G$.

I forgot to actually post this comment: the étale morphisms are exactly the localic atomic morphisms, and these do correspond exactly to the discrete fibrations. Also, any group homomorphism $G \to H$, viewed as a functor, induces an atomic geometric morphism, and the hyperconnected-localic factorisation of that morphism corresponds to the surjection-injection factorisation of the homomorphism; the morphism $[G^{\mathrm{op}},\mathrm{Set}] \to \mathrm{Set}$ is the special case of this for the unique morphism to the trivial group.

Mike Shulman (Feb 20 2021 at 16:06):

Morgan Rogers (he/him) said:

this particular example is not expressible in the topos of sets (unless you get into the universe business)

Well, the simplest solution is to get into the universe business. All (Grothendieck) toposes have universes as soon as the ambient set theory does.

Fawzi Hreiki (Feb 20 2021 at 16:17):

Anyway, the indexing is meta-theoretic no? The same way any LCCC has dependent types without needing universes

Morgan Rogers (he/him) (Feb 20 2021 at 16:18):

I wasn't saying that the presentation didn't make sense, just that it wasn't "in the language of the topos" without some caveats.

James Wood (Feb 20 2021 at 16:22):

Fawzi Hreiki said:

Anyway, the indexing is meta-theoretic no? The same way any LCCC has dependent types without needing universes

Indexing lets you get as far as saying what it means to be a monoid over a given set, but you can't collect up all the monoids (over different sets) without a universe (or maybe existential types).

Morgan Rogers (he/him) (Feb 20 2021 at 16:31):

Mike Shulman said:

Morgan Rogers (he/him) said:

this particular example is not expressible in the topos of sets (unless you get into the universe business)

Well, the simplest solution is to get into the universe business. All (Grothendieck) toposes have universes as soon as the ambient set theory does.

Sure, and that can work for Christian's project since he's currently looking specifically at presheaf toposes, but none of the dependent type theory outside of that example in the blog post is foundation-dependent as far as I can tell, so going to the trouble of invoking universes seems a bit much.

Mike Shulman (Feb 20 2021 at 18:14):

I think people should get over the idea that there's anything "much" about universes. (-:

Mike Shulman (Feb 20 2021 at 18:15):

There's nothing special about presheaf toposes, by the way; sheaf toposes have universes too.

Mike Shulman (Feb 20 2021 at 18:15):

(As long as the metatheory does.)

Christian Williams (Feb 21 2021 at 01:12):

yes, good points, thanks.

Christian Williams (Feb 22 2021 at 03:12):

@Mike Stay had a really good response on the blog post, and I just wanted to share it here as well. I don't yet have the real-world programming background to give very many compelling applications of native types, but Mike certainly does, and here's an example.

https://golem.ph.utexas.edu/category/2021/02/native_type_theory.html#c059431

John Baez (Mar 02 2021 at 18:02):

@Christian Williams: this sentence in the abstract of David Spivak's new paper seems at least slightly relevant to your interest in native types via topos theory and also "coalgebras for dynamics":

Finally, we review the fact that the category p-Coalg of dynamical systems on any p∈Poly forms a topos, and consider the logical propositions that can be stated in its internal language.

Christian Williams (Mar 21 2021 at 17:06):

Hi all, here is the second post Native Type Theory: Part 2. We present higher-order algebraic theories, the kind of categories which represent languages from which we build native type systems.

Christian Williams (Mar 21 2021 at 17:06):

In Part 3 (coming soon), we explore the native type system -- the internal language of the presheaf topos -- of a concurrent language.

Stelios Tsampas (Mar 21 2021 at 22:19):

Which concurrent language is this?

Christian Williams (Mar 21 2021 at 23:54):

The $\rho$-calculus. It's the $\pi$-calculus, plus operators which control the distinction between data and code.

Christian Williams (Mar 21 2021 at 23:54):

links to references are in the blog post.

Jason Erbele (Mar 23 2021 at 00:02):

Did you see the comment I made on Part 1 about 3 weeks ago? Type theory is at the edge of my understanding, so I had some fairly basic questions about what's going on.

John Baez (Mar 23 2021 at 04:33):

Here is Jason's comment:

https://golem.ph.utexas.edu/category/2021/02/native_type_theory.html#c059457

I hope @Christian Williams or someone answers it!

Christian Williams (Mar 23 2021 at 07:33):

ah, sorry! yes, I can answer tomorrow.

Cody Roux (Mar 23 2021 at 15:45):

There's some nice slides by Jeremy Avigad that somewhat justify the use of dependent (or indexed) types of this sort all over the place in mathematics. I think these are they https://www.andrew.cmu.edu/user/avigad/Talks/fields_type_theory.pdf

Cody Roux (Mar 23 2021 at 15:47):

But examples abound! One example is the definition of a category! Usually you have objects A, B and then for each pair of objects, you have an indexed family Hom(A, B). Obviously you could have one big set Hom and then functions dom, codom : Hom -> Obj but the other way is how we actually think about things. I think this is why it is claimed to be "natural".

Christian Williams (Mar 23 2021 at 23:57):

Thanks! That's perfect. @Jason Erbele

Christian Williams (Mar 23 2021 at 23:58):

also I responded to your question

Christian Williams (Mar 30 2021 at 03:40):

Here is Native Type Theory : Part 3.

We take a concurrent language called the $\rho$-calculus, represented as a second-order algebraic theory with rewriting, and embed it into the category of presheaves. The internal language of the presheaf topos is the native type system of the $\rho$-calculus, and we explore this highly rich and expressive system.

Christian Williams (Mar 30 2021 at 03:41):

phiT.png

Christian Williams (Mar 30 2021 at 03:44):

Given a theory, the all-powerful Yoneda embedding gives us a rich environment in which to reason about the structure and behavior of terms in the language. That's the whole idea of native type theory; it's extremely simple in theory, but potentially extremely useful in practice.

Christian Williams (Mar 30 2021 at 03:46):

I've included more pictures in the last two posts, so hopefully that makes them more engaging. I can include more here to help conversation. Mainly I'm just happy to hear your thoughts.

Morgan Rogers (he/him) (Mar 30 2021 at 11:54):

Wow you're churning this out quickly

Naso (Mar 31 2021 at 14:20):

Hi @Christian Williams

I had a couple of questions about the beginning of the paper:

Q1: On p2 you said

"In Hoare logic [18], assertions are predicates on the valuation of a memory heap. The triples $\{φ\}C\{ψ\}$, which express that if $φ$ holds and command $C$ is applied then $ψ$ holds, are modelled as the preimage $F^{-1}(C)$"

What actually is $F$ and how does its preimage $F^{-1}(C)$ model $\{φ\}C\{ψ\}$? I'm confused because how can the preimage know about $φ$ and $ψ$?

Q2: On p1 you mentioned a "rely-guarantee" operator. I know about the rely-guarantee quintuples $\{r,φ\}C\{g,ψ\}$ that generalise Hoare triples to concurrency and are interpreted roughly as "if the program is executed in a state satisfying $φ$ then while the environment satisfies $r$ the program will satisfy $g$ and then (possibly) terminate in state satisfying $ψ$". How could this quintiple formulation be interpreted in Native Type Theory?

EDIT: I guess the answer to my Q1 may be in the cited reference "Functors are Type Refinement Systems". I scanned over that now but it seems I don't know enough type theory to understand it. Q3: Can you please recommend a reference to get up to speed with the type theory needed to understand that and your paper? (I am ok with basic category theory but I never studied type theory).

Thank you.

Christian Williams (Mar 31 2021 at 17:21):

Hi Nasos, thanks for the questions. For Q1, I mean to say the preimage of some command $C$ is the set of all such triples. The fiber over each object in the base is the poset of predicates $\varphi$, and the fiber over each morphism would be this set of triples.

For Q2, the term "rely-guarantee" was provided by @Mike Stay. I don't know about its various uses; here it only means that $\varphi\multimap \psi$ is the set of all $f:A\to B$ such that $\varphi(a)\Rightarrow \psi(f(a))$. So "relying" on an input of type $\varphi$, we can "guarantee" an output of type $\psi$. That's all we mean there.

As for how this quintuple could be interpreted in NTT, that's a good question. I need to think about it.

Christian Williams (Mar 31 2021 at 17:25):

The main reference for the type theory is Jacobs' Categorical Logic and Type Theory. It is about how fibrations model many kinds of languages, where the fiber over a context are the types and terms one can derive in that context.

Christian Williams (Mar 31 2021 at 17:26):

Hope this helps; I can provide more information. Thanks for the questions.

John Baez (Mar 31 2021 at 18:15):

In Q1 Nasos asked "what is $F$?" Can you say what is $F$?

Mike Stay (Mar 31 2021 at 19:07):

I got the "rely-guarantee" terminology from Caires, who said $\phi \rhd \psi$ is the type of $\pi$-calculus processes that when run in parallel with a process of type $\phi$, the pair necessarily eventually evolves to a process of type $\psi$.

Christian Williams (Mar 31 2021 at 19:42):

sorry, $F:E\to B$ is an arbitrary functor in Functors are type refinement systems (Mellies/Zeilberger). they give a syntax for functors, which is most interesting and useful when $F$ is a monoidal closed bifibration. a main example they use is Hoare/separation logic.

Christian Williams (Apr 02 2021 at 19:17):

I want to share more examples of the expressiveness of native type theory.

Christian Williams (Apr 02 2021 at 19:18):

The main language from the paper is the $\rho$-calculus, which is presented as follows.

Christian Williams (Apr 02 2021 at 19:18):

rho-calculus.png

Christian Williams (Apr 02 2021 at 19:19):

This looks like a lot, but you can just focus on a couple chunks.

Christian Williams (Apr 02 2021 at 19:20):

rho-calculus_1.png

Christian Williams (Apr 02 2021 at 19:20):

Here are the constructors.

Christian Williams (Apr 02 2021 at 19:21):

rho-calculus_3.png

Christian Williams (Apr 02 2021 at 19:21):

Here are the main rules.

Christian Williams (Apr 02 2021 at 19:23):

It is a concurrent language, $-\vert -$ is parallel composition of processes. When there are two processes which input and output on the same name (channel) in parallel, they can communicate : the output sends a process, it is packaged up as a message using the reference operator "@", and it is substituted for the free name in the input process.

Christian Williams (Apr 02 2021 at 19:23):

That's really the core of the whole language. In general, processes are just huge parallels of outputs and inputs on different channels, and computation progresses by communication.

Christian Williams (Apr 02 2021 at 19:24):

So, I'm happy to talk more about this but I wanted to give an example. The native type system of this language is very rich.

Christian Williams (Apr 02 2021 at 19:25):

In this theory, we have a graph of processes and rewrites between them $s,t:E\to P$. All rewrites are generated from the basic communication rule, plus some rules at the bottom of that bigger presentation above, which allows for rewrites to happen inside parallels.

Christian Williams (Apr 02 2021 at 19:26):

This graph is the space of all possible computations that can occur in this language. Using native type theory, we can study and explore this space effectively.

Christian Williams (Apr 02 2021 at 19:28):

In particular, suppose we have a type of process $\varphi : T(-,P)\to \mathsf{Prop}$. This is a sieve in the theory, a type of process closed under substitution, which satisfies some property.

Christian Williams (Apr 02 2021 at 19:30):

For example, this could be the type for "liveness and safety", $\square (in(\alpha, N.P) \land \neg in(\neg \alpha, N.P))$ : the type of process which always inputs on a set of channels $\alpha$, and never inputs on $\neg \alpha$.

Christian Williams (Apr 02 2021 at 19:31):

So given two such types of processes $\varphi,\psi: T(-,P)\to \mathsf{Prop}$, we could filter to the subgraph of all computations whose source is $\varphi$ and whose target is $\psi$.

Christian Williams (Apr 02 2021 at 19:33):

This is constructed by the composite $T(-,E)\xrightarrow{\langle s,t\rangle} T(-,P)^2\xrightarrow{ \varphi\times \psi} \mathsf{Prop}^2\xrightarrow{\land} \mathsf{Prop}$.

Christian Williams (Apr 02 2021 at 19:35):

Hence we can use the type "computations which start with property $\varphi$ and end with security property $\psi$."

Christian Williams (Apr 02 2021 at 19:37):

Moreover, focusing on the one main rewrite rule of the $\rho$ calculus, we can filter computations by specifying exactly how communication should happen.

Christian Williams (Apr 02 2021 at 19:38):

We can say "give me all computations where the output process is $\varphi$ and the input process is $\psi$, and also the data that is being sent is of type $\alpha$."

Christian Williams (Apr 02 2021 at 19:39):

and much more. Native types can provide highly expressive and fine-grained specification of the space of communication happening on networks running on the $\rho$-calculus.

Christian Williams (Apr 02 2021 at 19:40):

I can draw up some pictures of this example to make it more clear and vivid. Please let me know any questions or thoughts.

Christian Williams (May 10 2021 at 18:57):

New version of the paper: Native-Type-Theory.pdf. (will be on the arXiv Wednesday)

Christian Williams (May 10 2021 at 18:58):

The story has gotten simpler and better. Our theories are "$\lambda$-theories with equality", meaning cartesian closed categories with finite limits. This expands the expressiveness, and allows the construction to be 2-functorial.

Jade Master (May 10 2021 at 23:26):

Nice

Jon Sterling (May 10 2021 at 23:40):

Christian Williams said:

The story has gotten simpler and better. Our theories are "$\lambda$-theories with equality", meaning cartesian closed categories with finite limits. This expands the expressiveness, and allows the construction to be 2-functorial.

Ah, very good. Remind me what you had before?

Christian Williams (May 11 2021 at 00:31):

we were using "higher-order algebraic theories", developed by @Nathanael Arkor and Dylan McDermott generalizing Fiore and Mahmoud's second-order algebraic theories.

Christian Williams (May 11 2021 at 00:33):

these are very nice because they correspond to monads, and the strength of these monads with respect to "substitution monoidal structure" provides a formal categorical method of variable binding and capture-avoiding substitution. Fiore slides

Christian Williams (May 11 2021 at 00:34):

but we were not using these ideas in the native types construction, so we decided to simplify and work with CCCs.

Jon Sterling (May 11 2021 at 01:17):

OK cool, thanks! Fiore & Mahmoud's stuff, and what came after, is very very elegant --- but I too have found in practice that it ends up being easiest for my intended applications to just work with either CCCs or LCCCs.

Tom Hirschowitz (May 11 2021 at 06:00):

Does anyone understand the link between this native type theory approach and gluing? I'm kind of asking while @Jonathan Sterling is around in the hope that he would :innocent: . Indeed, gluing looks a bit like a restriction of native type theory to closed terms, and predicates with a fixed arity. So, e.g., is there a sense in which native type theory embeds most forms of gluing? Or, for a more negative question, does native type theory make as much computational sense as gluing does (through realisability)?

Jon Sterling (May 11 2021 at 06:07):

Tom Hirschowitz said:

Does anyone understand the link between this native type theory approach and gluing? I'm kind of asking while Jonathan Sterling is around in the hope that he would :innocent: . Indeed, gluing looks a bit like a restriction of native type theory to closed terms, and predicates with a fixed arity. So, e.g., is there a sense in which native type theory embeds most forms of gluing? Or, for a more negative question, does native type theory make as much computational sense as gluing does (through realisability)?

I would say that these are diferent constructions, but the topos of presheaves on a language often serves as an input to a gluing construction --- for instance, this is how we proved normalization for cubical type theory. My idea from a few years ago, which thankfully panned out, was that we could obliterate all the complexities of Tait-computability arguments for type theories and programming languages by first turning a PL into a topos (whose internal language Christian is calling its "native type theory"), and then gluing this topos onto another topos that models whatever semantic thing I want to prove.

Taking presheaves on your syntactic category gives you a type theory that extends your existing language and speaks only of notions that make sense for open terms and are closed under substitution. But many statements about a language are not of this form: they may be statements about closed terms, or they may be statements about open terms but stable only under some substitutions, etc...

In this case you can consider a functor $\mathcal{D}\to \mathcal{C}$ into the syntactic category where $\mathcal{D}$ captures the shape of the contexts and substitutions you are going to be invariant under, and then take presheaves on $\mathcal{D}$. The result may not embed your language anymore (indeed, I guess it does not embed it unless $\mathcal{D}$ is a dense subcategory of $\mathcal{C}$), but it will be a place where various important notions about your language can be stated. But now you need to connect these things to $\mathcal{C}$! And that is what Artin gluing is for. In particular, you can embed your language into the Artin gluing of the inverse image to the induced essential morphism of topoi $\widehat{\mathcal{C}}\to\widehat{\mathcal{D}}$. This is what Johnstone calls the "closed mapping cylinder"; it is important to note that this is not usually an instance of sconing in the geometrical sense except in a few special cases, so it is unfortunate that this terminology has become so popular.

For intuitions, if you are studying closed terms, then $\mathcal{D}$ is the terminal category and the structure map sends $*$ to the empty context; in this case, the glued topos gives you an internal language that has the original "native type theory" as a open-modal subuniverse, and set theory as a complemetnary closed-modal subuniverse. On the other hand, if you are studying open terms up to renamings (but not substitutions), then $\mathcal{D}$ is a category of formal contexts and renamings and the structure map decodes these into actual contexts and actual substitutions.

Jon Sterling (May 11 2021 at 06:14):

The pertinent part of our paper on normalization for cubical type theory is Section IV ("The Computability Topos"). Unfortunately the exposition is very terse because of LICS length restrictions.

My thesis will be coming out soon, and there will be a much more leisurely introduction to these ideas.

Tom Hirschowitz (May 11 2021 at 06:47):

@Jonathan Sterling Thanks, this is very helpful! Looking forward to your thesis then. (I watched your talk at Augusta, which was also very helpful, but not quite enough for me to fully get how things work.)

Tom Hirschowitz (May 11 2021 at 10:20):

I couldn't resist and had a look at Section IV. It's actually quite readable, at least superficially. Congratulations for making such difficult material accessible!

What exactly is the scope of this technique? Until now, if I understand correctly, it has only been applied in this form to "congruent" languages, i.e., ones in which rewrite rules may be applied anywhere in the program --- that's rather informal, please don't hesitate to complain.

On the other hand, techniques like classical realisability kind of do similar things by hand.

Any guess on how easy it would be to apply it to, e.g., languages in the sense of bialgebraic semantics or transition monads?

Tom Hirschowitz (May 11 2021 at 10:24):

Of course, another framework for the congruent case is @Marcelo Fiore and @Philip Saville 's bicategorical construction.

Jon Sterling (May 11 2021 at 13:49):

Indeed, this method really only shines right now on languages that can be phrased as equational theories (for instance, by means of a congruent rewriting system or otherwise). I have been exploring lately what it looks like for languages where you have actual transitions that are not equational (in the sense of not being congruent, or in the sense of not being deterministic) --- such things can be expressed, but here one is likely to just be reconstructing standard operational arguments in a slightly nicer way, rather than demolishing them :wink:

Tom Hirschowitz (May 11 2021 at 16:18):

This sounds cool! Everything lies in the "slightly", which I suspect I'd find understated. What puzzles me at the moment is how you can tune the granularity, e.g., how you avoid being too intentional in the glued topos. Not exactly sure what I'm talking about here, but probably if you start with a syntactic category modulo rewriting, then individuals in the glued logic are only considered equivalent up to rewriting, right? Or can gluing make them equivalent up to something coarser like some contextual equivalence?

Jon Sterling (May 11 2021 at 16:42):

I have not explored trying to quotient by contextual equivalence, but generally I think this is a bad idea, because contextual equivalence is not modular. On the other hand, it is possible to use the gluing argument (modulo rewriting only) to establish contextual equivalences.

Jon Sterling (May 11 2021 at 16:43):

With that said, I think it is a very interesting question to try and phrase "respect for contextual equivalence" as perhaps some kind of orthogonality or lifting property in the gluing topos, and then one could investigate what connectives preserve this property! But I haven't thought about it. Perhaps this is something for you to try :)

Tom Hirschowitz (May 11 2021 at 16:49):

Maybe! The learning curve looks a bit frightening, but I might get to it at some point.

Christian Williams (May 11 2021 at 17:05):

great idea, to capture a certain shapes of contexts and substitutions you'd like to study. I'll have to think more about what this "closed mapping cylinder" is like. thanks for the overview.

Christian Williams (May 11 2021 at 17:08):

as for your subsequent discussion, I don't even know how rewriting comes into this picture at all. but I should mention, the idea of representing operational semantics using internal graphs in a theory is very expressive. it is not restricted to languages with congruent rewriting systems.

Tom Hirschowitz (May 12 2021 at 14:15):

Thanks @Christian Williams. Regarding rewriting, I got the -- apparently wrong -- impression that your framework used a notion of signature close to higher-order rewriting systems to generate languages. But yes, I agree with you that internal graphs are expressive, that's more or less what we use in transition monads. But then, what do you do exactly?

If you mod out by the graph (i.e., consider edges as equations), then that's probably too coarse in a few relevant examples, e.g., non-deterministic languages. Right?

If you retain the graph as a (proof-relevant) predicate in the logic, then (and this gets close to my earlier question about granularity) aren't you worryingly fine? E.g., in good old $\lambda$-calculus your logic isn't even invariant under $\beta$-reduction. Would you agree that this at least begs some discussion? Can gluing rectify this in some way?

Christian Williams (May 12 2021 at 17:20):

sorry, I'm not sure what you mean. the logic is very fine-grained, yes, but there should be ways to tune it... can you explain this desired beta invariance?

John Baez (May 12 2021 at 18:12):

@Tom Hirschowitz wrote:

If you mod out by the graph (i.e., consider edges as equations), then that's probably too coarse in a few relevant examples, e.g., non-deterministic languages. Right?

Yes. The pi calculus, one of the main examples in Christian's paper, is a perfect example of this. That's one of the main reasons Mike and Christian brought graphs into the game.

John Baez (May 12 2021 at 18:15):

If you retain the graph as a (proof-relevant) predicate in the logic, then (and this gets close to my earlier question about granularity) aren't you worryingly fine?

What does "worryingly fine" mean here, exactly?

Are you saying that two lambda-terms differing by just beta-reduction count as distinct in Mike and Christian's setup applied to the lambda-calculus? I guess that's right if we model beta-reduction as an edge of a graph.

Is that bad?

Jon Sterling (May 12 2021 at 22:39):

John Baez said:

If you retain the graph as a (proof-relevant) predicate in the logic, then (and this gets close to my earlier question about granularity) aren't you worryingly fine?

What does "worryingly fine" mean here, exactly?

Are you saying that two lambda-terms differing by just beta-reduction count as distinct in Mike and Christian's setup applied to the lambda-calculus? I guess that's right if we model beta-reduction as an edge of a graph.

Is that bad?

The "Is that bad?" thing is, I would say, one of the most important and deepest questions we have to deal with in PL (and type theory) right now... It's certainly the case that not modding out by beta-reductions is the source of 95% of the complexity in metatheoretic arguments for type theory and programming languages (those scary papers that have 200 pages of inductions), but there are many cases where you can't seem to mod out --- as you and Tom have pointed out, non-determinism is one of them.

My experience is that there is not usually a legitimate purpose (in the sense of being motivated by theorems that are of broad interest) to distinguishing beta redexes from their contracta, but that there are a variety of reductions (even deterministic ones) that probably we should distinguish because we have useful models that distinguish them. This arises, in particular, with recursive types and the so-called "unfold-fold" transitions.

Tom Hirschowitz (May 13 2021 at 06:12):

You're right, @John Baez and @Christian Williams, I'm not sure what I'm saying here. I guess it depends what you're planning to do with this native type theory. E.g., could you define some legitimate behavioural equivalence and prove some of its properties?

Jacques Carette (May 13 2021 at 13:06):

I would augment @Jonathan Sterling 's response regarding $\beta$-reduction in the following way: it makes little sense to regard two terms seen as values as different if they only differ by a $\beta$-reduction. But it makes a lot of sense to view two terms seen as computations as different in that same case.

So if computation is merely an ends to a means, then ignoring its process is fine.

When doing meta-programming of all sorts, often the main point is to shift computation around. One of the things we often want to do in meta-computation is to shift $\beta$-redexes from run-time to compile-time. So staging really cares a lot. One of the most basic things you keep track of in a partial evaluator is whether something is known to be a value (and thus it can be freely duplicated) or not (and so should be let-bound).

So in 1-stage PL seen as black-boxes for getting work done, indeed, we don't care. In other cases? I'd say we care a lot!

John Baez (May 13 2021 at 17:26):

I roughly understand what Jacques is saying and this is why I like working with graphs as Christian and Mike are doing: it's a way to treat terms as computations.

Jon Sterling (May 13 2021 at 17:52):

I feel ultimately it is a question of what you are trying to study. If you are trying to study the results of those computations, then it is going to be a major waste of time to differentiate between the different steps. If you are studying the steps themselves, then obviously we need to look at those directly! One methodological remark I would like to point out is, however, that in practice a mix of the two approaches is what is usually needed for most applications.

There is a reason, for instance, that while some people may be interested in studying the transition from fst(a,b) to a, nobody is interested in studying the transition from \x.M(x) to \y.M(y), etc. (Well, I may exaggerate when I say "nobody", but I hope my point is made that we are dealing with a spectrum, and where we end up on that spectrum can be determined by the applications we have in mind.)

John Baez (May 13 2021 at 17:55):

I guess I'd like an approach that lets you include something resembling 2-morphisms between all these syntactically different terms - even the ones "nobody is interested in" - and then lets you easily mod out by any 2-morphisms you don't happen to be interested in right now.

John Baez (May 13 2021 at 17:57):

In pure math, at least, it's generally easier to "mod out" when you decide you're uninterested in something you were paying attention to, than to "un-mod out" when you decide you're interested in something you were ignoring.

Jon Sterling (May 13 2021 at 17:59):

I like the 2-categoric approach too (and you get interesting stuff when you go beyond 2-categories too!). I think there is room for a bit of controversy, however, about whether some of these things should be dealt with by non-identity cells: for instance, there is a question of whether terms are graphs with distinguished back-edges denoting variable binding sites, or if they are strings. You could consider the string presentation and then add a lot of 2-cells that express the fact that adding parentheses around certain sub-strings is a no-op... And indeed, you can mod out by these if you consider them unimportant. But at some point you have to ask, why am I talking about strings in the first place? Maybe terms are actually graphs... In which case these 2-cells for dropping parentheses really don't make any sense...

Jon Sterling (May 13 2021 at 18:00):

In the end, as I say, it must keep coming down to whether you haev an interesting theorem to prove that would depend on being able to see (e.g.) the parentheses. If you do, then I really welcome the integration of them into some higher structure that can then be modded out later if one wishes to access a higher level of abstraction. But if you don't, then we shouldn't be doing it... Various low-level representations of things did not fall from the sky: human beings invented them. So categorification has to take into account not only what exists, but also what the intention was behind what exists.

John Baez (May 13 2021 at 18:07):

Yes, I'm just a mathematician, so I don't know much about what syntax computer scientists actually care about, and I don't actually have any interesting theorems to prove on this subject; I just want to be able to describe whatever is going on without being forced to identify things that don't look equal to me.

John Baez (May 13 2021 at 18:56):

So, my humble job would be merely to provide tools...

Jon Sterling (May 13 2021 at 21:20):

If you are mainly providing tools to be used by others, then I hope you will take our advice as to will and will not be useful to us ;-) But I do appreciate the distinction you are making and am, as always, very excited to see what you come up with.

Christian Williams (May 13 2021 at 21:42):

Jonathan Sterling said:

I like the 2-categoric approach too (and you get interesting stuff when you go beyond 2-categories too!). I think there is room for a bit of controversy, however, about whether some of these things should be dealt with by non-identity cells: for instance, there is a question of whether terms are graphs with distinguished back-edges denoting variable binding sites, or if they are strings. You could consider the string presentation and then add a lot of 2-cells that express the fact that adding parentheses around certain sub-strings is a no-op... And indeed, you can mod out by these if you consider them unimportant. But at some point you have to ask, why am I talking about strings in the first place? Maybe terms are actually graphs... In which case these 2-cells for dropping parentheses really don't make any sense...

I don't understand what you're saying about terms as graphs or strings; to me a term is just its abstract syntax tree. as for the 2-categorical aspect, John and I considered enriched theories for languages with rewriting; but only more recently I realized that these only work for congruent rewriting systems, not more general operational semantics. though maybe that's enough for many applications you care about.

Christian Williams (May 13 2021 at 21:46):

More generally in the discussion, this is why I think it's significant that native type theory combines reasoning about both structure and behavior. If the type system of the presheaf topos is initially too fine-grained for your purposes, we can restrict to subsystems which only make certain distinctions. We can quotient and reason up to behavioral equivalence.

John Baez (May 13 2021 at 22:45):

Jonathan Sterling said:

If you are mainly providing tools to be used by others, then I hope you will take our advice as to will and will not be useful to us ;-)

That makes plenty of sense. I was trying to weasel out of this responsibility but I didn't really give the true reason. The real reason is that it's @Christian Williams and @Mike Stay who are taking the lead on of this project, with me just providing a bit of category-theoretic assistance as Christian's thesis advisor. So I hope you keep talking about these issues, but I'll let them focus on the "practical" issues while I focus on the math questions that come up.

Jon Sterling (May 14 2021 at 12:21):

Christian Williams said:

Jonathan Sterling said:

I like the 2-categoric approach too (and you get interesting stuff when you go beyond 2-categories too!). I think there is room for a bit of controversy, however, about whether some of these things should be dealt with by non-identity cells: for instance, there is a question of whether terms are graphs with distinguished back-edges denoting variable binding sites, or if they are strings. You could consider the string presentation and then add a lot of 2-cells that express the fact that adding parentheses around certain sub-strings is a no-op... And indeed, you can mod out by these if you consider them unimportant. But at some point you have to ask, why am I talking about strings in the first place? Maybe terms are actually graphs... In which case these 2-cells for dropping parentheses really don't make any sense...

I don't understand what you're saying about terms as graphs or strings; to me a term is just its abstract syntax tree. as for the 2-categorical aspect, John and I considered enriched theories for languages with rewriting; but only more recently I realized that these only work for congruent rewriting systems, not more general operational semantics. though maybe that's enough for many applications you care about.

I don't care about terms, there are many possible representations --- I was just giving some examples of why it might not be obvious in principle that it is good to treat certain things as non-identity cells.

Your point about congruence is quite apt... The ironic thing is, I think that the place where we most need to bring high-powered category theory to bear is in figuring out what is going on with the non-congruent rewriting systems that appear in most current-day PL work. History has shown that a more careful analysis of these systems (as in the work of Paul Blain Levy and many others) leads to (1) isolating universal properties for connectives that appeared not to have universal properties, and (2) replacing incongruent rewriting systems with congruent ones --- or at least, decomposing the incongruent part of the rewriting system from the congruent part.

And I agree with you that having a single language in which you can do both kinds of reasoning is very good, which is why I am such a fan of the lightweight way that you integrate rewriting into your framework.

Nick Hu (May 17 2021 at 10:10):

Paul Blain-Levy addresses this in his lambda calculus course by working over 'binding diagrams' (https://www.cs.bham.ac.uk/~pbl/mgsall.pdf section 7) instead of terms-quotiented-by-alpha-equivalence, to give a concrete example