Type.Bitstring (mavis v0.0.6) View Source

Handles bitstrings and binaries in the erlang/elixir type system.

This type has two required parameters that define a semilattice over the number line which are the allowed number of bits in the bitstrings which are members of this type.

  • size minimum size of the bitstring.
  • unit distance between points in the lattice.

Roughly speaking, this corresponds to the process of matching the header of a binary (size), plus a variable-length payload with recurring features of size (unit).

Examples:

  • bitstring/0 is equivalent to %Type.Bitstring{size: 0, unit: 1}. Note that any bitstring type is a subtype of this type.
  • binary/0 is equivalent to %Type.Bitstring{size: 0, unit: 8}.
  • A fixed-size binary is %Type.Bitstring{unit: 0, size: <size>}.
  • The empty binary ("") is %Type.Bitstring{unit: 0, size: 0}.

Key functions:

comparison

binaries are sorted by unit first (with smaller units coming after bigger units, as they are less restrictive), except zero, which is the most restrictive.

iex> Type.compare(%Type.Bitstring{size: 0, unit: 8}, %Type.Bitstring{size: 0, unit: 1})
:lt
iex> Type.compare(%Type.Bitstring{size: 0, unit: 1}, %Type.Bitstring{size: 16, unit: 0})
:gt

for two binaries with the same unit, a binary with a smaller fixed size comes after those with bigger fixed sizes, since bigger fixed sizes are more restrictive.

iex> Type.compare(%Type.Bitstring{size: 0, unit: 8}, %Type.Bitstring{size: 16, unit: 8})
:gt
iex> Type.compare(%Type.Bitstring{size: 16, unit: 8}, %Type.Bitstring{size: 8, unit: 8})
:lt

intersection

Some binaries have no intersection, but Mavis will find obscure intersections.

iex> Type.intersection(%Type.Bitstring{size: 15, unit: 0}, %Type.Bitstring{size: 3, unit: 0})
%Type{name: :none}
iex> Type.intersection(%Type.Bitstring{size: 0, unit: 8}, %Type.Bitstring{size: 16, unit: 4})
%Type.Bitstring{size: 16, unit: 8}
iex> Type.intersection(%Type.Bitstring{size: 15, unit: 1}, %Type.Bitstring{size: 0, unit: 8})
%Type.Bitstring{size: 16, unit: 8}
iex> Type.intersection(%Type.Bitstring{size: 14, unit: 6}, %Type.Bitstring{size: 16, unit: 8})
%Type.Bitstring{size: 32, unit: 24}

union

Most binary pairs won't have nontrivial unions, but Mavis will find some obscure ones.

iex> Type.union(%Type.Bitstring{size: 0, unit: 1}, %Type.Bitstring{size: 15, unit: 8})
%Type.Bitstring{size: 0, unit: 1}
iex> Type.union(%Type.Bitstring{size: 25, unit: 8}, %Type.Bitstring{size: 1, unit: 4})
%Type.Bitstring{size: 1, unit: 4}

subtype?

A bitstring type is a subtype of another if its lattice is covered by the other's.

iex> Type.subtype?(%Type.Bitstring{size: 16, unit: 8}, %Type.Bitstring{size: 4, unit: 4})
true
iex> Type.subtype?(%Type.Bitstring{size: 3, unit: 7}, %Type.Bitstring{size: 12, unit: 6})
false

usable_as

Most bitstrings are at least maybe usable as others, but there are cases where it's impossible.

iex> Type.usable_as(%Type.Bitstring{size: 8, unit: 16}, %Type.Bitstring{size: 4, unit: 4})
:ok
iex> Type.usable_as(%Type.Bitstring{size: 3, unit: 7}, %Type.Bitstring{size: 12, unit: 6})
{:maybe, [%Type.Message{meta: [],
                        type: %Type.Bitstring{size: 3, unit: 7},
                        target: %Type.Bitstring{size: 12, unit: 6}}]}
iex> Type.usable_as(%Type.Bitstring{size: 3, unit: 8}, %Type.Bitstring{size: 16, unit: 8})
{:error, %Type.Message{meta: [],
                       type: %Type.Bitstring{size: 3, unit: 8},
                       target: %Type.Bitstring{size: 16, unit: 8}}}

Link to this section Summary

Link to this section Types

Specs

t() :: %Type.Bitstring{size: non_neg_integer(), unit: 0..256}