Re: [stack] Re: Concatenative Research

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.

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

The H-M type allows the function to accept only "true" and "false",
whereas a dynamically typed system will accept much more.  In that sense
H-M is over-constrained: it doesn't permit a vast number of calls to this
procedure that will actually (in a dynamically typed language) succeed.
H-M insists that you only pass argument that *cannot* cause a run-time
error (though, BTW, nobody has types "integer" and "nonzero integer" and
requires that the denominator of a division belongs to the latter type).

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

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.

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

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.

-- 
They do not preach                              John Cowan
  that their God will rouse them                [email protected]
    A little before the nuts work loose.        http://www.ccil.org/~cowan
They do not teach
  that His Pity allows them                         --Rudyard Kipling,
    to drop their job when they damn-well choose.   "The Sons of Martha"