On Fri, Jul 11, 2014 at 2:10 PM, Jonathan S. Shapiro <[email protected]> wrote: > I > think the revealing question to ask is: why are we coming to different > outcomes? > > The answer, I think, is that we have different perceptions about where the > usability constraints are in the language, and which constraints will > inhibit uptake by mainstream programmers.
No. Programmers change. They can learn a type system if it's useful. You have always been the one aiming for some magic middle ground where strong types for low-level programs can be used without understanding them. I'm worried this middle ground doesn't exist. > To the mainstream systems programmer, the HM type system is already well > past the line of Clarke's third law: > > Any sufficiently advanced technology is indistinguishable from magic. If that's true, it's because the mainstream systems programmer doesn't use HM. Not knowing all the ins and outs of a system doesn't automatically make it seem like magic. And it's much more important to understand the meaning of types than to understand how the language can/cannot infer them. > Unless we can make type-level computation feel reasonably natural to people > who don't know much about modern type theory, it will hinder adoption more > than it helps us. Who said anything about type level computation? Are you saying that's the thing that makes type inference hopeless? David recommended something that sounded an awful lot like type level computation recently, as a form of metaprogramming. So what would make it so distasteful to potential users? > This puts us up against Voltaire: > > Don't let the perfect be the enemy of the good. What put us up against Voltaire, and how did it manage that? > When I look at the problems in the field today, it seems a lot more > important to get the large majority of programs moved to safe languages in a > stronger system framework than it is to prove properties about the three > real-world programs we can actually specify. If mainstream adoption is the > goal, proof support may be an impediment. To the extent that types are already specs, type checking is already proving properties of programs. Other than that, I don't know what you think I was suggesting. If the "extensible proof checking" thread gave you the willies, pretend it said "extensible type checking". > When I look at something like Habit, I see uses of type-level computation > and kinding that are new, but they are explicable to a systems programmer, > and the value of them can be readily seen. So far so good. How does Habit fare with type inference? > We know, empirically, that writing higher-order types by hand is > exceptionally hard for even experts to do. You can find an annotation that > works, but it will rarely turn out to be a complete type. I'm not sure what you mean by higher-order type. And I still don't see how some notion of complete type got to be the #1 language requirement. > In BitC, we already have a bunch of things running around in the type > system: > > Parametric types in the style of HM > Kinding in the style of Habit [almost certainly] > General mutability > Regions > Effects > Concurrency labels [if I can figure out how to make them work] > > Of these, only the first one exists in HM so far as any programmer need > notice. Similarly in Coq. Coq is more interesting for the type systems it can define and/or model than for its own type system, which is pretty plain other than dependent types. But with dependent types, it's a small step from easy type checking to impossible type checking. The hard part about type inference in Coq is higher-order unification. If that doesn't help, ignore it. I'm not sure why you brought up Coq here. > So even before we get to the question of dependent > type, we're already looking at something enormously complicated that has to > be rendered in a directly comprehensible way. Personally, I think it likely > that we already have more than we can manage, and we are going to need to > drop things in order to make the language practically approachable. The only > tool we have to mitigate that complexity is inference. That's not the only tool to mitigate the complexity of types. It does seem to be the only one you're comfortable using though. Domain-specific type checking would be the first on my list, and that's what got me interested in extensible type/proof checking. Another is using stronger type systems, so that the various types you need are definable, rather than being built-in. > Frankly, I'm a scared to put dependent typing in BitC. I think it's too > much. On the one hand, I can't point to a single dependently typed language > that I can really wrap my head around. Try imagining your average Linux > programmer working in Idris. On the other hand, I think we have enough new > stuff in other dimensions that is demonstrably important and useful to > systems programs. I don't think that's a fair argument. You haven't tried a dependently typed language, and neither has your average Linux programmer. Te way I see it, if you can understand metaprogramming in Lisp, you can understand dependent types. Really, it's much harder to understand when it _can't_ do something you want than when it can. But that's the case with any complicated type system, and the solution is to make it stronger. The theoretical folks will stick around trying to come up with a proof of why the weak-feeling system is weak, but that's their problem. > It may be the right answer for dependent types to wait another generation of > PL. Could be we can capture a lot with pre/post conditions and assertions. The two are not so different. I didn't think you'd be OK with statically checked assertions either. One of the selling points of dependent types is that it implies that you also have first-order logic. Add monads to a dependent type system, and you have an assertion language, and procedure types with pre/post condition. Strictly first-order assertion languages are a pain. But add anything more, and higher-order unification comes up. > There are a lot of paths here. Success requires that we thread the needle > between expressiveness and usability. I'm concerned that things are already > too complicated for usability, and we're going to need to pick our battles. Alright, but my philosophy is that language design has gotten too monolithic. Usable systems should be built on top of powerful systems. Think of dependent type systems as potentially a microkernel for programming languages, if that analogy isn't too terrible. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
