Lambda the Ultimate

Tom integrates pattern matching and rule based programming facilities into Java. It is particularly well-suited for programming various transformations on trees/terms and XML based documents.

Tom adds new constructs to Java that enable information retrieval and transformation (via conditional rules) in lists and trees. Traversals of trees and transformations are based on a strong theoretical background. Tom compiler is mature enough to be used for large scale developments and applications, and integrating Tom in any existing application is straightforward, as Tom produces Java source code.

Some applications developed in Tom (both in academia and industry):
- requests transformations (ex: XQuery requests' optimizations )
- the Tom compiler itself
- languages semantics, interpreters and program transformation tools
- a generator of canonical abstract syntax trees (Gom)
- a Just In Time strategy compiler using dynamic Java bytecode transformation
- a proof assistant for supernatural deduction
- a compilation algorithm for anti-pattern matching and disunification

A guided tour of Tom can be found here, and the release notes here.

Tom is available, in open source (GPL/BSD License), from the web page: http://tom.loria.fr/

Hello everybody, this is my first post, so please be gentle... (actually i was passive around here for years, and find LtU a great source of inspiration and wisdom).

I'm not at all into dynamic typing, i find static type-checking superior in any way. However, recently i just had the thourght:

"If all I want to write is a single side-effect-free, IO-free, terminating function F(x), with well defined argument- and return-types. And further, if I am able to come up with an x which trigger all branches (selections and pattern matches) of F, then i can get static (compile time) typing of F in a dynamically strong typed language."

Suppose i write F in the dynamically strong typed language, which does the following:

Immediatly after each compile of F, evaluate F(x), (yes, please). If it does not crash (or loop forever) F is type-safe, else report an error. The idea is that type-checking F is no harder than evaluating it on a sufficiently large test set argument.

Is this sound? If yes, what about the next step:

If it shows be the evaluation that F(x) has a strong typing, would it be possible to record all types of all expressions and create G, equivalent to F decorated with type annotations?

I do realize i'm asking for (usually turing-complete) type-infernce for free...