Can simple algebraic expression be used in type spec? Alternative options?

Questions / Help
,
1

I am fairly new to Erlang and Elixir. Please excuse my ignorance. I have found function specification documentation to be slightly lacking, and the error message I am receiving to be missleading. Given function declaration:

 def my_function(a,n) when a in 1..10 and
                                            n in 1..10 and
                                            a + n <= 10

I believe the type spec could be written similar to:

@spec my_function(a, n) :: {:ok, data} | {:error, error}
        when a: [1..10],
                  n: [1..10],
                  a + n <= 10 #Compilation error invalid syntax before "a" on this line

Can algebraic expressions be used to suggest limits of data values be include in function specifications? The error message seems to indicate the error is before “a”, but when I remove the last line and the last comma in second to last line it works just fine. Is this a valid error message?

The only solution I have come up with is create an additional private function to evaluate the result of a+b is within the valid range. I want the function specification to be exposed in documentation for the user interface for the public api of the library I am working on (I don’t mind adding additional comments, but feel like it should be unnecissary especially if it can be included in specification). Please provide syntax or suggestions on how this is typically solved in elixir (using best practices).

Thanks!

2

You can’t express the limitation that the sum of a and n has to be less than or equal to 10 in a type. You can’t apply functions in types/specs in general.

You can enforce this rule via guards (which you already did) and you should document it. Perhaps even with a dedicated return value?

3 Likes
3

What @Nobbz is saying is correct: The type signatures in Elixir are not expressive enough to write what you want. The closest you can get in Elixir is to document that the output has a certain type (but not limit which variant of that type is used), document it, and constrain it at runtime using a guard.

1 Like
4

Thanks. I didn’t show my dedicated return value for simplicity.

For future readers: I noticed in my example that I specified [1
10] instead of 1
10. Hope this doesn’t confuse anyone.

1 Like
5

For note, the type of typing requested initially is a form of refined or dependent typing, which is very high level (though entirely possible to do), and it is not something dialyzer is capable of, hence specify it at run-time via guards. :slight_smile:

1 Like
6

To make sure nobody gets confused here, I am very certain that @OvermindDL1means: It is theoretically possible to build a system that does dependent-typing , but it is difficult, takes a lot of effort, and combining that with an opt-in type checker like Dialyzer (Elixir’s type checker) is even more so.

2 Likes
7

Indeed, I try to be clear between ‘possible’ and ‘easy’
 ^.^;

8

Although you can’t express this directly at the type level, you can still do it indirectly, by creating an ‘abstract’ type that represents the fact that your function’s guarantees were enforced:

defmodule Test do
  @typedoc """
  Return type of `my_function` success case, indicates that guarantees
  provided by `my_function` are obeyed. Don't create by hand.
  """
  @opaque data :: integer

  @doc "Converts return type of `my_function` into an integer."
  @spec data_int(data) :: integer
  def data_int(n), do: n

  @spec my_function(a :: 1..10, n :: 1..10) :: {:ok, data} | {:error, String.t()}
  def my_function(a, n) when a in 1..10 and n in 1..10 and a + n <= 10, do: {:ok, a + n}
  def my_function(_a, _n), do: {:error, "Error"}
end

defmodule Test2 do
  # Dialyzer warning: the call ... does not have an opaque term of type
  # `data` as first argument
  def result, do: Test.data_int(1)
end

Since we deliberately left out an API-approved way to create terms of type Test.data, except for using Test.my_function, this guarantees that once we do get a Test.data, it must have come from Test.my_function, which means it must obey the guarantees of that function.

Of course, users can just bypass our API and create values of Test.data directly, as in the last example. But at least Dialyzer will at least warn on these cases.

2 Likes