Name: Anonymous 2016-01-04 12:29
1. There's many more ways of doing things compared to more simply typed languages so that API design becomes pretty delicate. I can think of four or five feasible types to assign to the simple list head function for instance. With more complex functions this gets even worse and the number of possible types increases. When working in teams you then need to become pretty stringent over matters of style.
2. 40 years after the initial publications on dependent type theory equality is still an absolute disaster. There's a whole panoply of various equalities, equivalences, and similar, that you need to be aware of to get anything serious done. There's definitional equality, propositional equality, heterogeneous equality, bisimulations for stream types, decidable fragments of these, and so on.
3. Definitional equality is antimodular in that it exposes implementation details of functions to clients, making them brittle to implementation details. For example 0 + x reduces to x but x + 0 does not, solely because of how + was implemented.
4. Closely related to the previous point, but proofs in general are extremely brittle to even minor implementation changes, though this is not restricted to dependently typed systems and affects any reasoning tool. Even minor architectural changes therefore become nightmarish tests of resolve.
5. Coq, Agda, and other dependently typed proof assistants suffer from a lack of automation compared to e.g. Isabelle, which being based on classical logic can hook directly into the masses of research carried out on automated reasoning for classical logic fairly easily. Coq still has no usable equivalent of sledgehammer or Isabelle's smooth SMT solver integration, for instance, which makes a big difference when constructing large proofs.
6. When things go wrong, they go wrong badly, and it's often very hard to work out what the problem is unless you have an intimate knowledge of the internals of the type checker, unification machinery, reduction machinery, tactic subsystem, and so on. Further, error messages can become impenetrable very quickly making debugging e.g. a higher order unification problem extremely hard.
7. You need a level of mathematical sophistication to use these systems that most programmers lack. Even worse, even trained mathematicians find adjusting to predicative, constructive reasoning using type theory (i.e. Agda or Idris) a major hurdle. Last summer I had a summer student work with me on a project in Agda who had never programmed before. He was however a very gifted mathematician, yet by far the greatest hurdle he had to overcome when learning Agda was adjusting to constructive reasoning, and adjusting to the idea that proofs are first class objects that can be passed as arguments to and returned from functions. This idea was mind blowing!
8. Repetition everywhere! A vector is a list indexed by its length. As a result, it shares many similar operations (e.g. map, filter, append, and so on) with a plain list datatype yet these operations all need to be reimplemented despite nothing much changing other than the types. For every different list-like indexed type, you also need to reimplement these same operations, and same proofs, over and over again. "Don't Repeat Yourself" is thrown out of the window.
Java's architecture astronauts are well known. Dependently typed languages enable something much worse: type astronauts. A function cannot merely be written that works on some concrete type. It needs to be abstracted and abstracted until it operates on elements of some obscure algebraic structure mentioned once, in passing, in a PhD thesis in 1983. Further, datatypes become decorated with invariants to such an extent it becomes impossible to work out what they actually do. "Keep it simple, Stupid" and "You aren't gonna need it" are both thrown out of the window.
2. 40 years after the initial publications on dependent type theory equality is still an absolute disaster. There's a whole panoply of various equalities, equivalences, and similar, that you need to be aware of to get anything serious done. There's definitional equality, propositional equality, heterogeneous equality, bisimulations for stream types, decidable fragments of these, and so on.
3. Definitional equality is antimodular in that it exposes implementation details of functions to clients, making them brittle to implementation details. For example 0 + x reduces to x but x + 0 does not, solely because of how + was implemented.
4. Closely related to the previous point, but proofs in general are extremely brittle to even minor implementation changes, though this is not restricted to dependently typed systems and affects any reasoning tool. Even minor architectural changes therefore become nightmarish tests of resolve.
5. Coq, Agda, and other dependently typed proof assistants suffer from a lack of automation compared to e.g. Isabelle, which being based on classical logic can hook directly into the masses of research carried out on automated reasoning for classical logic fairly easily. Coq still has no usable equivalent of sledgehammer or Isabelle's smooth SMT solver integration, for instance, which makes a big difference when constructing large proofs.
6. When things go wrong, they go wrong badly, and it's often very hard to work out what the problem is unless you have an intimate knowledge of the internals of the type checker, unification machinery, reduction machinery, tactic subsystem, and so on. Further, error messages can become impenetrable very quickly making debugging e.g. a higher order unification problem extremely hard.
7. You need a level of mathematical sophistication to use these systems that most programmers lack. Even worse, even trained mathematicians find adjusting to predicative, constructive reasoning using type theory (i.e. Agda or Idris) a major hurdle. Last summer I had a summer student work with me on a project in Agda who had never programmed before. He was however a very gifted mathematician, yet by far the greatest hurdle he had to overcome when learning Agda was adjusting to constructive reasoning, and adjusting to the idea that proofs are first class objects that can be passed as arguments to and returned from functions. This idea was mind blowing!
8. Repetition everywhere! A vector is a list indexed by its length. As a result, it shares many similar operations (e.g. map, filter, append, and so on) with a plain list datatype yet these operations all need to be reimplemented despite nothing much changing other than the types. For every different list-like indexed type, you also need to reimplement these same operations, and same proofs, over and over again. "Don't Repeat Yourself" is thrown out of the window.
Java's architecture astronauts are well known. Dependently typed languages enable something much worse: type astronauts. A function cannot merely be written that works on some concrete type. It needs to be abstracted and abstracted until it operates on elements of some obscure algebraic structure mentioned once, in passing, in a PhD thesis in 1983. Further, datatypes become decorated with invariants to such an extent it becomes impossible to work out what they actually do. "Keep it simple, Stupid" and "You aren't gonna need it" are both thrown out of the window.