3
$\begingroup$

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.

$\endgroup$
1
$\begingroup$

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, which is inconsistent with univalence. Later, Sozeau added HoTT support to Equations, 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 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?

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ Doesn't Cubical Type Theory at least make progress towards this? $\endgroup$ – jmite Jun 21 at 5:11

Not the answer you're looking for? Browse other questions tagged or ask your own question.