I love Elm’s guarantee that “if it compiles, it usually works”, especially in the promise that it doesn’t create any runtime errors. There are a few known exceptions, such as:
An HTTP call getting blocked by invalid CORS headers
Comparing functions using the == operator
Running into the browser’s max recursion depth
The browser running out of memory
I would like to erase all runtime exceptions as much as possible - and I’ve looked into doing that with a back-end Elm-like language. Problem 1 doesn’t exist for the back-end, and a re-design of the compiler could solve problem 2. However, problem 3 and 4 are memory issues, and I cannot find a programming language that doesn’t break when running out of memory!
Creating a back-end solution
I think that a back-end version of Elm could avoid runtime errors as a result of running out of memory. I’ve written a design in a blog post and I’d love to hear your opinions on it. In short, functions could look like this:
add : Int -> Int => Int
add x y =
x + y
|> Mem.withDefault 0
Here, the => indicates that the function would still return an integer, even if there is no memory available. So even if the stack is full and would overflow into the heap, it can still function.
Feedback
Given that even C has unrecoverable stack overflows, I’m trying to build a quick & dirt Elm-like programming language that aims to never crash by tracking all its data on the heap. I see great value in a back-end language that offers recovery from memory failures. Refer to my blog post for more details on the concept language.
Is this experiment a great idea? Is it a lost cause? Is there a programming language that does anything similar, or is there an obvious reason why no-one else has attempted memory-aware functional programming before?
Is this experiment a great idea? Is it a lost cause?
If you’re enjoying your time then it’s a great idea!
Is there a programming language that does anything similar, or is there an obvious reason why no-one else has attempted memory-aware functional programming before?
I feel like I’ve see something about memory-aware PLs before, in the style of a C like language, but it’s escaping me right now.
It may be worth looking into linear or dependent types, or PLs like Agda, Idris, and Ada. I feel like Zig could be an ok reference as it can do some stuff at compile time (built into the syntax of the language) and has robust memory options.
Likely also be worth asking/searching in /r/ProgrammingLanguages as there’s a decent chance someone has asked similar questions before.
@Bram Do you have a real world example of how this => would look (I saw the fibonacci example on your blog)? My guess is that you’d end up with an enourmous amount of Result types that would be a pain to work with and probably introduce bugs of their own.
That being said, if the goal is increased memory safety and you’re open to other ideas, I do have a suggestion. What if instead of adding a new language feature, you exploit the fact that Elm is a pure functional language by having a backend platform that looks something like this
main =
BackendPlatform.worker
{ init = init
, requestHandler = \msg model -> update msg model
, runWhenMemoryRunsOut = \model -> functionThatRemovesUnimportantStuffFromModel model
}
Then when the requestHandler throws an OutOfMemory exception, the platform can run the runWhenMemoryRunsOut function on the old model, and then call the requestHandler function again with the new model and the msg that didn’t get handled. Since Elm is a pure functional language, there’s no risk in running requestHandler on the same msg twice.
An HTTP call getting blocked by invalid CORS headers
This isn’t an exception? You should get Err NetworkError back without the app crashing.
Could be great on memory restricted devices such as micro-controllers or other embedded applications. A functional compiler that can provide guarantees about never exceeding a limited amount of RAM.
Yes, great question! That’s exactly a horror scenario I want to avoid.
My current design is that the new memory-aware relation => is an optional feature, and behaves like a runtime exception that crawls up to the nearest function that catches a memory problem. If the program at the top then requires a record that looks something like this:
{ init : flags => Model
, update : msg -> Model => Model
, subscriptions : Model => Sub msg
}
Then the compiler would only require you to handle the memory error SOMEWHERE in your code near the top. So the compiler takes the responsibility of ensuring everything is memory safe, without requiring you to write EVERY function memory safe.
Alternative design
Since this is relatively unorthodox for how Elm likes to handle exceptions, I’ve also considered that the compiler introduces a Mem.Safe a type which would still fit the memory safety part.
So the program would ask for something like
{ init : flags -> Mem.Safe Model
, update : msg -> Model -> Mem.Safe Model
, subscriptions : Model -> Mem.Safe (Sub msg)
}
Although that WOULD suggest that you’ll need a library with functions like Mem.map, Mem.andThen, Mem.toMaybe and other types similar to Result. This aligns with Elm’s design more, but might bring us back to the enormous number of Result types in our code.
Running out of memory is very tricky. If you’re out of memory, then you might not be able to run the function that removes some memory - because it takes memory to run another function.
Instead, it is much more effective if your runtime immediately knows what to remove from memory once it runs out of memory.
foo : Int -> Int => Int
foo x y z =
x
|> (+) y
|> (*) z
|> Mem.withDefault 0
If the foo function is unable to call the (+) function because of a stack overflow error, then it immediately knows to return the (pre-cached) value 0 and to delete the function. It doesn’t need to allocate any memory or call another function to safely finish the function.
I’m still wrapping my head around situations like that, and I think that that can be a different scenario. For example:
-- Example 1
foo : Foo => Foo -> Foo
foo x =
(\y -> bar x y )
|> Mem.withDefault identity
-- Example 2
foo : Foo -> Foo => Foo
foo x y =
bar x y
|> Mem.withDefault defaultFoo
I think these two would work differently. One is guaranteed to return a Foo -> Foo function regardless of memory, while the other is guaranteed to return a Foo after two valid Foo types have been inserted.
I recall that the Koka language tracks divergence in its effect system, though there are limits to what can be marked as non-divergent, like here. It looks like they are also exploring a pretty interesting technique for memory management as well.
I recall that Lucid Synchrone was able to figure out the maximum memory requirements of each program at compile time, though they were focusing on “real-time systems” like emergency braking systems, plane autopilots, electronic stopwatches, etc.
Systems like Coq require that all programs terminate, so if you have recursion, you must prove that the recursion terminates. This can be done by showing that a certain ADT gets smaller on each step of the recursion. I personally found it very difficult to construct these proofs when I was trying to write more complex programs, but my point is that it is possible to differentiate between “recursion that will definitely terminate” and “recursion that may not terminate”. This is called the halting problem in the general case though, so it’s not something that can just be automated and no one ever has to think about it. You must construct your programs very carefully such that termination can be proved.
Then the compiler would only require you to handle the memory error SOMEWHERE in your code near the top. So the compiler takes the responsibility of ensuring everything is memory safe, without requiring you to write EVERY function memory safe.
A little tangential to the discussion but this is kind of analogous to what the ExceptT monad transformers aim to help you with in languages like Haskell and PureScript. Would it be worth looking into them for inspiration to avoid the other concern mentioned here about ending up with too many Result types (a problem Rust has, IMO).
Thanks, everyone. I’ve written a second blog post which summarizes some of my findings.
Apparently, this is a relatively new concept! The Perceus paper that Koka points to is from 2020, and another paper on immutable reference counting that I found, dates back from 2019. I think Elm’s compiler would be able to take a step further, though, combining Rust’s lifetime tracker with how Neut handles memory.
I think that this section explains the benefit best: if you want to update a Tree Int to a new Tree Int type, it seems much better to do an in-place operation than to recreate the entire structure and dump the older version. And the compiler should be able to realize this and make it an in-place operation. (Although, to be honest, I’m not sure how difficult that will be.)
Lastly, I’ve created a first design of a compiled version! It should function reliably, regardless of how much memory you feed it. With this design, I think I can start writing an AST that will transpile to a C program like this one.
If you have more resources to share, I’d love to hear them! This has been an educational journey so far.
I’ve written a