Best of luck. Dhall is a current language with totality, but it runs into impossibly high memory requirements as a result. We had CI workers with 16 GB RAM run into out-of-memory issues because of the sheer size of the totally expanded type space (sum types of types which are themselves sum types of types which are themselves sum types etc... Exponential growth is easy).
I appreciate that this is scoped as a hobby project for now, not recommended for production, so like I said, best of luck :)
I'm not sure what you mean with totally expanded type space. But it sounds like Dhall has an issue with unfolding/normalisation.
Totality shouldn't have any special impact on memory usage as far as I know. It just restricts the kind of recursive functions and data types you can write.
If you have a sum type `< a : A | b : B | c : C >.a`, then A, B, and C need to be unfolded. If A itself is of type `< j : J | k : K | l : L >`, and J is also a sum type, etc., then unfolding everything can result in exponential memory usage and exhaust the amount of available memory. Of course there are ridiculously high-memory systems available, but then it's no longer economical.
Best of luck. Dhall is a current language with totality, but it runs into impossibly high memory requirements as a result. We had CI workers with 16 GB RAM run into out-of-memory issues because of the sheer size of the totally expanded type space (sum types of types which are themselves sum types of types which are themselves sum types etc... Exponential growth is easy).
I appreciate that this is scoped as a hobby project for now, not recommended for production, so like I said, best of luck :)