Re: [stack] Re: Concatenative Research

On Feb 6, 2011, at 11:40 PM, John Cowan wrote:

> John Nowak scripsit:
> 
>> What's "sufficiently general" typing here? 
> 
> What I meant was, if you generalize your type system enough, it eventually
> becomes Turing-complete (by the Curry-Howard correspondence), hence
> undecidable.  I think this is uncontroversial.  That's presumably more
> general than you actually want.

Right, I agree. I may have misread. I thought you were claiming that a system that is sufficient for "real work" will be undecidable or something along those lines.

> (though, BTW, nobody has types "integer" and "nonzero integer" and
> requires that the denominator of a division belongs to the latter type).

Well, languages with dependent types can and do.

> It's complete in the sense that it rejects all expressions that it can
> prove to be invariably unsound (that is, unsound no matter what happens
> at run time).  It's not complete in the sense that it fails to reject
> all expressions that are sometimes unsound.
> 
> I don't know any meaning of "decidable" except "guaranteed to terminate",
> which it is.

Well, as I said, it does terminate. But an algorithm that is decidable yet incomplete and unsound isn't much of an accomplishment! Any algorithm can be made decidable by just bailing out after awhile. I wouldn't, therefore, claim this is a feature of Dialyzer. Any practical system will do this. When people talk about decidabaility, they usually are asking if something is guaranteed to terminate while implementing the complete rules of the system. I don't believe Dialyzer does (or can) do this.

> Well, I have no problem with you having your preferences.  But the
> importance of success typing is that it shows that type systems can be
> useful even if they are not in the H-M (or M-W) family.

Of course. The type system in Typed Scheme is particularly nice given its goals.

- jn