Re: [stack] Re: Concatenative Research

On Feb 3, 2011, at 11:39 AM, John Cowan 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.

What's "sufficiently general" typing here? I use type systems that are decidable and sufficiently general every day. In fact, I often use type systems to do generic programming in ways I can't without a type system (e.g. Haskell's type classes).

> 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.

I'd rather have the HM type. It makes it clear in the type that the values I'm passing will be used only for their boolean properties. I don't think it's fair to say the type is "over-constrained" at all, even if you assume that all values in the language do have some sort of boolean property that can be assigned to them.

> 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).

Firstly, I strongly doubt the type system that Dialyzer attempts to enforce is decidable. There may be a terminating algorithm for what Dialyzer does, but this doesn't mean it is complete with respect to the type system. If the choice is between decidability and completeness, choosing the former isn't much of an accomplishment. (Is there even a particular type system that Dialyzer is attempting to enforce? I'm not sure it makes sense to talk about decidability or completeness at all.)

Secondly, a type system that is restricted to only reporting errors that would occur at runtime is, in my opinion, severely limited. I'd prefer a type system that can easily enforce properties that I can't enforce at runtime (e.g. all the fun things you can do with phantom types and the more advanced variations thereof).

- jn