Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

Well, yes, it's a functional programming language. But not one like most people here are familiar with, so that's a little misleading. It's also an object-oriented language with polymorphism and inheritance.

Specifically, it's (almost exactly) the Calculus of Constructions (http://en.wikipedia.org/wiki/Calculus_of_constructions), the language at the top of the lambda cube (http://en.wikipedia.org/wiki/Lambda_cube).



No, HoTT is not based on the Calculus of Constructions, but instead on intensional Martin-Loef type theory with identity typed. The novel part is the univalence axiom, which MLTT doesn't have.

If you erase types, the underlying programming language is the lambda-calculus, familiar to every programmer.


Yes, Vladimir Voevodsky says HoTT is based on Martin-Loef type theory, but he discovered HoTT by learning the CoC used in Coq, and is implementing his Univalent Foundations library of proofs in Coq. That implies that HoTT is implementable in Coq (with a couple of minor tweaks), which means that CoC is at least as powerful as HoTT. And anyway, according to Voevodsky, they are the same thing.

Really, Martin-Loef type theory is the mathematics foundation, and the Calculus of Constructions is the computer science foundation. HoTT ties them together.


It depends on what you mean by "embedding". If one does a deep embedding then powerful calculi can be embedded in much weaker calculi. E.g. Isabelle uses a variant to LF as meta-language to embed all manner of more powerful logics. That doesn't mean LF has a lot of expressive power.

Coq's logic isn't quite the CoC anymore: impredictivity is switched off by default, Coq has universes etc.

With this in mind, I'm not sure what Voevodsky means when he says HoTT and CoC are the same thing.


I would like to see more clarification of why you'd call HoTT OO. I have no doubt you can encode those things, but I find it strange to try to argue that it doesn't have more in common with the FP tribe than the OO tribe. Given that neither term is terrifically well-defined, I think that's the best you could argue.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: