4 ms·

With my limited experience in Agda I'm really excited about dependent types. I've been under the impression that there is some research in this area...

catnaroek 10y ago
A language whose type level allows you to express arbitrary mathematical propositions can't possibly have as good inference as ML and Haskell have, because higher-order unification is known to be undecidable. Agda and Idris require manual type annotations for all let-bound identifiers. Coq requires all dependent pattern-matching blocks to be type-annotated. This is a real chore, and dependent types will never become mainstream unless their usability improves significantly. What I have in mind is one way to hopefully achieve that “significant usability improvement”: (0) Have dependent types, but restrict them to be first-order. This is good enough for programming purposes: invariants of data structures can almost always be expressed as first-order formulas. (1) Use known and proven type inference technology: generate a system of type-level equations, and solve them via first-order unification, which is known to be decidable and tractable in practice. But I don't see anyone in the FP community exploring this possibility.
- nickpsecurity 10y ago
  I just got a bunch of papers on first-order verification, implementation, compilers, and so on as the simplicity & tractability part peaked my interest. I'm keeping them in case I run into some students or hobbyists that want to try that on top of some "verify the verifier" kind of issues. Then I see these suggestions... "(0) Have dependent types, but restrict them to be first-order. This is good enough for programming purposes: invariants of data structures can almost always be expressed as first-order formulas. (1) Use known and proven type inference technology: generate a system of type-level equations, and solve them via first-order unification, which is known to be decidable and tractable in practice." I'll add those to the list given that sounds worth a good try. Especially if combined with automated approaches to generating & solving for common attributes like in SPARK and AutoCorres. Maybe something will come of it.

catnaroek 10y ago

A language whose type level allows you to express arbitrary mathematical propositions can't possibly have as good inference as ML and Haskell have, because higher-order unification is known to be undecidable. Agda and Idris require manual type annotations for all let-bound identifiers. Coq requires all dependent pattern-matching blocks to be type-annotated. This is a real chore, and dependent types will never become mainstream unless their usability improves significantly. What I have in mind is one way to hopefully achieve that “significant usability improvement”: (0) Have dependent types, but restrict them to be first-order. This is good enough for programming purposes: invariants of data structures can almost always be expressed as first-order formulas. (1) Use known and proven type inference technology: generate a system of type-level equations, and solve them via first-order unification, which is known to be decidable and tractable in practice. But I don't see anyone in the FP community exploring this possibility.

nickpsecurity 10y ago
I just got a bunch of papers on first-order verification, implementation, compilers, and so on as the simplicity & tractability part peaked my interest. I'm keeping them in case I run into some students or hobbyists that want to try that on top of some "verify the verifier" kind of issues. Then I see these suggestions... "(0) Have dependent types, but restrict them to be first-order. This is good enough for programming purposes: invariants of data structures can almost always be expressed as first-order formulas. (1) Use known and proven type inference technology: generate a system of type-level equations, and solve them via first-order unification, which is known to be decidable and tractable in practice." I'll add those to the list given that sounds worth a good try. Especially if combined with automated approaches to generating & solving for common attributes like in SPARK and AutoCorres. Maybe something will come of it.