On Sat, Jul 12, 2014 at 3:06 PM, Matt Oliveri <[email protected]> wrote:
> On Sat, Jul 12, 2014 at 11:43 AM, Jonathan S. Shapiro <[email protected]> > wrote:> > > Programmer's do change, I agree. But I have never looked for a type > system > > that programmers did not have to understand. > > Sorry, then I guess I don't know why programmers would be bad at > coming up with types for their code. Can you point me to whatever gave > you that idea? > Or you could go do some searches on LtU, where it's been discussed several times. Programmers *can* come up with types. What they can't usually do is come up with *complete* types. There are a lot of ways to go wrong at that. Three common ones: 1. Overspecification: you specify a type because you are thinking about a particular use case at the time you happen to write the function. 2. Using the same parametric type variable in two places that don't actually need to be the same. This is a variant on [1]. 3. Over-qualifying the types with type class annotations. In our experience with BitC v1, it's *especially* hard to get complete mutability annotations right. On the other hand, it isn't clear that you always want those to be complete. > >> > To the mainstream systems programmer, the HM type system is already > well > >> > past the line of Clarke's third law > >> > >> 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. > > > > Matt, how many systems programmers do you interact with on a daily basis? > > I think you're the only one, if you count. And that's only recently. :) > Then you might want to try to maintain a clearer distinction between what you assume/hope is true about those programmers and what is *actually* true. BitC needs to target the latter. > I guess I'm optimistically figuring systems programmers are smart > enough to learn any type system that is evidently useful to them. Right. You are *assuming*. But you are missing something. Systems programmers are pretty smart. They *can* learn just about anything that solves a problem for them. This certainly includes type systems. But the key words are "that solves a problem for them". Before they are going to commit the effort to learn something like this, they need to see a clear benefit to some immediate problem they are facing. Given such a benefit, they will then ask how much investment of time and energy is needed to learn that new thing. Then and only then will they learn the new thing. One reason that inference is so important is that it allows those programmers to approach type system issues incrementally and as needed. When inference is incomplete - which is what makes you need to fiddle the type annotations - it stops being a way to ease in to the language and starts becoming an obstacle in its own right. The question here isn't "what *can* systems people learn?" It's "how can we get them to make the effort?" I'm not interested in giving BitC the perfect type system. I'm interested in giving it a *useful* type system that solves real problems. I agree. And I think that by worrying about superficial things like > type inference, rather than types strong enough to do whatever is > needed.. Needed for *what*? What use case are you concerned with solving that matters in the eyes of the BitC target user base? How do strong types help that use-case, and what is their cost in terms of complexity impact for all the other use cases? > Strong typing _does_ seem to be an > impediment, unless it's so strong it can actually rule out the bugs > that come up in systems, without ruling out too many correct programs. > (And "too many" is a matter of opinion.) > Type systems can't rule out bugs in general. A type system is *always* a trade-off between *perceived* benefit and *perceived* effort. > > >> > 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? > > > > Well, there was this whole discussion thread about dependent type and how > > that wasn't the only way to do type-level computation... > > Well, that was another thread. Why did you bring it up on the topic of > type inference? > Because type-level computation is one of the potential impediments to inference. E.g. it's not obvious that the omission of division over the Nat kind in Habit is actually important to preserving decidability. > > I don't think anybody said that it was distasteful. My concern is that it > > has to be natural enough to feel reasonable and workable to a user who is > > relatively hostile to HM-style typing. > > Sorry, that was a bad choice of wording. I'm curious why you think it > could be unnatural, given its similarity to metaprogramming. > Perhaps because metaprogramming is *also* unnatural. Matt, these are people who *like* twiddling bits and *utterly rely* on having a direct understanding of what is happening on the actual machine. Metaprogramming is an impediment, not a feature. > Extensible type checking gives me the willies too when I examine it in the > > light that current C users are the target for BitC. > > Why? > Because it suffers all of the problems and complexities of extensible proof systems, with about the same degree of benefit. Which is to say, in the eyes of most systems programmers, a lot less than is warranted by those complications. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
