3 ms·

> The other idea being FP languages with hardware-level capabilities. This won't happen until FP implementors work on bridging the gap between typed lambda cal

> The other idea being FP languages with hardware-level capabilities. This won't happen until FP implementors work on bridging the gap between typed lambda calculi (ideal source languages) and the C machine model (ideal target machine). This needs: (0) A limited form of dependent types, tailored to express invariants of data structures, rather than arbitrary mathematical propositions. (1) Substructural types, so that use-once objects can be reclaimed eagerly and deterministically. (2) Designing abstractions so that their implementations have no overhead with respect to what a C programmer could have done manually. But FP people in general don't seem terribly interested in any of these. Instead they write compilers targeting JavaScript.

agentultra 10y ago
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.

agentultra 10y ago

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.