Total functional programming language without an static type checker

Question

All papers with the subject of total functional programming make use of some kind of static type checking to ensure totality. This make sense considering hoy easily is to make a language Turing-complete. The question is: Is there any untyped/dynamically-typed formalism that ensures total functions?

Edit

In other words, there exist any formalism that only allows to construct total functions, with the impossibility of construction of partial functions, so there is no need of a filtering stage like a type checker or a termination analysis?

Answer 1

The question is, how do you eliminate terms that run forever:

In particular, things like $(\lambda x \ldotp x\ x)(\lambda x \ldotp x\ x)$ and the Y combinator must NOT be in your language, since they can be used to construct computations that do not halt.

Static typing in things like System F eliminates these: they start with a full lambda calculus, and then filter out ill-typed terms.

But, do do this in an untyped setting, you need to eliminate these terms by construction. They cannot be expressible in your language.

I can think of some silly ways to do this, like the language of imperative programs with no functions or and only loops over lists. But in general, as soon as you have higher order functions, these problematic constructs are constructible. So while I won't say that it's impossible, it's probably very difficult to do in a way that makes much sense.

It's possible for you to statically filter out these things with something that isn't a type system, with termination checkers, but these will always throw false positives, and while they aren't static typing, they are still very much a static filter on your programs.

Note that, depending on what you consider "dynamically typed," you could eliminate programs like this by keeping track of types using inference, but only throwing errors at runtime. Thus something like the Y combinator is still rejected, just later. This is dynamically typed, but probably not what you are looking for.

Answer 2

Absolutely! There's even an existing implementation! I wrote this loop.py program in python:

while True:
    print "Hello world!"
    print "20 GOTO 10"

And ran it like this: timeout 10 python loop.py. Tadaa!

More to the point, what do you consider to be "static analysis"? A programing language that only contains for-loops will always terminate. Is parsing it "static analysis"? How about a compiler that compiles a C program and runs it for 10 seconds, and returns the compiled code only if the program terminates?

In theoretical CS, we always have the option of running a program a few steps at "compile time" to see what happens. At run-time, you always have the option of making an early exit out of a program if it's taking too long. Indeed, that is what the vast majority of programs do, instead of "termination checking". There's even such a feature for javascript scripts in the browser (or the infamous "program not responding" messages).