> There is a standardized way - via "ad-hoc" macros. Except they're not really more "ad-hoc" than using classes and traits in Scala is "ad-hoc".
They're not standardized enough to have good common tooling around restricted embedded DSLs. If you use the type system to enforce restrictions around certain areas of Scala code, every Scala tool understands it. IME a lot of lisp programmers end up writing their own tool integration, because there is no standard for that kind of restriction (macros can be arbitrary code; in practice programmers restrict themselves to sensible macros, but in a way that isn't exposed to tooling).
> Idris is not Turing-complete? :o.
In practice there are escape hatches, but it's a total language: your function must come with a proof that it terminates.
> So, you can't express the programs that never terminate, but can you express all the programs that would terminate?
This gets philosophical - would the program "Y {f => x => if(x is a proof of the inconsistency of PA via the Goedel encoding) 0 else f(x+1) } 0" terminate? If you assume consistency of PA then no.
> Point in case, you probably shouldn't ever want to use a language for the specific feature that could express a non-deterministic program.
Well the mu operator or equivalent (informally, the inverse operator) is an extremely useful feature. Many useful programs can't be written strictly primitive recursively (as a trivial example, you can't compute the Ackermann function). I have hope that we can find more restricted versions of mu that let us express all the programs we want to, but that's a decidedly nontrivial problem.
They're not standardized enough to have good common tooling around restricted embedded DSLs. If you use the type system to enforce restrictions around certain areas of Scala code, every Scala tool understands it. IME a lot of lisp programmers end up writing their own tool integration, because there is no standard for that kind of restriction (macros can be arbitrary code; in practice programmers restrict themselves to sensible macros, but in a way that isn't exposed to tooling).
> Idris is not Turing-complete? :o.
In practice there are escape hatches, but it's a total language: your function must come with a proof that it terminates.