Re: [stack] Re: Concatenative Research

On Feb 3, 2011, at 10:51 PM, William Tanksley, Jr wrote:

> John Cowan <[email protected]> wrote:
> 
>> William Tanksley, Jr scripsit:
>> 
>>> Typing is inherently undecidable. That's one of the fundamental
>>> results of computer science.
>> 
>> Well, sufficiently general typing is undecidable.  Hindley-Milner typing
>> isn't undecidable, it's just a straitjacket.
> 
> My response was to a question asked about the phrase "You could try to
> infer some cases of this (Milner-Mycroft), but the problem is
> undecidable in general." This phrase is the true story of typechecking
> -- you can often find a special case, but usually the first place you
> look winds up not being very useful for actual programming.

On the contrary, Milner-Mycroft works very well in most cases. When it appears to not be terminating, you can "just" bail out and report the issue to the programmer. This may not be particularly pretty, but it's not at all clear to me that it isn't useful. For example, recent work on inferring types in the presence of GADTs depends crucially on Milner-Mycroft and is able to infer types for vastly more expressions than existing, decidable systems.

The reason Milner-Mycroft hasn't been more heavily adopted is that there isn't much of a need for it. Most programmers using languages like Haskell are already comfortable with types and see them as an important form of checked documentation and a very useful means of constraining program behavior. Adding complexity to the language so that programmers can avoid a bit of typing (pun not intended) is usually a bad tradeoff.

- jn