I am frustrated. I feel bad for the future BitC programmer who will write 90% of a strongly-typed program, only to discover that the remaining 10% is inexpressible, at which point they have to go through everything to weaken the types. This is what can happen with a type system that _looks_ strong, due to a long feature list, slick type inference, and clever examples.
This kind of thing is _not_ unavoidable in strongly typed languages. You just need to really be committed to making the type system itself "complete"; the hell with complete inference or complete types for any and every function. (Truly complete types systems are technically impossible, but type systems that incorporate logic are a helluva lot closer.) My fear is you are either going to get terrifically lucky, or you are going to make another strongly-typed toy that provides no practical benefit because no one can hope to predict whether a program will exist with a strong type. I'm sorry for venting my philosophy on your nice list again. Maybe I should disappear for another two years. Good luck engineering the right system for your urgent need, even if it does end up being a crap shoot for anything else. On Sun, Jul 13, 2014 at 12:45 PM, Jonathan S. Shapiro <[email protected]> wrote: > 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: > > Overspecification: you specify a type because you are thinking about a > particular use case at the time you happen to write the function. > Using the same parametric type variable in two places that don't actually > need to be the same. This is a variant on [1]. > 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. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
