Is annotating and checking purity of functions feasible?

My idea:

Suppose function f1 calls print_newline, then we annotate it with something like effect_system. Function f2 modifies a state, then we annotate it with something like effect_state.

A function without effect annotations is pure.

How checking works: if a function calls a “system function” (eg print_newline) but is not annotated with effect_system, the type checker will produce an error.

This is exactly what effect systems do. In functional programming languages we can use functional effect systems: Functional Effect systems in Sclala: Build your own ZIO/Cats-Effect/Monix... | Wix Engineering

Note–this is distinct from OCaml’s new effect handlers. OCaml does not have a functional effect system library (as far as I know).

1 Like

This is also what checked exceptions in Java do (for exceptions). It is known to interact poorly with higher order functions (at least in its basic form). It is also know to lead to a problem sometimes referred to as “function coloring”.

That is to say, there are tradeoff associated with this feature, and building a practical, ergonomic language that does this well is an open problem, AFAIK.

EDIT: See for example the paper Accepting blame for safe tunneled exceptions.

1 Like

Just to be the devil’s advocate–the strong statically typed functional programming crowd typically prefer that functions which could perform effects be ‘coloured’ properly i.e. clearly indicate the effects in the types. Since typed effects are also planned for OCaml, I’m not sure how OCaml’s effectful functions would then remain colourless after that.

2 Likes

I suspect you’d want higher order functions to be polymorphic over the color? But I don’t know much of the literature in the area, I’m sure there are people on this forum who have written papers on the matter and could give much more informed answers.

And yet Eio/OCaml 5.0-style effects are celebrated for allowing us to write concurrent programs without Async/Lwt coloring… :slight_smile:

EDIT: I guess the open challenge is to design a system that gives you type safety (“coloring”) without loss of ergonomics.

This can be achieved with standard monadic composition. [EDIT: in the sense that you just lift the functions up into the effectful world, you don’t bother keeping them separated. See e.g. Introduction to ZIO's Control Flow Operators | ZIO )

And yet Eio/OCaml 5.0-style effects are celebrated for allowing us to write concurrent programs without Async/Lwt coloring… :slight_smile:

Definitely not to downplay Eio, but Erlang/Elixir and Go already achieved that years ago :slight_smile: Even Java has now shipped virtual threads.

As someone who spends his day to day coding in ZIO (Scala) which does exactly this (using a monadic style) I thought I’d weigh in.

As @yawaramin writes, this is easily solvable. You essentially have multiple combinators, one pure and one monadic, i.e map: (F[A], A => B): F[B] and flatMap: (F[A], A => F[B]): F[B] where F[_] is your monadic type.

Yes, and I would definitely prefer writing in direct style for this reason. It is nicer, and it does make programs simpler.

What I would definitely not want to give up is the tracking of what side-effects a function uses, such as logging, networking, filesystem access etc. It’s an extremely powerful concept that makes it trivial to understand what the effect of calling a function will be (i.e “this will call the network so I probably need consider my error handling”).

From my understanding Eio can provide some of this (haven’t had the time to play around with it yet). But ideally I’d want the best of both worlds – being able to write code in a direct style without monads, but still allow the type system to track effects for me. I’m hopeful that typed effects will provide an elegant solution to do this in a polymorphic way!

2 Likes

Thanks for expanding on how to handle monads polymorphically, that makes sense.

Concurrency can also be considered an effect (after all, it’s literally implemented using OCaml effects in Eio). Are you saying that you’d like some effects to be tracked, just not concurrency? Or are you saying that you would like concurrency to be tracked, just not with monads but with a more ergonomic language mechanism?

The article seems to achieve something similar to the IO monad in Haskell, no?

My idea is simpler (and likely way less powerful) than using the IO monad — only two annotations: effect_system and effect_state. A function may have neither, one, or both of them. What do you think of this approach? What are the flaws, if any?

It doesn’t compose :slight_smile: There are many other possible effects, like randomness, clock time, non-termination, etc. As Steffen said earlier, it’s also difficult to make functions polymorphic with these kinds of markers.

Nevertheless you can prototype this right now if you want, using OCaml’s alerts feature. These can be used to mark functions and get the compiler to check them. In fact that’s what I did here for exceptions: Add alert `exn` to Stdlib functions which raise exceptions · yawaramin/ocaml@07e69a9 · GitHub

2 Likes

Not sure if that’s useful in any way, I just played around with polymorphic variants to “color” functions:

let require_console_effect x = if x == `Console then () else ();;
let require_counter_effect x = if x == `Counter then () else ();;

let counter = ref 0;;

let hello_world eff =           
  require_console_effect eff;   
  print_endline "Hello World!";;

let increment eff =
  require_counter_effect eff;
  counter := !counter + 1;;  
                
let foo eff =      
  increment eff;   
  hello_world eff;;

Resulting in:

val hello_world : [> `Console ] -> unit = <fun>
val increment : [> `Counter ] -> unit = <fun>
val foo : [> `Console | `Counter ] -> unit = <fun>

I don’t see, however, how this could be used in restricting calling these functions.

In capability-passing style, you explicitly would pass a “console capability” to every function that needs the console and maintain the discipline that this is the only way you can use the console. Then you could potentially pass the set of capabilities as one row-typed OCaml object, instead of as separate arguments.

I suggest making it vary in the other direction:

let foo eff = eff `E1
let bar eff = eff `E1; eff `E2
let baz eff = eff `E1; eff `E3

let test (eff : [`E1|`E2] -> unit) =
  foo eff; (* OK *)
  bar eff; (* OK *)
  baz eff (* Error : [...] The first variant type does not allow tag(s) `E3 *)
