20 ms·
Type inference isn't the most important, most languages that employ type inference are moving towards features sets make full inference hard, if not impossible.
by jroesch 10y ago
Type inference isn't the most important, most languages that employ type inference are moving towards features sets make full inference hard, if not impossible. Not to mention you can get pretty good "inference" in dependently typed programming languages just by designing an appropriate higher order unification procedure. I have never met a daily user of these tools that find this to be the bottleneck.
In practice you spend way more time writing proofs in these system then doing anything else. There is evidence that we don't need to limit the expressive power of our logics, just design appropriate automation for the logic. Lean, a new ITT based theorem prover from MSR, has been focused on building automation for type theory. It already has promising results that formal methods techniques can be scaled to type theory (see the website for more information on recent work).
- catnaroek 10y ago> Type inference isn't important, most languages that employ type inference are moving towards features sets make full inference hard, if not impossible. What I'm saying is that I don't like this direction, because type inference is very important to me. > Not to mention you can get pretty good "inference" in dependently typed programming languages just by designing an appropriate higher order unification procedure. Such higher-order unification procedures must always be tailored towards specific use cases, since higher-order unification is in general undecidable. Effectively implementing a different type checking algorithm for every program I write doesn't feel like good use of my time. What I want is a type system that is more honest about how much it can help me: it only promises to enforce properties expressible as first-order statements, but offers much better inference, and the remainder of my proof obligation is hopefully small enough that I can fulfill it manually. > In practice you spend way more time writing proofs in these system then doing anything else. Indeed, and that's what I'd like to fix.
- nickpsecurity 10y agoI like your proposal of first-order, dependent types. Shocked I havent heard of it before now given advantages. I hope someone helps you build it. On related note, what do you think about the Shen LISP approach where Sequent Calculus can be used for advanced typing? Does it have the expressibility and decidability benefits you described? Hadn't seen many specialists talk about it so still an unknown to me. If it does, I figure some default type systems could be created for a specific style of Shen and/or specific libraries. Or something similar done in a ML. http://www.shenlanguage.org/learn-shen/types/types_sequent_calculus.html http://www.shenlanguage.org/learn-shen/types/types_sequent_c...
- catnaroek 10y agoI'm not familiar with Shen, but, if I recall correctly, its type system is Turing-complete, so it's probably more complicated than I'd be comfortable with. IMO, the topmost priority in a type system designed for programmers ought to be automation, not expressiveness. Programmers don't spend their time proving deep theorems. Most of what a programmer does is actually fairly boring, but it ought to be done correctly, reliably and within a reasonable time frame.
- nickpsecurity 10y agoI totally agree. They're not going to use it if we make them work for it. Neither work hard or even lightly. Needs to be no harder than basic annotations but preferably closer to existing, static typing. Let them focus on functions instead of proofs.