Architectural Changes & Example Programs

[rdck]

Hello!

@favonia kindly took some time recently to help me understand the project. They suggested that this is a good place to communicate.

I was surprised to find that the type theory is no longer "computational" in the sense of NuPRL and RedPRL! I'm sure it will take me some time to understand the problems you encountered there. If there is anything written down about the motivation for that change, that would be helpful.

For my own understanding, I will try to write at least a few example programs, and understand the existing ones. Can I suggest that if anyone has an illustrative example in mind that isn't already included, they might briefly describe it here, so I can try writing it? I assume you want to focus on cubical-specific features in the examples.

I could also try adding some explanatory commentary to the existing examples to make them a bit more readable, though I'm not confident I'll be able to understand them all without help.

Thanks

[jonsterling]

Hi @outerpassage, thanks for your interest!

I will try to be as transparent as possible about the reasons for the different architecture; we had both semantic and syntactic reasons for switching from the PRL architecture:

1. The semantic reason is that PRL-style formalisms tend to have only realizability-style models, but as our research interests have evolved, it has become important for us that theorems proved in one of our tools have useful consequences in ordinary mathematics too, in addition to the computational models. In particular, we wanted it to be possible to use our tools to prove theorems about actual spaces in the traditional sense so that our research can make contact with the actually existing applications of higher-dimensional type theory.

2. The syntactic reason is that we have found PRL-style formalisms to inhibit automation of basic well-formedness conditions, making it exceedingly difficult to prove what should be very easy theorems; while this can be seen already without cubical machinery, I think the problem becomes more clear in cubical type theory because almost none of the important equations that need to be automated can take the form of untyped rewrites. In classic PRL systems, more (but not all) of the equations that needed automating could be phrased as untyped rewrites and therefore it was more frequently possible to solve them automatically; cubical type theory adds context-sensitive rewrites involving boundaries (e.g. if r = s or t = u, then M needs to reduce to N).

My experience with PRL-style formalisms is that one expects to use (e.g.) equality reflection to make a very hard problem very easy, but what happens in practice is that you are mostly making a lot of use of equality reflection in order to painstakingly convince the system that C[\x. f(x)] can be replaced with C[f] very deep in some very complicated term context C[-] --- something that is automatic in type-based approaches like those that we have now adopted. As mentioned above, these difficulties are compounded when the desired identification is more sensitive to context, which is what happens in cubical type theory.

These two 'reasons' come together in the following place: PRL systems usually emphasize (and take advantage of) various untyped principles that are true only in computational/realizability-style models, and these untyped principles let you do some pretty cool stuff. But we were surprised to learn that most interesting untyped principles of these kind are not true in the computational/realizability-style model of cubical type theory, hence one could not get much mileage out of them even if one was not interested in mathematical applications. For these reasons, we switched to type-based techniques including normalization-by-evaluation and bidirectional elaboration, a style that has been shown to work very nicely for everything from logical frameworks to very powerful type theories.

So what do we retain from the PRL experience? Our implementation is still based on proof-refinement, just like Nuprl/RedPRL, and we use tactics as an organizing principle for our elaborator. On the semantic side, we retain the computational interpretation which we find to be of both philosophical and practical importance; on the syntactic side, we actually have a stronger computational interpretation in the sense of supporting computation with open terms in a way that is sound and complete for judgmental equality, rather than only computation with closed terms. (See the recent result of Carlo and me: http://www.jonmsterling.com/pdfs/cubical-norm.pdf)

There is another thing we lost, which is the presence of exact equality pretypes that Nuprl/RedPRL had (meaning, equality types with equality reflection). These are a very important aspect of our current understanding of higher-dimensional type theory, because they enable the solution to certain coherence problems involved in the construction of homotopy-coherent notions such as higher-categories, etc. The downside is that they disrupt automation of typechecking; while some researchers are working to develop better typechecking heuristics in the presence of exact equality types (e.g. the recent work of Bauer & Petkovic), we are taking the view for now that various special cases of equality reflection can be considered that would do what is needed without disrupting the properties of the system like full equality reflection would; in fact, cubical type theory itself and its interval and cofibration machinery can be seen as introducing some special cases of equality reflection in a controlled way, just as the where type foo = bar clauses of SML and OCaml's module systems can seen to be controlled introduction of equality reflection.

[jonsterling]

Btw if you are curious about examples that illustrate the difference between the PRL approach and the type-based approach that we have adopted, check out the following implementations of the same lemma in RedPRL and redtt:

• RedPRL: https://github.com/RedPRL/sml-redprl/blob/master/example/invariance.prl#L54
• redtt: https://github.com/RedPRL/redtt/blob/master/library/cool/invariance.red#L130

The above illustrates how the type-based approach of redtt/cooltt manages to totally automate well-formedness conditions, whereas a pretty complex tactic script with a lot of equational reasoning is required to convince RedPRL that the term was well-formed. This is somewhat paradigmatic of the different experiences between *PRL and *tt; one interesting thing is that the RedPRL proof actually takes advantage of equality reflection to see that C[x] == if x then C[tt] else C[ff], whereas redtt must treat this as a path -- but the redtt version was nonetheless easier.

Similar examples that likewise illustrate the difference in ability-to-automate are:

• RedPRL: https://github.com/RedPRL/sml-redprl/blob/master/example/invariance.prl#L161
• redtt: https://github.com/RedPRL/redtt/blob/master/library/cool/invariance.red#L150

[rdck]

Thank you for such a detailed response!

I understand you to mean by (1) that types in the PRL-style formalisms, which I think of as specifications of behaviour, cannot be interpreted as traditional spaces in the same sense that types in the intrinsically-typed formalisms can. Is that correct?

If that is what you meant, the only potential reason I can think of is that having the untyped rewrite rules available means it's possible to write down strange-looking terms that aren't interpretable as points. For example, you might write something like if true then base else 42, which should be a perfectly valid term of type S1 in a PRL-style formalism, but perhaps doesn't correspond to anything sensible in the other models you have in mind. Is that right?

I'm not sure I understand what you mean when you say that "most interesting untyped principles of these kind are not true in the computational/realizability-style model of cubical type theory". AFAIK, such untyped principles (i.e. NuPRL's intersection types) do not usually have a direct logical meaning, for example as products do as conjunctions, so what would it mean for them to be true in a model?

