Re: [stack] fundamental type system problems + possible solutions

John Nowak <[email protected]> wrote:
> It seems there's a fundamental problem with typing concatenative
>  languages: Most type systems are not compositional which destroys the
>  simple algebra of concatenative programs.

The literature includes some uses of the word "compositional" for type
systems, but is there a specific meaning you have in mind here? I
think you're talking about a type system which completely preserves
the associative property of concatenative languages (the associative
property guarantees both arbitrary factoring and arbitrary order of
evaluation).

That's a goal I share... Although it's also a goal I want to be able
to work around. There are times when a type system should be able to
force a specific order of evaluation, primarily when the system
deduces the presence of side effects.

Let me add one more thing before I go on: this problem is specific to
type inference, not to type checking in general. If you always
annotate inputs, outputs, and executions, there's no problem.

I need to read up on this; thank you for the references.

>  As I see it, there are three main benefits of static type systems:
>  Automatic and correct documentation, increased safety, and increased
>  efficiency.

I suppose the availability of statically known information to the
programmer counts as "documentation", but sometimes it's more than
that. Consider Ada's type attributes, as in TYPENAME'MAX or
TYPENAME'SIZE. In theory, we could do much better.

I would consider a static type system to be a huge "win" if it helped
programmers. I'm not against static type systems for their own sake,
but I'm strongly for them when they help.

The effect system you proposed would have some interesting ways of helping.

Compare Spark Ada -- which, by the way, might be a useful role model
for a very powerful type system that doesn't actually hurt code that
it can't check (it's entirely optional, contained entirely within
comments of perfectly standard Ada code).
http://en.wikipedia.org/wiki/SPARK_programming_language is perhaps a
good place to start. (I know there are more formal systems out there,
but this one's especially interesting because it's purely optional.)

>  Of these three, I consider documentation to be the most
>  important. After all, there are language implementations without
>  static type systems that perform quite well such as SBCL and LuaJIT.

A good point; JITs tend to have a lot of useful information available
to them. On the other hand, it's easy to design a language that is
very hard to JIT.

>  ultimately, the design of a program and ability
>  of the implementors contributes much more to software reliability than
>  the presence of a type system (compare Haskell/Darcs to C/Perl/Git).

Ability, dedication, and above all else _testing_. Darcs isn't buggy
because its maintainer is unskilled; it's buggy (to the extent that it
IS) because he can't consider all the possible cases, and there aren't
enough people hammering on it (both in coders and in users) to find
them reliably. (I know Darcs is getting a LOT better, by the way; it
was my favorite, although I use Mercurial now.)

Support for testing is important; it would be nice to have support for
it baked into the compiler, and to have support not only for specific
test cases, but also for universal claims (as in Design By Contract,
Haskell's QuickCheck, and formal static annotation-augmented analysis
like SPARK).

>  I would rather have no type system than one which makes simple
>  transformations, and hence macros and much refactoring, impossible.
>  Static type systems seem doomed to being either non-compositional or
>  not suited to producing human-readable documentation.  Therefore, as I
>  see it, there are two possibilities going forward.

Requiring limited annotation could be useful, and has some nice
effects in terms of safety as well -- it's easy to write a function
for which the compiler infers a correct type that is not similar to
the type you'd desired (thus deferring the error message until later,
when it's probably less useful).

>  The other approach would be some way of inferring the equivalences
>  mentioned at the beginning of this email. I guess this would take the
>  form of some kind of abstract interpretation. The goal here would not
>  be to catch all type errors (although some would be catchable), but
>  rather to provide a detailed description of what a function does
>  beyond what an HM-based type system would be capable of yielding. It
>  seems the primary issue here would be giving equivalencies for
>  functions involving recursive data types. For example, if we define
>  some 'each' function that simply places an element from a list on the
>  stack and then calls some function repeatedly until the list is empty,
>  how would we express this?

The uncomputable sky is the limit -- we need a type theory in order to
decide anything here.

>  - John

-Wm