Typed Elixir

Chat & Discussions Discussions
6

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

6 Likes