Elm is Totally Total?

[John_Orford]

To my mind, Elm is a (the?) purveyor of total functions.

I can think of Edge cases where this is not the case, but all in all, I think Elm is total all the way.

Am I correct, or misguided somehow?

[mfeineis]

I’m not aware of any exceptions other than Debug.crash, everything else I can think of uses Maybe or Result, at least the code that has to do with pure Elm… Regexs can blow up at runtime, and I think Date is a notorious candidate but these are inherited from JS

[John_Orford]

I wasn’t actually aware of Regex & Date issues (but they Sound like a work in Progress in any case).

Thanks!

[MarkHamburg]

Anything that checks for equality can die with an exception if passed something that contains functions directly or indirectly.

So, basically, Elm is total except for some cases where JavaScript can fail horribly and some cases where probably no other mainstream language would throw. I program as if it is total and generally try to avoid making equality checks.

Mark

[John_Orford]

Oh, that is another v good pt!

Functional equality is hairy at best of times, I suppose best avoided on every level.

[MarkHamburg]

One way for Elm to address this without a deep implementation change would be to restrict (==) and (/=) to comparable types. This is overly restrictive but safe.

It could also introduce an equals function which would return a Maybe Bool or a special tri-state value.

The combination of those two would keep equality checks available for numerical work and strings and a variety of other “simple” but common cases while providing a safe way for code to use something approximating equality testing in other circumstances.

Mark

[opvasger]

type classes is such an elegant feature when it comes to, for example, making things comparable; I wonder if there is a more restricted and simple approach to them (compared to Haskell) that could yield some of that power for Elm.

[Collin]

It would certainly be fun

[mattpiz]

To my mind, Elm is a (the?) purveyor of total functions.

I’d add Idris to that, which longs for totality, even if you can write partial functions. Edwin Brady blog post on the question: https://edwinb.wordpress.com/2013/02/19/on-partial-functions-in-idris/

[John_Orford]

Yes indeed - I read half of his book, sorely need to return to it v soon!

[luke]

A total programming language is one in which every program can be proven to terminate. There are various runtime issues mentioned throughout this topic, but even after eliminating those and removing Debug.crash Elm would not be a total language because you can write functions that recurse in an unbounded way. Sometimes that will overflow the stack, but other times the compiler will identify tail recursion and the function will execute forever!

The first example that comes to mind of a total language is dhall

[mattpiz]

The first example that comes to mind of a total language is dhall

Oh it looks interesting! thanks for the link

[John_Orford]

Yup the infinite recursion was on my mind also - another good pt.

I have been meaning to writing a little Dhall myself actually, docs are OK, but would love more tutorials…

[John_Orford]

Btw, is there any reason why you would want to write a function in an unbounded recursive way?

TEA gives us a nice recursive method of running a SPA.

But within an Elm app, I could try some recursive computation that would require a_lot or an indefinite amount of finite recursive calls.

But I am never going to aim to kick off an indefinitely running recursive process like a server within my TEA app, right?

I suppose general recursion is a requirement, but just seems so close to being not really necessary…

[brian]

a relational programming system like one of the kanrens would need this. Or, as you mention, a server… which is not in Elm per se but TEA acts an awful lot like a server implemented in this way.

[norpan]

Would it be sufficient to disallow recursion in Elm (but keep the core data structures and functions)? We cannot have infinite lists, so the list functions would terminate.

[MarkHamburg]

Sufficient to what end? This would disallow unbounded recursion but would also result in a significantly less powerful programming language.

Mark

[rupert]

I suppose general recursion is a requirement, but just seems so close to being not really necessary…

It most definitely is a necessity. How else would you write functions that iterate over lists without knowing in advance how long the list will be? Taking Turing completeness out of Elm would be a step too far for me. I don’t think anyone is really serious about this?

[norpan]

Mark, I was replying to Luke’s comment about total languages and dhall

[norpan]

rupert, to iterate over lists you’d use the predefined iteration functions, map, fold etc. It’s interesting to think about having a language like that