Re: [stack] Cat Type Inference

chris glur  wrote:
> > A perhaps trivial question [which also serves to test if my - via
> > gmail - posts get through] is: "is it obvious why one would
> > want to 'infer the types' ?"
>
William Tanksley, Jr wrote:
> Maybe not.
>
> There are many languages that do very little typechecking at compile
> time. They include concatenative languages like Forth, Joy, and
> Postscript; people have worked with them for years. The problem is
> that many errors you can make in them are incredibly hard to narrow
> down and find, but very easy to make. You'd think that with just a
> little tiny bit of static checking you could prevent a huge, annoying
> class of problems from ever becoming an error.
>
> 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.

> 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. 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.  Then [as has been proven over
decades] type checking [not inference] should be done.

==========
Christopher Diggins  wrote:
] This question implies the question "why would one want to statically verify
] the types?". This one is fairly well-known: e.g. documentation, reducing
] defects, and improving performance, so I'll assume that it is already known.
] 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?".
]

] 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'.
How can they 'knows how to write the program they want correctly',
without knowing the types to be used ?
Similarly, smarty-pants multiple error indicating compilers are worse
than the primitive old recursive descent [eg. for pascal] which just
scrolled the source to screen, till it hit the first error.

] Finally, there are scenarios where the type
] is so trivially obvious, writing it is redundant.
]
] 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.

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. With forth too, adding typing is pointless.  Similarly I'm
no convinced
that infereing typing, for a language which was apparently conceived of as
being non-typed is sound ?

As typing provides extra info which can be used for checking, analagously
eg. my Oberon mail-list is better than this one, in that for any post which
I make, I get a confirming echo.

William Tanksley, Jr wrote:
> Your answer was better than mine, but I did have one little tidbit I
> think it worthy: a program that must be type-inferenced must be
> written in a predictable manner: the compiler has to be able to
> figure it out easily. This makes it generally easier to analyze even for
> humans.

Yes, the language must be designed to catch errors by type CHECKING
by the compiler.  Indeed, work load must be removed from the
programmer; eg. by allowing whole constructs, instead of ascii-chars
being 'selected'/entered.  Free up the programmer for more creative
tasks eg. selecting/designing good data names and types.

] Well I agree it would be ideal for programs to be written in a
] predictable manner, I don't believe it to be a theoretical
] prerequisite. I know that other type inferring compilers (e.g.
] Haskell) are quite limited with regards to what they can infer but it
] is mostly a combination of intention (i.e. the designers wanted a
] stricter type systems than I see as being practical) and
] implementation approach.
]
] It'll remain to be seen how sophisticated the Cat inference engine
] turns out to be in practice once the current version is completed. I
] am confident however (based on the performance of the earlier
] prototype) that Cat will be able to handle inferring the type of
] complex edge-case programs with ease. This is due mainly because of
] the simplicity of the type system of Cat compared to other languages.

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

Since I don't know how gmail works [except that it seems to keep
spam out - so far] I'm going to try to just cutNpaste this to gmail
and set 'include quoted text' to No.  Excuse me if I mess up.

Thanks,

== Chris Glur.