Elixir Type System Examples

elixir_type_system_examples.ex

# Based on framework semantic subtyping: https://www.irif.fr/~gc/papers/icalp-ppdp05.pdf
# CDude implements this framework: https://www.cduce.org/ 

# Why?
## 1. aid documentation
## 2. ensure correct contracts

# Code examples

$ integer() -> integer()
def negate(x) when is_integer(x), do: -x

$ (integer(), integer()) -> integer()
def subtract(a, b) when is_integer(a) and is_integer(b) do
  a + negate(b)
end

# Set-Theoric Types (unions, intersections and negations)

# Can you find a problem here?
$ (integer() or boolean()) -> (integer() or boolean())
def negate(x) when is_integer(x), do: -x
def negate(x) when is_boolean(x), do: not x

$ (integer() -> integer()) and (boolean() -> boolean())
def negate(x) when is_integer(x), do: -x
def negate(x) when is_boolean(x), do: not x

# Singleton types

$ (false -> true) and (nil -> true)
def negate(false)
def negate(nil), do: true

# Type group definition

$ type t() = { integer() or string(), boolean() }

$ (t() -> t())
def example(x), do: x

# Polymorphism with local type inference
## term() is like a super type which represents all others having your real defined in runtime

$ ([a], b, (a, b -> b)) -> b when a: term(), b: term()
def reduce([h | t], acc, fun), do: reduce(t, fun.(h, acc), fun)
def reduce([], acc, _fun), do: acc

## Protocols

## Example with Enum.into/2

### Current typespec
into(Enumerable.t(), Collectable.t()) :: Collectable.t()

###  Using new static types
$ Enumerable.t(a), Collectable.t(b) -> Collectable.t(a or b) when a: term(), b: term()

$ type transversable = Enumerable.t(a) and Collectable.t(a)
$ a -> a when a: transversable(string())
def echo(var) do
  Enum.into(var, var)
end

# Using the symbol _ the compiler decides the best returning type
$ integer() -> _
def negate(x) when is_integer(x), do: -x

# Maps

$ %{age: integer(), ...} -> integer()
def get_age(person) when is_integer(person.age), do: person.age

# Gradual typing

$ dynamic() -> _
def foo1(x), do: ···