2 Likes

I felt like variance was wrong, but didn’t know how to solve that. Thanks!

You can then call a function like this:

test (Fun.const () : [<`E1|`E2|`E9] -> unit);;

which removes the side-effects again (i.e. “handling” the effects).

Although this conversation is a bit stale by now, I just came across this. Since I can’t find your commit upstream in the OCaml standard library, I was wondering what your long term review of the alert is. Although I haven’t tried it in OCaml, having the compiler warn about exceptions and possibly effects is a really nice feature in Swift and Rust and improves the confidence while writing code a lot. Possibly reducing unforeseen runtime errors as well.

1 Like

Chiming in a bit late, but I pretty much love Swift’s way of handling checked exceptions. For me, they strike the perfect balance between providing a sanity check when calling an exception-raising function, without colouring the calling side too much. I think this could be a nice fit for OCamls exceptions and effects as well.

This is how Swift does error-handling.

// Throwing functions need to have the throws keyword
func someThrowingFunction() -> throws {
    let ratings = [1, 2, 3, 2, 2, 1]
    // summarize throws an error, which has to be acknowledged by a leading try.
    // This error "bubbles up" the call stack automatically.
    try summarize(ratings)
}
func someNonThrowingFunction() {
    let ratings = [1, 2, 3, 2, 2, 1]
    // summarize throws an error, which has to be acknowledged by a leading try.
    // A do try block catches the error, like you know it from other languages.
    do {
          try summarize(ratings)
    catch {
        print("Catched an error")
    }
}
func someNonThrowingFunction() {
    let ratings = [1, 2, 3, 2, 2, 1]
    // summarize throws an error, which has to be acknowledged by a leading try.
    // foo is an optional and when summarize throws, foo is empty.
    let foo = try? summarize(ratings)
    guard foo != nil else {
        print("Summarize failed and foo has no value")
    }
}
func someNonThrowingFunction() {
    let ratings = [1, 2, 3, 2, 2, 1]
    // summarize throws an error, which has to be acknowledged by a leading try.
    // If summarize throws, the runtime will panic. Just like uncatched exceptions.
    // This is super discouraged and is basically the same as Rust's panic!().
    let foo = try! summarize(ratings)
    print("The program did not panic and foo has the return value") 
}

As you can see, the caller has to acknowledge the error in each case, but it can easily be propagated to the callee. For Ocaml the easiest thing would be to change the semantics of the try keyword, but that would not be backwards compatible.

This is how it works now:

let rec sum_up acc =
    let l = input_line stdin in
    acc := !acc + int_of_string l;
    sum_up acc 

let run = 
  let r = ref 0 in
  sum_up r
  (* This can maybe? raise an exception or cause an effect *)

let _ =
  try run with
  | End_of_file -> print_endline "EOF encountered"

And this would be with a mandatory try.

let rec sum_up acc =
    let l = input_line stdin in
    acc := !acc + int_of_string l;
    sum_up acc 

let run = 
  let r = ref 0 in
  try sum_up r
  (* I acknowledge this can definitely raise an exception or cause an effect which propagates *)

let _ =
  try run with
  | End_of_file -> print_endline "EOF encountered"

This is however only one possibility I came up with. The alert feature mentioned my @yawaramin can potentially introduce the same effect without breaking backwards compatibility and keeping the semantics I mentioned above. Honestly I am a very irregular OCaml user and consider myself as very unseasoned, as I mostly use Elixir, Swift, Rust, JS and Go to various degrees. I am just learning about effect handlers and this was one pain point I encountered with booth effect handlers and exceptions. Therefore this is a very high level take on the matter