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?EditIn 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?
Total functional programming language without an static type checker
functional programming