Re: [stack] Cat Type Inference

Whew, a long email.

chris glur <[email protected]> wrote:
> > The problem then becomes that the programmer has to tell the compiler
> > all about the types of the programs he wants to write, even though
> > "types" are not what programming is supposed to be about.

> OK, the old 'strongly typed vs untypes languages' debate,
> where my prefered language is Oberon - from Wirth's
> strongly typed family.

All type-inferenced languages are strongly staticly typed. If they
weren't, they wouldn't require type inferencing.

And you've misunderstood the debate. Almost no modern languages are
untyped; many of them are dynamically typed (like Python and Joy)
rather than being statically typed (like Oberon).

Most of the currently existing concatenative languages are dynamically
typed; Factor can express some types, and may optionally enforce them
(I don't know). Enchilada is actually untyped, and thus qualifies as a
"rare bird" (it has only one type that can serve as any kind of data).
Forth has types, but doesn't enforce them at all. Cat and strongForth
are the only concatenative languages I know of that consistently
statically enforce types.

(I agree that Oberon is a pretty cool language, by the way.)

> > Type Inferencing makes the compiler do a bit of work to figure out
> > what the programmer meant, assuming that the programmer wanted to
> > write a program that behaves consistently and predictably. As a bonus,
> > not only does the programmer NOT have to explain all the types to the
> > compiler, the programmer also gets an error from the compiler if his
> > program isn't going to behave consistently and predictably.

> I don't like this !
> There are 'problems' where the answers are not yet know, and where
> having the machine infer is appropriate.

If the answers are unknown, having the machine infer them is
_impossible_. Type inference is only possible in the simple cases --
in general it's an NP complete problem.

> Data 'non-typeing' is NOT
> such a case.  When the data is 'created' by the human's mind, the ID
> and type [pair] should be specified.

This is a non-sequitur. We're not talking about untyped data; we're
talking about statically typed data. When the data is created, the
type is always specified; but when a function is written that can
apply to only one type, why should you have to explain which type it
is?

> Then [as has been proven over decades] type checking [not inference]
> should be done.

Why not both?

> ==========
> Christopher Diggins  wrote:
> ] The question that remains then is "why allow the compiler (or better yet,
> ] the editor) infer the types instead of insisting the programmer write them
> ] out?".

Christopher's answer was better than mine; his question (which I've
quoted above) gets right to the issue.

By the way, the ONLY thing type inference replaces is having the
programmer write out the type signatures of functions. It doesn't
replace data types, and doesn't make it possible to write type-unsafe
code; in fact, generally it makes it harder, since you have to write
code that that computer can prove is safe.

> ] If you want static type verification then you will encounter a fair number
> ] of scenarios where expressing the types is non-trivial and the type
> ] signature may even be longer than the function body. Sometimes the type is
> ] not easily deduced by a programmer due to lack of familiarity with the
> ] complexities of type systems, but the programmer still knows how to write
> ] the program they want correctly.

> No, then rather write an ES to explain the 'complexities of type systems'.

What does "ES" mean?

> How can they 'knows how to write the program they want correctly',
> without knowing the types to be used ?

Of course they know the types to be used. But properly specifying the
types can be very difficult and lengthly. You don't have much
experience with strong static typechecking systems, since you're only
used to Oberon, but in a system that actually enforces types you can't
insert an item into a list unless the type of the list allows that
type of item insertion (Oberon allows any object to be inserted into
any list); and functions may only be called in locations where their
types allow such a call. Specifying those things for every place
they're used can become exhausting.

> ] Finally, there are scenarios where the type
> ] is so trivially obvious, writing it is redundant.

This is a surprisingly big win for type inference :-).

> ] As for whether or not it is obvious, that really depends on your experience
> ] with statically typed languages, and an understanding of how the refactoring
> ] capabilities of modern IDEs for C# and Java actually do their magic. The
> ] more type inference you are able to do with a langauge, the more an IDE can
> ] refactor your code for you.

> It seems intuitive that strong-typing, whether by pre-declaration or inference,
> would allow better refactoring by an IDE. Smart IDE's are really what
> I'd like to know more about.

Agreed.

I'd like to hear more about what you're thinking of in the area of
IDEs. I've done a little thinking about them, and of course I use a
moderately smart one at work (Eclipse), but there's plenty more to do.

The only real idea I've had for a smart IDE for a concatenative
language would be an IDE that, when you hovered the cursor on a word,
would draw graphical arrows showing where the word's data came from.

Refactoring support is wonderful, but would depend on the specific
language -- in general, Extract Method is simple in a concatenative
language :-), so presumably other refactorings would be more useful.
(Of course, it's trivial in a flat language -- but since there are no
practical flat languages yet we'll just have to wait.)

> I haven't formalised yet if/why eg. lisp [and presumably joy, which I'm not
> yet familiar with] can't be typed. It sure would ruin the minimalist look
> and feel.

Common Lisp does not have a minimalist look and feel :-). Static
typechecking for Common Lisp has been done -- the language includes
all the type specifiers, so all you have to do is tell the compiler to
look for them.

Joy probably won't be typechecked, but Cat could be said to be Joy's
descendant, and it certainly is.

> With forth too, adding typing is pointless.

I'm not sure why you'd say that, but even if it's true, someone did it
:-). StrongForth is available under the GPL at
http://home.vrweb.de/stephan.becher/forth/. The author originally
created the static typechecking and subtype polymorphism algorithm to
help him manage all the different types of addresses he had to work
with in a particular embedded processor.

There's no reason why the algorithm would only work on Forth; it's
quite general and very simple. The full StrongForth implementation is
fairly complex, but that's because it attempts to imitate ANSI Forth,
which is not designed for strong static typechecking.

> Similarly I'm no convinced
> that infereing typing, for a language which was apparently conceived of as
> being non-typed is sound ?

That's why Cat was designed from the ground up to be type inferenced.
Factor wasn't, but I would expect that it would work well; the author
is not known for sloppiness.

> As typing provides extra info which can be used for checking, analagously

Generally speaking, inference is stricter than explicit specification.
With inference, the program alone must be unambiguous about what it's
doing; with explicit specification, it can be vague.

> OK. PS you know about a similar [infereing types] debate going on
> in Newsgroups: comp.lang.functional ?

Not in the sense of seeing it, but I've been in that newsgroup before,
and I have faith that particular discussion is still alive and well.
It's been running for years now -- perhaps not under the title it has
now, but certainly the same basic discussion, hitting the same basic
points.

There's nothing to debate; a statically typed language with type
inferencing is better that a statically typed language without, UNLESS
the language has to be interpreted faster than the type inferencer
will run. But if that's the case, it's usually more sensible to do
dynamic type checking.

> == Chris Glur.

-Billy