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

Yeah... This is correct as far as I know though a bit out of my complete technical grasp. To my understanding MLTT was a fairly central topic and it helps to distinguish MLTT from just type theory since plain-old-TT might be harder to distinguish as something interesting above `(int *)`.

But, to solidify, mafribe is much more correct than my comment and there's, as far as I'm aware, a much larger menagerie of other type theories. The recent Homotopy Type Theory publication—which was on HN as notable due to its publication process—was yet another step in this direction.



Per Martin-Löf was instrumental in extending type theory to dependent types, although the first version of his dependent type theory was impredicative with Type:Type and was shown to be inconsistent by J.-Y. Girard. Subsequent versions of Martin-Löf type theory have been predicative, but other dependent type theories (such as the calculus of constructions) stuck with (more benign forms of) impredicativity.




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

Search: