On Fri, Jul 11, 2014 at 1:51 PM, Jonathan S. Shapiro <[email protected]> wrote: > On Thu, Jul 10, 2014 at 2:06 PM, Matt Oliveri <[email protected]> wrote: >> Even inference failures don't have to be intuitive. When Coq's >> inference doesn't work, I often don't know or care why, but adding >> more annotations within the top level definition is always the >> solution. > > But I think you are making my point. You seem to be saying that when Coq's > inference fails, you don't really have much insight into why, and you are > reduced to what sounds like a strategy of "make random modifications until > something works". This is bad.
Well it isn't truly random changes, or even pseudo-random. It's more like a combination of conditioned responses and educated guessing. It's pretty rare for this kind of trouble shooting to account for a significant portion of the development time. >> I guess what I don't understand is why people would need to be so >> clever just because the type inferencer doesn't always work. You just >> fiddle with annotations 'till it works. > > I'm an engineer. I find non-principled solutions deeply dissatisfying. My > biases aside, the approach you are proposing limits reuse. If you're an engineer, then you should be able to accept that weird, messy inference can be a pragmatic win if neat inference is impossible. Consider an alternate universe where ML was literally the strongest type system with well-behaved type inference. Anything stronger, and it's either piles of hacks or nothing. Would you then say "Well, I guess BitC isn't a good idea."? If not, then why be limited by whatever the situation is in the real world? _You_ are in danger of giving up something good because it isn't perfect. >> > I disagree with you very strongly about the need for principal types. >> > Every >> > principal typing you can't obtain is a place where genericity fails. >> >> Was I right that by complete types you meant principal types? > > No. Complete type inference means that the inference engine infers the best > (most general) type for every function and expression in the program. ... > Principal types are complete, but they require bottom-up inference. So > principal types are one way to arrive at complete typings, but not the only > way. OK. Luckily that doesn't significantly affect my argument. Dependent type systems don't necessarily have most general types either, in any useful sense. (I mean, singletons are the most specific. They tell you everything you could hope to say about their element.) >> What do you mean by genericity failing? Does this happen in dependent >> type systems, where principal types often don't exist? > > If you don't get the most general type, then there will be generic > structures that you are unable to instantiate over certain types that, if > you had the most general type, would instantiate just fine. > > So yes, this happens in dependent type systems. Keep in mind that any "most general" type in a weaker system will still exist in a stronger system, it just isn't uniquely the most general anymore because other plausible types have been added. So intuitively, what you're saying doesn't seem true. But neither of us are being very precise. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
