Typed Elixir

[OvermindDL1]

@DianaOlympos

Just so you know, the problem Philip Wadler found when he tried to type erlang :

• message
• pid and process in particular self ()

The other question is… how do you deal with distributed message. You can get a message from a node that do not follow the comtract you assigned. So your type checking is useless in that case…

Already have a test library for that (in OCaml). A quick overview:
Message is just typed as Erlang.t, which is a blackbox unknown erlang type.
Pid is an Erlang.Pid.t, which is also a blackbox erlang type that you know is a pid, you can do something like Erlang.Pid.send somePid someMessage as an example.

The Erlang module would have testing like Erlang.is_int something as well as reifiers like Erlang.reify something that can be used like:

let open Erlang in
match reify something with
| Int i -> doSomethingWithInt i
| Binary b -> doSomethingWithBinary b
| Tuple [ Int i; Float f ] -> doSomethingWithIntAndFloat i f
| _ -> doSomethingAsDefaultCase

Or so forth, and those are only the primitives, can build up better matchers on top of that pretty easily (including dynamically creating arbitrary depth decoders based on types of, say, a receive call). This is pretty easy to do in OCaml and I already have this part done (as I was playing around to see how easy it is). I was planning something similar in this once I figured up a good API but I do think I’d end up having to enforce a new language or so…

@michalmuskala

Another thing that makes typing erlang/elixir really difficult is dynamic loading of modules. The function you’re using may actually not exist yet when you’re writing it, the module may be loaded later. Not to mention hot upgrades that completely mess stuff up.

Eyup, this would only typecheck at compile-time, at runtime it would all still be elixir and you gotta deal with the changes you make, if you do non-atomic hot code swapping and you change your API, then just like in normal erlang be prepared to deal with the consequences (and exceptions, :EXIT’s, etc…). This is less to ensure safety at runtime (erlang does that pretty well already) and more to help ensure that I do not screw up at compile-time by passing things in the wrong order or so, that is my primary use of statically typed languages. Trying to statically type it all at runtime is a fools errand and not something I would even attempt except for occasionally throwing in is_int’s or so in when clauses. I want something to help me code, not ensure safety at runtime (as stated, erlang does that well enough itself via OTP).

@keathley

The papers on dialyzer and success types include a lot of the pitfalls in trying to build an ML type system for Erlang: Research groups – Department of Information Technology – Uppsala University.

Yeah I ran across that long ago, and is one of the reasons I started by thinking of a way to black-box a type like my above Erlang.t type, that way I can always fall back to that and force the user (I.E. me) to do proper tests to reify it and use what they want and handle the cases where they get what they do not want.

@keathley

@OvermindDL1 Have you looked into multi-party session types? From Data Types to Session Types: A Basis for Concurrency and Distribution. That research seems like it could be a promising way forward.

Hmm, that is not something I’ve come across, seems like a decoder of the Erlang.t type could fit within that, it either succeeds or fails given a pattern, which is defined manually if you wish like:

let myDecoder =
  let open Erlang.Decoders in
  Tuple
    [ Literal.Atom `Something
    ; Atom
    ; Validate Int (fun i -> i >= 0 && i < 10)
    ; Binary
    ]

(* Use it like: *)
match Erlang.Decoders.decode myDecoder something with
| Some (_, someAtom, someInt, someBinary) -> doSomething someAtom someInt someBinary
| Error _e -> ()

Which in Elixir would be the same as:

case something do
  (:Something, someAtom, someInt, someBinary) when
    is_atom(someAtom) and
    is_int(someInt) and
    is_binary(someBinary) and
    someInt>=0 and someInt<10 ->
      doSomething(someAtom, someInt, someBinary)
  _ -> nil
end

Thus modules can define decoders (and with mapping and such can transform the data as well during decoding) that can be used elsewhere to parse data. If I made an ocaml backend (I would so love to get the time for that!) then reify could reify a whole tree so you could match on something like this as well:

let rec blah something v in
  let open Erlang in
  match Erlang.reify something with
  | Tuple [ Atom `Something; Int i ] -> i + v
  | List [] -> v
  | List (Int i :: rest) when i<10 -> blah rest (i + v)
  | _ -> v

Which in Elixir would be:

def blah something v do
  case something do
    (:Something, i) when is_int(i) -> i + v
    [] -> v
    [i | rest] when is_int(i) and i<10 -> blah(rest, v + i)
  end
end

In both cases it is just a function that can take a tuple of `(:Something, 42) or a list of integers that it will then sum up each element if the element is less than 10 (OCaml has ‘when’ like in Erlang/Elixir in its pattern matching too).

I’m pretty sure I’ve worked around each usual issue that would happen by having a statically typed language compile to Erlang/Elixir, although it would be slightly more wordy what with things like the Erlang.reify work and such. But for something like receive you can pass in a decoder (that can decode a variety of types, I modeled it on Elm’s JSON Decoders/Encoders) to get back a specific type or could just call it with an identity to get back the next message as an opaque type that you can then match on to unconditionally remove from the mailbox anyway.