patternModerate
Total functional programming language without an static type checker
Viewed 0 times
totalwithoutprogramminglanguagetypefunctionalcheckerstatic
Problem
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?
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?
Solution
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.
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.
Context
StackExchange Computer Science Q#65796, answer score: 10
Revisions (0)
No revisions yet.