<p>The computational implications of homotopy type theory &amp; higher type theory. </p>

<p>Homotopy type theory was invented and developed by a group of computer scientists and mathematicians as a new foundation of mathematics, and as a language to formalize math in, specifically with a view towards algebraic topology (&amp; related fields). However, not much research is done in the computational content of homotopy type theory, i.e. HoTT/HTT as a functional programming language.</p>

<p>Can HoTT be a basis for a practical programming language? What kind of programs do HoTT/HTT enable us to write more easily? What constructs can we add to HoTT/HTT to facilitate programming? There is some research going on in this area, but definitely not enough. </p>

<p>In 2014, Cockx et al. developed <a href="https://jesper.sikanda.be/files/pattern-matching-without-K.pdf" rel="nofollow noreferrer">a way to do dependent pattern matching without using Axiom K</a>, which is inconsistent with univalence. Later, Sozeau added <a href="https://www.irif.fr/~sozeau//research/publications/Equations_for_HoTT-HoTT19-130819.pdf" rel="nofollow noreferrer">HoTT support to Equations</a>, the dependent pattern matching plugin for Coq. This is an example of work done on HoTT as a programming language, i.e. to improve developer friendliness.</p>

<p>Also in 2014, Angiuli et al. showed <a href="https://www.cs.cmu.edu/~cangiuli/papers/hpt-expanded.pdf" rel="nofollow noreferrer">how to do version control using HoTT</a> by developing a Darcs-style "patch theory" in HoTT. This shows that HoTT is a promising tool for some practical programming applications; can we find more appropriate application areas which can benefit from HoTT?</p>

CC BY-SA 4.0
2020-06-21T05:11:16.623Z
Doesn't Cubical Type Theory at least make progress towards this?
Joey Eremondi
CC BY-SA 4.0
2020-03-23T13:57:27.253Z
2020-03-23T13:57:27.253Z
xrq
<p>What are the major areas of functional programming that require more research and development? For example, I know a lot of people are asking for dependent types in Haskell, and someone at my uni is doing a PhD in algebraic effects.</p>

<pl.programming-languages><functional-programming><open-problem><research-practice><haskell>
Areas of research and open problems in functional programming
otah007
# Areas of research and open problems in functional programming

(Asked by: username_0 on 2020-03-22)

What are the major areas of functional programming that require more research and development? For example, I know a lot of people are asking for dependent types in Haskell, and someone at my uni is doing a PhD in algebraic effects.

**Tags:** pl.programming-languages, functional-programming, open-problem, research-practice, haskell


---

## 1 answers

### Answer by username_1 on 2020-03-23. Score: 2

The computational implications of homotopy type theory & higher type theory.

Homotopy type theory was invented and developed by a group of computer scientists and mathematicians as a new foundation of mathematics, and as a language to formalize math in, specifically with a view towards algebraic topology (& related fields). However, not much research is done in the computational content of homotopy type theory, i.e. HoTT/HTT as a functional programming language.

Can HoTT be a basis for a practical programming language? What kind of programs do HoTT/HTT enable us to write more easily? What constructs can we add to HoTT/HTT to facilitate programming? There is some research going on in this area, but definitely not enough.

In 2014, Cockx et al. developed [a way to do dependent pattern matching without using Axiom K](https://jesper.sikanda.be/files/pattern-matching-without-K.pdf), which is inconsistent with univalence. Later, Sozeau added [HoTT support to Equations](https://www.irif.fr/~sozeau//research/publications/Equations_for_HoTT-HoTT19-130819.pdf), the dependent pattern matching plugin for Coq. This is an example of work done on HoTT as a programming language, i.e. to improve developer friendliness.

Also in 2014, Angiuli et al. showed [how to do version control using HoTT](https://www.cs.cmu.edu/~cangiuli/papers/hpt-expanded.pdf) by developing a Darcs-style "patch theory" in HoTT. This shows that HoTT is a promising tool for some practical programming applications; can we find more appropriate application areas which can benefit from HoTT?

> **Comments:**
> **username_2**: Doesn't Cubical Type Theory at least make progress towards this?  

---

