Typed Elixir

Given this module:

    defmodulet TypedTest do
      @moduledoc false

      import String

      @type test_type :: String.t

      @spec simple() :: nil
      def simple(), do: nil

      @spec hello(String.t) :: String.t | Map.t
      def hello(str) when is_binary(str) do
        # @spec ret :: String.t # TODO
        ret = trim(str) <> " world"
        ret
      end

      def fun_no_spec(), do: nil
    end

So far it just tests if specs exist, but it is a start. Verbosely it prints out this at compile-time:

Type Checking: TypedElixirTest.TypedTest

Types:
%{test_type: {{:., [line: 19],
    [{:__aliases__, [counter: 0, line: 19], [:String]}, :t]}, [line: 19], []}}

Specs:
%{{:hello,
   1} => {[{{:., [line: 24],
      [{:__aliases__, [counter: 0, line: 24], [:String]}, :t]}, [line: 24],
     []}],
   {:|, [line: 24],
    [{{:., [line: 24], [{:__aliases__, [counter: 0, line: 24], [:String]}, :t]},
      [line: 24], []},
     {{:., [line: 24], [{:__aliases__, [counter: 0, line: 24], [:Map]}, :t]},
      [line: 24], []}]}}, {:simple, 0} => {[], nil}}

Funs:
%{{:fun_no_spec, 0} => {{:fun_no_spec, [line: 31], []}, [do: nil]},
  {:hello,
   1} => {{:when, [line: 25],
    [{:hello, [line: 25], [{:str, [line: 25], nil}]},
     {:is_binary, [line: 25], [{:str, [line: 25], nil}]}]},
   [do: {:__block__, [line: 12],
     [{:=, [line: 27],
       [{:ret, [line: 27], nil},
        {:<>, [line: 27],
         [{:trim, [line: 27], [{:str, [line: 27], nil}]}, " world"]}]},
      {:ret, [line: 28], nil}]}]},
  {:simple, 0} => {{:simple, [line: 22], []}, [do: nil]}}

Funs missing specs:
[{{:fun_no_spec, 0}, {{:fun_no_spec, [line: 31], []}, [do: nil]}}]

Finished in 0.09 seconds

I wonder if @types can have arguments to make them parameterized… if not I should support that if possible or make a new one… I do not have too much time to work on this but at least it is a start if I confine my code to a certain style…

Typing is hard.

@spec foo :: string
def foo() do
  receive do
    x -> x
  end
end

I don’t know how you’re gonna handle stuff like ^

Types can be parameterized in the following way:

@spec reduce(list, b, (a, b -> b)) :: b when a: any, b: any

That is the challenge, I am curious if it is even possible in Elixir. So unless someone finds a case that is truly beyond difficult or impossible, I may work on it little by little over time.

Oh, and in that case with receive, I’d try to throw some error like (in the optimal case):

Function: Module.foo
Location: file.ex:76
Must return a type of: string
However it returns a type of: any()
Suggestion:  Change or add a case from receive that adds a `when is_binary` condition

Or something like that. I want to be forced to put typing on anything and everything that is ambiguous, that is how you catch a lot of bugs.

Been playing with more, slowly building a DHM inference engine with dependent types (mostly a learning exercise), not working yet but would be nice to get something like this:

defmodule Testing do
  @spec div(number, (d is number if d != 0)) :: number
  def div(x, y), do: x / y
end

Not my preferred syntax but the Elixir parser is unforgiving for what I would prefer (without resorting to strings, blehg). This would define a Testing.div/2 function that accepts any number in its first argument, any number that is not 0 in its second, and can return any number. Basically if you tried to do something like:

case Integer.parse(getInputFromUser()) do
  {i, ""} -> Testing.div(40, i) # Boom
  _ -> return nil
end

Then on the line with the Boom comment it would fail to compile due to unmatched constraint or so, you would have to do something like this instead:

case Int.parse(getInputFromUser()) do
  {i, ""} when i != 0 -> Testing.div(40, i) # Boom
  _ -> return 0
end

Or something that would actively refine the constraints of i to not include 0.

I doubt I will finish this, I think I’d be more apt to write an OCaml backend to Elixir, but this is still a fun very-slow-moving-project. ^.^

EDIT: Yeesh, this was two months later? I really do have about no time… Wish I could get paid to do this. >.>

@spec foo :: received(t) # maybe received(string)?
def foo() do
  receive do
    x -> x
    end
end

How would you go about to writing an OCaml backend to Elixir? That idea seems very interesting, but I don’t see how that would bring static typing to Elixir?

It would be to supplement Elixir. Any module you made in OCaml would output an Elixir module of the same name. You could call into it from normal Elixir code, and you could call normal Elixir code from the OCaml-output-version by the ‘external’ declaration, that is the easy stuff. Everything within a module you’d know would be typed-safe, so as long as the external Elixir modules call it right (and I could always add when checks and assertions and such at public points to verify) then no worry about something stupid within (like me passing a user object in the room field in one of my projects here…). Could slowly convert your code to OCaml or just add it as you go. The more you’d have, the safer the overall project would be.

OCaml itself does not have dependent types (few ML languages do, Haskell does not either), but you can emulate them via typed modules and probably GADT’s… Just playing with the idea of them in my playground here.

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…

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.