8 ms·

Curious how approachable you think homotopy type theory is to people who think they know better than researchers? Simple type systems would be understandable (H

Curious how approachable you think homotopy type theory is to people who think they know better than researchers? Simple type systems would be understandable (Haskell has type systems similar to System F and rust has an affine your system) but if anything being a programmer may add obstacles to understand HoTT since programmers (generally) have never had the opportunity to learn topology or anything else that HoTT builds on. Also not everything in HoTT has a clear computational interpretation, notably the univalence axiom. That said I encourage everyone who's interested to investigate this but I don't think it's realistic without having a solid foundation in mathematics. (And I also agree with the sibling comment that HoTT isn't really used as a foundation of mathematics.)

stepchowfun 4y ago
I don't think it's an easy journey—not because the material is intrinsically difficult, but because almost all resources are written for mathematicians and computer scientists. I think a "homotopy type theory for programmers" book/blog/playlist could be a big hit. I've been considering putting something like that together. I view the relationship between HoTT and topology as similar to that of functional programming and category theory: you don't need to know the latter to learn the former, but having that extra background can certainly help.
- isaac21259 4y ago
  I was also considering writing some introductory stuff about HoTT but I don't think it's possible to avoid talking about topology, homotopy theory, and category theory in depth like you can with, say Haskell and category theory. This is because the stuff that makes HoTT so cool cannot be separated from it's mathematical foundations. How would you explain truncated types without going fairly deep into the math? Or the circle type? Sure both of these could be explained as instances of higher inductive types but that explanation is missing a lot.
  - Koshkin 4y ago
    As already has been done with category theory, you need to target a specific audience, whether it is programmers, scientists, engineers, or mathematicians, and illustrate the concepts by giving examples from their area of expertise, if possible.
- deleted 4y ago
  [deleted]

stepchowfun 4y ago

I don't think it's an easy journey—not because the material is intrinsically difficult, but because almost all resources are written for mathematicians and computer scientists. I think a "homotopy type theory for programmers" book/blog/playlist could be a big hit. I've been considering putting something like that together. I view the relationship between HoTT and topology as similar to that of functional programming and category theory: you don't need to know the latter to learn the former, but having that extra background can certainly help.

isaac21259 4y ago
I was also considering writing some introductory stuff about HoTT but I don't think it's possible to avoid talking about topology, homotopy theory, and category theory in depth like you can with, say Haskell and category theory. This is because the stuff that makes HoTT so cool cannot be separated from it's mathematical foundations. How would you explain truncated types without going fairly deep into the math? Or the circle type? Sure both of these could be explained as instances of higher inductive types but that explanation is missing a lot.
- Koshkin 4y ago
  As already has been done with category theory, you need to target a specific audience, whether it is programmers, scientists, engineers, or mathematicians, and illustrate the concepts by giving examples from their area of expertise, if possible.
deleted 4y ago
[deleted]