Cubical Computational Type Theory

Stream: general

[Uros Nedic]

I would like to know if it is possible to use Cubical Computational Type Theory for everyday computing?

[Floris van Doorn]

(Cartesian) Cubical Computational Type Theory is a logical framework. You'd need an implementation of it to do everyday computing.
Given such an implementation, would it be possible to compute ordinary things? Yes. Would it be efficient? Probably not, similar to Lean's kernel computation.

[Floris van Doorn]

Part of the reason that Lean's kernel computation is bad is that we use unary natural numbers instead of binary ones. It would still be slow to compute things in the kernel, even if we optimize our definitions for computation. I have not tried it though, so I don't know how slow it would be compared to programming languages.

[Uros Nedic]

What is example of an implementation of Cubical CTT? And how it relates to HoTT? I thought that HoTT is framework.

[Floris van Doorn]

Cubical Computational Type Theory is a type theory, just as HoTT or CiC, or the type theory of Lean.
It was designed to give a computational meaning to the univalence axiom in HoTT. In HoTT (more precisely: the type theory of the HoTT book) the univalence axiom is an axiom and doesn't compute. In CCTT the "univalence axiom" is a theorem that can be proven using new primitives in the type theory. These primitives compute, and so does univalence.

[Uros Nedic]

Is RedPRL an example of implementation og CCTT?

[Floris van Doorn]

There are some big differences in the way Computational type theory works, compared to Formal(?) type theories (HoTT or CiC, or the type theory of Lean). In computational type theory you start with a programming language, and then "carve out" the programs which are well behaved and have a certain type, so you get the type theory second. In formal type theory the type theory comes first: you cannot talk about a term without telling me what type that term is. Computational type theory comes from a different tradition (c.f. NuPrl)

This means that I should probably take back my statement about efficiency: maybe implementations of CCTT can be as efficient as you want, in theory.

[Tim Daly]

In Cubical type theory, as I understand it, there is a path that can be traced around every face of the cube. Assuming one corner of the cube is a point it seems to me that every face attached to that point traces a closed path, making it the identity path. Topologically, then, the cube is isomorphic to the point. I suspect I'm wrong but it isn't clear why.

[Floris van Doorn]

There are different proof assistants of cubical type theory, some of those are also of cubical computational type theory. RedPrl is indeed an implementation of cubical computational type theory.

[Koundinya Vajjha]

But RedPrl development has ceased. Now it's redtt. I'm not sure if that is "computational" in the sense of computational type theory.

[Floris van Doorn]

Redtt is indeed the successor of RedPrl, and they dropped the computational aspect of the proof assistant.

[Floris van Doorn]

Other cubical proof assistants (none of them computational):
https://github.com/mortberg/yacctt
https://github.com/mortberg/cubicaltt

[Floris van Doorn]

https://github.com/agda/cubical

[Uros Nedic]

Thank you for all you answers (Carry on, I am glad to read this thread). My idea was if HoTT makes foundation for all mathematics than is it possible to develop some computing language from HoTT (let it be pure type-level programming, if necessary) like Cartesian CCTT or some 2-Level TT if needed, and then do everyday programming (software development) and proving our software as easy as proving math proofs because we would use Cat Theory, Topoi, etc., as objects in that programming language?