Re: [stack] Re: Concatenative Research

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.

Consider the function x defined by the following cases:

x true true = true;
x _ false = false;
x false _ = false;

where _ is "don't care".  Under H-M typing, this is an AND function, and
its type is bool -> bool -> bool.  But the actual function allows a lot
more than that!  For example, x foo false is defined, and so is x false
bar, though x foo bar is not defined.  So the H-M type overconstrains
the function.

Success typing, as used in Erlang's Dialyzer, comes up with the much
more reasonable type any -> any -> bool, where any is a union of all
the available types.  It's quite decidable, and has the advantage that
it never reports a type error unless there is a definite clash (like
passing the wrong type to a built-in).

-- 
They tried to pierce your heart                 John Cowan
with a Morgul-knife that remains in the         http://www.ccil.org/~cowan
wound.  If they had succeeded, you would
become a wraith under the domination of the Dark Lord.         --Gandalf