Hi there,
for my master thesis I need to formally define the Elm language. (more on that at a later date) I really want to say that Elm has no run-time errors, that would make things a lot easier. From what I understand Elm uses Recursion without checking its termination and therefore will always run into run-time errors.
I would like to use this topic to get a feeling for how many people actually use recursive functions in their code, why and if it could be avoided/if I can ignore recursive functions in my formal definition.
How often do you use recursive function calls?
Could these recursive function be also written using fold, map, filter?
If so, why do you choose recursive function instead? Is it like in my find example, where I’m just optimizing efficiency or does it have other reasons?
So I’ll start with my experience with recursive functions. The only time I really needed to use them was when I wanted to exit out of the fold-function:
{-| calling `find true` will always run though the entire list
-}
find : (a -> Bool) -> List a -> Maybe a
find condition =
List.filter condition >> List.head
{-| Now the function actually aborts once it has found a valid candidate.
-}
findRec : (a -> Bool) -> List a -> Maybe a
findRec condition list =
case list of
head :: tail ->
if head |> condition then
Just head
else
findRec condition tail
[] ->
Nothing
For function where I my self don’t know when it stops, I usually use the update-function for each iteration:
update : Msg -> Model -> (Model, Cmd Msg)
update msg ({x} as model) =
case msg of
Approximate ->
let
newX = iterate x
in
( {model| x = newX}
, if newX |> isGoodEnough(x) then
Cmd.none
else
Task.perform (always Approximate) (Task.succeed ())
It would be interesting to know how many of you also use the update-function like I do.
Hi there,
for my master thesis I need to formally define the Elm language. (more on that at a later date) I really want to say that Elm has no run-time errors, that would make things a lot easier.
Sorry, I’m not answering your question directly but here I’d like to add that even if you ignore runtime errors caused by recursion, there are still other runtime exceptions. Testing two functions for equality will cause a runtime exception (though hopefully this will become a compile time error in the future) and if your app runs out of memory that will also cause a runtime exception (I doubt this can be prevented).
It seems a curious approach to only recurse through the update function. I think you will find this runs much quicker:
update : Msg -> Model -> (Model, Cmd Msg)
update msg ({x} as model) =
case msg of
Approximate ->
({ model | x = approx x}, Cmd.none)
approx : X -> X
approx x =
let
newX = iterate x
in
if isGoodEnough x newX then
newX
else
approx newX
If approx takes a long time, this can freeze the UI, as no other Cmds will run during the calculation. You can work around that by either splitting the approximation into batches of iterations (say 10, 100, 1000, … it depends on what you are calculating). Another approach is to JSON encode the inputs and outputs to the calculation and pass to another Elm process running in a background thread as a web worker.
My approach intentionally tried to avoid a recursive function call, because it might be that my approximation never stops (in case isGoodEnough(x,newX) == False).
But I’m really not interested in ways how things could be done, I’m interested in knowing:
How often do you use recursive function calls?
Could these recursive function be also written using fold, map, filter?
If so, why do you choose recursive function instead? Is it like in my find example, where I’m just optimizing efficiency or does it have other reasons?
Yes. But they are also build-in functions and one can trust that they will terminate.
For my master-thesis I will need to write a mathematical definition of Elm, meaning I need to describe mathematically the things that the compiler does. For me it’s no problem at all to add fold, map, filter as build-in expressions. (similar to the way while,for,do are used in other languages, even it they could be also written using recursion)
But my mathematical definition should also be able to handle a typical code from the real world. In case that recursive function are but mostly not used (or only for optimization), I could ignore them all together.
Alright. In my experience, recursion is a very common pattern, both in library as well as in application code. Since Elm is turing complete, termination cannot be proven, but in practice, that turns out not to happen very often.
Anecdotally, I have this to share: back in 0.18 days, there was a code-generation issue when dealing with certain recursive patterns (json decoders, parsers, etc) using lazy which could in practice result in runtime errors. This happened enough for me to write an article detailing how this happens and how to prevent it. So, me deduction goes as follows:
people generally write recursive decoders for recursive data structures
people wrote enough such decoders that I got tired answering the same questions
the only way to use recursive data structures, is through recursion
people generally write decoders for use in application code
-> recursive code in applications is fairly common.
I personally wouldn’t feel very comfortable with characterising functions like foldl as language constructs rather than plain old library functions, but that’s sort of besides the point, so let’s hold off on that discussion
Your find is not optimizing efficiency. List.filter will iterate through the entire list, even after the first result is found. A recursive solution could terminate immediately.
we use recursion heavily preferably using functions like folds or find. Also we has our domain specific recursive datastructures which I don’t think is uncommon and for those we implement folds and traversals used in business logic. Also often even views are recursing (trees).
More broadly…
“no runtime exceptions” is marketing claim. Reality is more like “avoiding avoidable runtime exceptions within what is believed to be reasonable tradeoff by authors”. We know that infinite recursion is a problem in any turing complete laguage. You can try to detect some fix point things like Idris does for instance but won’t be able to detect every single one anyway (formaly proven). Function equality was already metioned as another example of runtime exceptions - that’s due to lack of eq “type class”. I also encourage you to check totality checks for recursive functions in Idris as it might be relevant to your work.
Thanks for your response. I believe there will not be a way around both exceptions and recursive functions.
I don’t believe that I will be using fix point theory. I might be confusing this with something else, but I believe my adviser models functions as relations instead.
The thesis is still in its beginning stage. Currently, I am trying to figure out what exactly I want to do, that aspects are the most important and so on. I’ll close this topic for now, and will come back to you once my thesis is in a stage where I can give more detail about what I am actually doing. Thanks, you all, you really helped me a lot.
A lot. I estimate I write a recursive function for every 1500 lines of code I write.
I think most of my recursive functions could be substitued with a fold.
Well, I think recurive functions have a lot more flexibility. Its easier for me to just think through what behavior I want to happen, and what type signature I need my functions need, than it is for me to start with fold : (a -> b -> b) -> b -> List a -> b and try and fit what I am trying to do into that mold.
If I understand it then you probably want to disallow recursion in language and define all recursive functions like folds and find as a language construct. I believe that would me language you’re left with is not turing complete.
You know, with all of this discussion of recursive data structures, I haven’t heard anybody opine about whether or not Lucas_Payr’s “use the update function for all recursion” approach would … at least in principal … work.
Because update can abuse the Task system to call itself indefinitely, and any function can call update and use the Msg to differentiate their needs, then at least in theory I suspect that every recursive call could be transformed into an update call.
But that leaves me wondering about the ultimate relevance of recursion to your thesis if a structurally identical mechanism already exists, Lucas_Payr.
Perhaps, but it does add a considerable overhead. For example, you would not write some recursive data structure this way - it would be inconvenient to break up the iterations into Tasks or Cmds as well as slow.
Theoretically I don’t see why not - you just need to create a continuation to carry on from in the next update. Note also, this means putting continuation functions either in the Model or in the Msg - but perhaps they can also be captured inside a Task.
I think you’re on to something, I didn’t even think about adding the full Elm Architecture to my formal language
The more I think about it, the more I like this idea. As long as I show that every recursive function can somehow be implemented in TEA, I don’t even need to worry if its done with a lambda function, Msg or a Task.
But maybe I’m missing something and I’m actually making things more complicated than it would have been with normal recursion.
