How to declare type variables using elixir/dialyixir?

Questions / Help
, , ,
1

NOTE all these questions are related to my use of dialyxir.

Type variables

From the erlang documentation.

Type variables can be used in specifications to specify relations for the input and output arguments of a function. For example, the following specification defines the type of a polymorphic identity function:

-spec id(X) -> X.

This suggests that dialyzer does support type variables and polymorphic types. I cannot see how to declare type variables in Elixir. For example I tried the following code

defmodule TypeVariables do
  @spec id(T) :: T
  def id(x) do
    x
  end

  def run() do
    id(:foo)
  end
end

However this fails because the compiler does not consider T as a variabled. Running dialyxir gives the following output.

lib/test1.ex:7: Function run/0 has no local return
lib/test1.ex:8: The call 'Elixir.TypeVariables':id('foo') breaks the contract ('Elixir.T') -> 'Elixir.T'
1 Like
2

Maybe @spec id(t) :: t. T seems to be considered as an atom :"Elixir.T" by dializer, and not a variable.

3

No that doesn’t work either.

4

Is the error the same?

What about

@spec id(t) :: t when t: any
5

Close… when a: var, or t :wink:

2 Likes
6

Thanks, I know longer get a compiler error but i’m not sure what it’s doing.
I would have expected the following to give an error

defmodule TypeVariables do
  @spec id(t) :: t when t: var
  def id(x) do
    Atom.to_string(x)
  end

  def run() do
    id(:foo)
  end
end

It’s a function taking an atom and returning a string

7

Defining a specification

Type variables with no restriction can also be defined.

That reads as if it is simply unconstrained rather than unified.

In my experience dialyzer wants specifics, e.g.

  @type my_t(t) :: list(t)
  @type my_int_t :: my_t(integer())
  @spec id(t) :: t when t: my_int_t
  @spec id(t) :: t when t: integer()
  @spec id(atom()) :: atom()
  def id(x) do
    x
  end

  @spec run() :: r when r: atom()
  def run() do
    id(:foo)
  end

  @spec run2() :: r when r: integer()
  def run2() do
    id(10)
  end

  @spec run3() :: r when r: my_int_t
  def run3() do
    id([10])
  end
1 Like
8

Does equivalent Erlang code produce the same not-warning?

9

Even in Erlang the error isn’t detected on id/1 - it is only caught if you spec run/0

-spec id(T) -> T.
id(X) ->
    X,
    10.

-spec run() -> atom().
run() ->
    id(foo).

$ dialyzer frequency.erl
  Checking whether the PLT /Users/wheatley/.dialyzer_plt is up-to-date... yes
  Proceeding with analysis...
frequency.erl:250: Function id/1 will never be called
frequency.erl:254: Invalid type specification for function frequency:run/0. The success typing is () -> 10
frequency.erl:255: Function run/0 will never be called
 done in 0m0.14s
done (warnings were emitted)

The Erlang documentation sets the expectation that it should work

Type variables can be used in specifications to specify relations for the input and output arguments of a function.

Edit: I suspect that we are overlooking the “success typing” aspect. Strictly speaking any type is a term() so:

  • @spec id(atom()) :: String.t()
  • satisfies @spec id(t) :: t when t: term()
  • therefore @spec id(t) :: t when t: var is satisfied.
10

Type variables are not unified by dialyzer. In the spec @spec id(t) :: t when t: var, the t as arg and t as return may as well be different type variables entirely.

1 Like
11

Does anyone do this or similar.
Here I am using a spec’d identity function to “cast” a binary to an opaque type which will instruct dialyzer to warn when I try to use it in normal strip operation.

defmodule MyID do
  @opaque t(x) :: x

  @spec id(binary) :: t(binary)
  def id(x) do
    x
  end

  def run do
    id = id("alice")
    String.upcase(id)
  end
end
2 Likes
12

Yep. I LOVE this pattern and use it excessively at times in a large variety of languages. ^.^

1 Like
13

Phantom types… Never used them in elixir, as I usually use types and specs for documentation only.

I rarely use dialyzer itself. Just ran it in a handfull of projects recently to test the new error-message-translator :wink:

14

Those are Named Types. Phantom types are zero-sized types added to a larger type who’s whole purpose is to carry type information (with no associated values) ‘through’ something to be used elsewhere. :slight_smile:

15

A prime simple example in OCaml’ize is:

type EscapedString = EscapedString string

let escape_string str = EscapedString (escape_whatever str)

let to_string (EscapedString str) = str

let render (EscapedString str) = do_render str

And so forth. Essentially it just enforces you to make sure that you run something through, say, a validator before it can be used, in the above case it is to make sure the string is escaped before it is rendered for example.

EDIT: Or for things like tagging integers to keep them distinct for memory arrays for a text-adventure engine emulator so you can’t accidentally use the wrong value in the wrong memory chunk. :slight_smile:

It’s basically Manually Made Refined Typing… ^.^;

16

Yes, Phantom types uses a (ore more) “polymorphic parameter(s)” which are not used in the body of the types. Elixir/Erlang (via Dialyzer) does not support (I think) concept of “variance”, so I suppose that the usage of Phantom Types could be limited.

Btw, I did not known the name “Named Types”. Thanks @OvermindDL1 :wink:

17

It has a few names, but Named Type is popular in the ML world. :slight_smile:

1 Like