It’s more the other way around. The static type system makes the IO monad and those checks possible.

Elixir doesn’t yet have a robust static type system so you cannot statically prove properties of your program. There’s work on adding types and other forms of static analysis to Elixir but today you’ll need to look at other BEAM languages such as Gleam or Purerl.

It looks like Witchcraft focuses on the polymorphism aspect of type classes rather than the static verification.

The IO monad only tracks side effects and ordering, so it’s not enough to get that property. You need the more general tool of a robust static type system.

For specifically side effects I think algebraic effects would fit well with Elixir as they are easier to use, have less runtime cost, and map well only existing Elixir code. They don’t do ordering but in a strictly evaluated language that is unimportant.

Macros make implementing a type system more challenging but it’s not a show-stopper, it is still possible.

If you are happy with the level of analysis that Dialyzer offers you then you can implement an IO monad in Elixir without too much pain!

defmodule IOMonad do
  @opaque io(a) :: %__MODULE__{__effect__: (-> a)}
  defstruct :__effect__

  @spec pure((-> a)) :: io(a)
  def pure(effect) do
    %__MODULE__{__effect__: effect}
  end

  @spec map(io(a), (a -> b)) :: io(b)
  def map(io, transform) do
    pure(fn -> transform.(io.__effect__.()))
  end

  @spec bind(io(a), (a -> io(b))) :: io(b)
  def bind(io, transform) do
    pure(fn ->
      transform.(io.__effect__.()).__effect__.()
    end)
  end
end

The same rules apply as in Haskell:

1. You must wrap all side effecting code in the IO monad rather than performing it immediately.
2. You must never access __effect__ anywhere in your code, you must always use map and bind.

This unfortunately will be very challenging in Elixir. Unlike in Haskell there is little to verify you are using it correctly, and you’ll have to fork or wrap any libraries you use that have side effects, including the standard library.

Algebraic effects could be used with existing Elixir code without modification but require a more powerful static analysis tool than exists for Elixir today.

edit

As a bonus here’s the same thing in Gleam. The nice thing about this is that the compiler will check that you use it correctly!

pub opaque type Io(a) {
  Io(effect: fn() -> a)
}

pub fn pure(effect) {
  Io(effect)
}

pub fn map(io: Io(a), transform: fn(a) -> b) -> Io(b) {
  Io(fn() { transform(io.effect()) })
}

pub fn bind(io: Io(a), transform: fn(a) -> Io(b)) -> Io(b) {
  Io(fn() { transform(io.effect()).effect() })
}

but I thought…

Gradient/Gradualizer would do much better! I’m not sure how complete it is but I’m quite excited for it. Looks great.

It’s more of a type checker or compiler feature than a library. The nice thing about it is that for just inferring and restricting effects you don’t need to change the code at all.

Here’s some normal Elixir code

defmodule Main do
  def main do
    text = IO.gets("What's your name?")
    IO.puts("Hello, " <> name)
  end
end

Here it is with an IO monad

defmodule Main do
  def main do
    IOMonad.pure(fn -> IO.gets("What's your name?") end)
    |> IOMonad.map(fn name -> IO.puts("Hello " <> name) end)
    |> IOMonad.unsafe_perform_io()
  end
end

And here it is with algebraic effects.

defmodule Main do
  def main do
    text = IO.gets("What's your name?")
    IO.puts("Hello, " <> name)
  end
end

There’s no changes from the normal code to use IO with this system! All you need to do is annotate functions with any effects they emit.

defmodule MyApp do
  @effects [:console]
  def print_string(string) do
    IO.puts(string)
  end

  @effects [:send_message, :receive_message]
  def run do
    send(self(), "Hello")
    receive do
      x -> x
    end
  end
end

Any functions that call these functions will automatically be detected as also having these effects.

They will be approximately the same. A gradual type system with full annotations should be as sound as Gleam’s type system (with or without annotations) though it comes down to the details of Gradualizer specifically.

Thank you for your support

The Gleam discord server is often a good place to chat about Gleam or to ask questions. It is quite active these days