[jonsterling]

Re: your first couple paragraphs, I think that's a good summary of the kind of issue at hand, yes.

For your final paragraph, let me try to clarify things. What I mean is that a PRL typically contains various principles involving untyped computation, and these are interpreted and validated by Nuprl's PER semantics; that is what I mean for them to be true in the computational/realizability/PER model.

An example of an untyped computation rule (i.e. one that can be applied without any additional typing premises) that is valid in Nuprl's PER semantics is the one that reduces if tt then M else N to M regardless of the types of everything; while this untyped rule remains valid in cubical type theory's PER semantics, the corresponding rule for the circle that would reduce case loop(x) of base => M | loop(y) => N(y) to N(x) in an untyped way is actually false in the cubical PER semantics. Of course, there is a typed beta law that corresponds to this, but the untyped rule doesn't hold. But this is only the tip of the iceberg...

[rdck]

Ah, thanks, that's very clear. We can leave the rest of the iceberg for another time.

[RobertHarper]

Having said all that, it must be understood that the computational formulation is a realization of Brouwer’s conception of truth based on computation.  And, as demonstrated amply in NuPRL, there are concepts that only make sense, or are only known to make sense, with respect to the computational meaning, types as specifications.  It is true that there are tensions with the cubical apparatus, but then again the computational applications of cubes are relatively thin on the ground.  So we shall see how things shake out.  For now, there are two views of type theory, a form of algebra, and a form of program specification/verification.  Both are interesting and important, and it is clear that the cubical methods are best-suited to the algebraic setup. Bob (c) Robert Harper.  All Rights Reserved.

…

On Mar 18, 2021, 22:23 -0400, River Dillon ***@***.***>, wrote: Ah, thanks, that's very clear. We can leave the rest of the iceberg for another time. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or unsubscribe.

[rdck]

I'm wondering whether the tensions that @jonsterling described are fundamental, in the sense that they will appear in any univalent computational formulation with HITs. Not that I have any alternate presentations in mind, but I imagine that the cubical style with syntactic intervals likely isn't the only possible approach.

It seems to me that the semantic issue (1) is serious if you require that types be interpreted exactly as traditional spaces, but shouldn't mean that theorems about "computational spaces" aren't interesting in their own right. S1 in a computational setting might not be exactly the circle you're used to, but it's still at least "circle-like" in some sense.

Forgive me for presumably retreading old ground here.

[jonsterling]

I think computational spaces are an interesting topic that is worthy of study in its own right! In the same sense that people study what mathematics looks like under realizability.

…

On Fri, Mar 19, 2021, at 7:14 PM, River Dillon wrote: I'm wondering whether the tensions that @jonsterling <https://github.com/jonsterling> described are fundamental, in the sense that they will appear in *any* univalent computational formulation with HITs. Not that I have any alternate presentations in mind, but I imagine that the cubical style with syntactic intervals likely isn't the only possible approach. It seems to me that the semantic issue (1) is serious if you require that types be interpreted exactly as traditional spaces, but shouldn't mean that theorems about "computational spaces" aren't interesting in their own right. S1 in a computational setting might not be exactly the circle you're used to, but it's still at least "circle-like" in some sense. Forgive me for presumably retreading old ground here. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#186 (reply in thread)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAANOEJJAFEUSPGS4KG35VDTEPLETANCNFSM4ZLXSGIA>.