= 27d567bc2d48d9f40e9ccc20ea370b15)
Douglas_Knight comments on Open Thread, December 1-15, 2012 - Less Wrong Discussion
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (177)
You seem to be confusing intuitionist MLTT (c.1970) and HTT (c.2005). Your second and third links are about MLTT, not HTT. The second link does mention HTT in passing and claims that it is "a new interpretation of type theory," but this is simply false. In particular, your first quote is not about HTT.
Your first link really is about HTT, but does not claim that it is relevant to programming. HTT is an extension of type theory to reduce the impedance mismatch between logic and category theory, especially higher category theory. It is for mathematicians who think in terms of categories, not for programmers. In as much as programmers should be using category theory, HTT may be relevant. For example, Haskell encourages users to define monads, but does not require them to prove the monad laws. HTT provides a setting for implementing a true monad type, but is overkill. This is largely orthogonal to MLTT.
Automated theorem proving is rarely done, but it usually uses MLTT.
You are of course right about the distinction between MLTT and HTT, but Risto_Saarelma's first link is a computer science blog. In my view, the claim that computer scientists are "making noise" about homotopy type theory as applicable to programming is fairly justified: in particular, HTT might make it easier to reason about and exploit isomorphisms between data types, e.g. data representations.
Also, Martin-Lof type theory is not exclusively used for computer-assisted theorem proving: for instance, the Calculus of Constructions is one alternative. Formal work on HTT is done in Coq, which is based on the CoC.