Can we factor out our type systems?

["Peter J. Wasilko" <address@hidden>]

> A simple request, a lot of work. I have been involved with four
> dissertations on this topic (the fourth one is coming along) and
> I can't say what's good. Just think how large ML's front-end is
> compared to the compiler as a whole and that ratio in relation to
> other languages. Take a step back and think about how many people
> AT&T employed on a full time basis to produce this language (and
> what these people failed to deliver). The same is true for our
> soft-typers. Ditto for the Cecil "soft typer" (they use a different
> terminology).

Greetings All,

Would it be feasible to 'factor out' the type system (ie. the analysis
performed on type information explicitly or implicitly present in one's
code) and treat it as orthogonal to the rest of one's language design by
adopting some suitable optional type annotation convention that could be
drawn on by a number of alternative 'type checking plugins'?

In the absence of an active ST module(s) (which would be regarded as a
development environment feature as opposed to a LL component) the
language would be dynamically typed. In this mode, it would use the
optional type annotations to introduce brute force runtime checks and
fall back on exceptions raised by forwarding library calls to
'suspicious' routines that carefully check the types of their arguments
to catch any remaining type errors.

But where static analysis is supported by the development environment
the language would operate in a mix typing mode so it could elide some
runtime checks and invoke faster 'trusting' library code where one or
more of its type checkers could prove that a given application is type
safe.

That way, we could treat running the type checking system(s) of our
choice as a form of partial evaluation to reduce code containing
implicit runtime checks to faster code containing fewer runtime checks.

Then the only serious problem at the language design level would be
deciding how much of the programmer's type intuition needs to be
captured with explicit annotation and what that annotation should look
like.

We could even consider staged type analysis where one ST module could
employ type recovery techniques to deduce obvious implicit types and
augment the code with those additional type annotations for use by the
remaining type checkers.

The key goal is to permit work in the type checking dimension to proceed
independently of the rest of the language design while designing the
type annotations to be as natural to use as possible so the programmer
is more likely to employ them in lieu of raw comments whose
interpretation would be opaque to the type modules.

Warmest Regards,

Peter


_________________________________________________________________

Peter J. Wasilko, Esq.
     J.D., LL.M.               

Executive Director, The Institute for End User Computing, Inc.

Visit us on the web at: http://www.ieuc.org

_________________________________________________________________

It's time to abandon brittle architectures with poorly factored
interfaces, gratuitous complexity, and kludged designs dominated
by sacrifices on the altar of backwards compatibility.

Such artifacts are vulnerable to cyber-attack, weigh down the
economy costing trillions of dollars in lost productivity, and
suffer from an impoverished conceptual model that lacks the
integration and elegance needed to empower end users to
get the most from advanced applications in the future.

_________________________________________________________________
The Institute for End User Computing --- Pursuing Secure, Simple, 
   Supple, & Sophisticated Systems to Unlock Our Human Potential
_________________________________________________________________

* The Institute is incorporated under New York State's
   Not-For-Profit Corporation Law