Phantom Types

Questions / Help
1

In terms of typespecs, I have a use case where I would like to have a type variable on the left hand side that does not appear on the right hand side. Something like @type t(a) :: pid. However the complier fails with message “type variable a is only used once (is unbound)”. I am wondering how something like the above typespec would be possible and how it would interact with dialyzer.

2

To what end?

Type parameterization is supported

@type dict(key, value) :: [{key, value}]

but clearly the type parameters are provided on the left hand side to complete the type definition on the right hand side. In the case of

@type t(a) :: pid

a doesn’t contribute to the final type so it is assumed that the type specification is malformed.

Dialyzer is a success typer - there is nothing on the level of type classes here.

1 Like
3

If @type t(a) :: pid represents the pid of a process that has a state of type a, I would like to be able to write @spec map(t(term), (term -> any)) :: t(any).

4

FYI: term() is the built-in type that any() is defined as - i.e. they are equivalent Hexdocs: Typespecs.

Now if I understand your intent, you seem to be trying to map over processes in a certain state and apply a function to transform that state resulting in processes of the new state. That is simply something that Dialyzer cannot cover.

  • The pid is simply a dumb reference to a process that may or may not be running.
  • The process state is internal to the process and there is no concept of a “process type”
  • Given a pid a message can be sent to the process. That message may of may not change the internal state of the process but that entirely depends on the internal logic of the process.

Historically adding a static type system to Erlang failed because the typing of the interprocess communication types is non-trivial.

4 Likes
5

One process should not usually care how any other process decides to represent their state. Can you please explain the benefits you think you will get out of this?

1 Like
6

term() is the built-in type that any() is defined as

Yes I was trying to give an example similar to Enum.map where @type element :: any and @spec map(t, (element -> any)) :: list.

Can you please explain the benefits you think you will get out of this?

If you have @type t(a) :: pid and @spec map(t(term), (term -> any)) :: t(any). The map funtion may return not the pid given to it but might spawn a new process with the resulting state. A benefit I would hope to get would be to determine at call site that you can say that given a process with state term and a function from term to any, a process of state any will be returned.

1 Like
7

Dialyzer only covers the typing of the sequential code that is internal to the process. There is no notion of typing of the processes created, messages sent or received. As it is Dialyzer will always assume that you know what you are doing and will only complain when it can prove that you are violating the contract as laid out in the type specification.

2 Likes
8

If dialyzer assumes you know what you are doing is it possible to still consider phantom types. Even if not for processes but a more contrived example of:

@type const(a, b) :: {:const, a}

@spec map(const(any, term), (term -> any))) :: const(any, any)
def map(const) do
  const
end
1 Like
9

Which is why I always say that messages should be black boxed. ^.^

10

See: Emulating phantom types maybe

As Dialyzer doesn’t support the required level of type inference, the suggested workaround was to instead hide explicit details needed by Dialyzer of the type from the potential consumers of the type:

defmodule Demo do
  @opaque plane_air :: {String.t, :flying}
  @opaque plane_ground :: {String.t, :landed}
  @type plane :: plane_air | plane_ground

  @spec new_plane(n) :: p when n: String.t, p: plane_ground
  def new_plane(name), do: {name, :landed}

  @spec land(f) :: l when f: plane_air, l: plane_ground
  def land({name, :flying}), do: {name, :landed}

  @spec take_off(l) :: f when l: plane_ground, f: plane_air
  def take_off({name, :landed}), do: {name, :flying}

end

defmodule Plane do
  @spec flight(p) :: p when p: Demo.plane_ground
  def flight(plane) do
    plane
    |> Demo.take_off()
    |> Demo.land()
  end
end

    done in 0m2.28s
    done (passed successfully)

defmodule Plane do
  @spec flight(p) :: p when p: Demo.plane_ground
  def flight(plane) do
    plane
    |> Demo.land()
    |> Demo.take_off()
  end
end

done in 0m2.23s
lib/plane.ex:18: Invalid type specification for function 'Elixir.Plane':flight/1. The success typing is ('Elixir.Demo':plane_air()) -> 'Elixir.Demo':plane_air()
done (warnings were emitted)

Though if applicable at all, I’d imagine that this would be pretty tedious to maintain.

2 Likes
12

Could you please elaborate your Dialyzer example? I’ve read the hex type specs page at least 10 times and I still could not decode your specs. :107:

13

User-defined types

An opaque type, defined with @opaque is a type where the internal structure of the type will not be visible, but the type is still public.

@opaque plane_air :: {String.t, :flying}

Represents: “airborne aircraft”
Type: Two element tuples where the first element is a string and the second element is a fixed constant: the atom :flying.

The type is public but the internal representation is off-limits by convention. Introspection of the internal data should only be done through module functions directly coupled to the type (functions which will have to be modified when the internal structure of the type changes).

Of course Dialyzer needs to know all the details of the internal structure.

@opaque plane_ground :: {String.t, :landed}

Represents: “grounded aircraft”
Type: Two element tuples where the first element is a string and the second element is a fixed constant: the atom :landed.

@type plane :: plane_air | plane_ground

Represents: “aircraft” (either grounded or airborne)
Type: A union of the plane_air and plane_ground types (i.e. a union type or sum type)

@spec new_plane(n) :: p when n: String.t, p: plane_ground

new_plane takes a string to be used as an identifier and returns “an aircraft on the ground”. This essentially is a constructor that specifically creates a plane_ground value - which by definition is also more generally a plane value.

@spec take_off(l) :: f when l: plane_ground, f: plane_air

take_off maps a plane_ground value to the corresponding plane_air value. So as per spec it can only be applied to plane_ground values and is guaranteed to return a plane_air value.

@spec land(f) :: l when f: plane_air, l: plane_ground

land maps a plane_air value to the corresponding plane_ground value. So as per spec it can only be applied to plane_air values and is guaranteed to return a plane_ground value.

@spec flight(p) :: p when p: Demo.plane_ground

flights spec asserts that it can only be applied to a plane_ground value and is guaranteed to produce a plane_ground value.

This is the example to demonstrate that with this level of detail Dialyzer can actually detect at compile time that take_off and land have been reversed (pattern matching fails at runtime when there is no matching function clause) - because a plane_ground value is being fed to land which expects a plane_air value.

2 Likes