On Thu, Jul 10, 2014 at 4:03 PM, Jonathan S. Shapiro <[email protected]> wrote: > On Wed, Jul 9, 2014 at 9:34 PM, Matt Oliveri <[email protected]> wrote: >> Type inference doesn't have to be intuitive. > > Correct. But type inference failures have to be intuitive. When the > inference engine is unable to solve yshaour problem, you need to be able to > develop a sense of what to do.
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. > If we choose an incomplete inference strategy, what I suspect will happen is > that subprograms which require non-inferrable types will be relegated to > libraries written by clever experts. As long as those idioms are things that > only need to work in corners, that will be fine. If they turn out to be > central to getting effective use out of the language, that's another matter. 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 disagree with you very strongly about the need for principal types. Every > principal typing you can't obtain is a place where genericity fails. What do you mean by genericity failing? Does this happen in dependent type systems, where principal types often don't exist? But actually, first: Was I right that by complete types you meant principal types? _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
