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.

1 Like

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).