Hacker News Reader

I think Cubical Type Theory (derived from HoTT) is a part of the future for general-purpose dependently-typed programming -- it has canonicity, which I'd argue is necessary for a general-purpose programming language, and it being suitable for a foundation of mathematics nigh-guarantees it's powerful enough to express whatever properties are useful in the domain.

View on HN

> it has canonicity, which I'd argue is necessary for a general-purpose programming language

MLTT, even without HoTT/CTT, already features canonicity, no? (At least for positive types.)

I thought the main advantage of HoTT is that you can define non-trivial equalities, and the advantage of CTT in particular is that univalence can be derived in it (rather than introducing it as a non-computational axiom).

Right, I think I'd put univalence in my list of "I want this for my dream general-purpose dependently-typed programming language" features; being able to prove properties on simple representations of data and transport those properties to more optimized forms is pretty important, imo.

So you're saying that cubical type theory will be a good fit for cubical programming?

Reply on news.ycombinator.com