On Sat, Jul 12, 2014 at 11:43 AM, Jonathan S. Shapiro <[email protected]> wrote: > On Fri, Jul 11, 2014 at 3:41 PM, Matt Oliveri <[email protected]> wrote: >> 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. > > 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? >> > 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. :) > Is > your opinion motivated by ample experience and qualified judgment, or do you > think that anybody will learn anything? I guess I'm optimistically figuring systems programmers are smart enough to learn any type system that is evidently useful to them. If I were to be pessimistic, I would figure systems programs will be written in C and assembly for ever and ever. > Systems programmers certainly can learn HM-style type systems, and in some > cases they have. The problem today comes in two parts: (a) the languages > that use HM-style type systems are completely unsuitable to anything a > systems programmer would ever want to do (and therefore are not taken > seriously), and (b) setting that aside, the benefit of strong typing is not > seen by systems programmers. In most cases they view strong typing as an > impediment rather than a tool. > > BitC, just as it is, is an uphill battle. I agree. And I think that by worrying about superficial things like type inference, rather than types strong enough to do whatever is needed, you will end up with a BitC that _isn't_ sufficiently compelling. In other words, 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.) >> > 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? >> 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? > > 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. But I don't care whether you add it. >> > 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? > > The user base puts us up against that. The kind of super-fancy type system > you are angling for just isn't going to be acceptable to current users of C. Well not all of them. But neither will BitC. And C isn't acceptable to us. And all three of them are imperfect. >> 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". > > 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? >> Think of dependent type systems as potentially a microkernel for >> programming languages, if that analogy isn't too terrible. > > Dependent types are way too big to be that microkernel for this cycle of > systems programmers. Hmm, that was potentially confusing. Dependent type system is to microkernel as programmer is to end user. In particular, programmers don't have to see the dependent type system any more than end users have to see the microkernel. Of course systems programmers see the microkernel, but that would be putting them on both sides of the analogy. (But really, I think the world would be a better place if type guys and systems guys got along better. BitC seems to be intentionally steering clear of that possible outcome.) Unless... Are you saying you wouldn't trust a type system built on top of dependent types? _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
