Re: [stack] Re: Concatenative Research

On Feb 7, 2011, at 12:02 AM, John Cowan wrote:

> John Nowak scripsit:
> 
>>> (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.
> 
> At the expense of being undecidable!

Not necessarily. Total languages (or languages that otherwise separate non-terminating terms) can have decidable dependent type checking. 

Regardless, undecidability isn't necessarily much of a curse. Provided it works well most of the time and can hint to the programmer how to help it when it fails, an undecidable system type *inference* system may be perfectly acceptable. After all, it's a compile-time issue. I'd rather that than a system that always terminates but may fail to catch legitimate problems. 

Of course, a system without a decidable algorithm for type *checking* is a more severe problem that might cause some irritation. Still, it may work well enough in some instances. People do claim to use C++.

>> Of course. The type system in Typed Scheme is particularly nice given
>> its goals.
> 
> FWIU, Dialyzer and Soft Scheme are close variants of each other.

That may be. I don't know much about Dialyzer. 

Typed Racket (which is what I was thinking of -- not the older Soft Scheme system), however, isn't what I'd usually call a soft system. Programs with type errors are rejected and there's no way that it'll fail to notice a type error. (I'm unsure if you can force it to run the program anyway.) The only way a runtime type error can occur is if a Typed Racket program calls regular untyped Racket code. In this case, contracts are used to do dynamic enforcement. It's quite a clever system, although I'm unsure of its utility outside of pedagogy.

Not telling you anything you don't already know probably. Just encouraging people to give Typed Racket a look.

- jn