News for hackers. Stuff that matters.

A comment on Relation Between Type Theory, Category Theory and Logic. Parent comment

Re:Relation Between Type Theory, Category Theory and Logic by rndn on Saturday July 11, 2015 @12:29PM (#9870387)
Doesn't the halting problem pose an obstacle in deciding whether two types act in an equivalent way (similar to how the equivalence between two programs is undecidable)?
[ Parent | on HN ]
Re:Relation Between Type Theory, Category Theory and Logic by eli_gottlieb on Saturday July 11, 2015 @01:37PM (#9870737)
No. Homotopy Type Theory is a total language, so even type-level programming simply has to terminate, or the proof-checker won't accept it.

Proving that nontrivially recursive programs terminate can be a bugger.

[ Parent | on HN ]
Re:Relation Between Type Theory, Category Theory and Logic by jonsterling on Saturday July 11, 2015 @02:16PM (#9870935)
You do not in general decide whether two types are equivalent. You prove it...
[ Parent | on HN ]
Re:Relation Between Type Theory, Category Theory and Logic by gallabytes on Saturday July 11, 2015 @01:21PM (#9870650)
Why would it do that? Univalence is unrelated to the halting problem.

What the univalence axiom says is that you can treat types you have proven isomorphic as equal.

[ Parent | on HN ]