Skip to content

Instantly share code, notes, and snippets.

@josevalim
Last active Dec 24, 2018
Embed
What would you like to do?
defmodule Types do
@moduledoc """
A type system for Elixir.
The goal of the type system is to integrate well with
current Elixir code and idioms by relying on atoms,
tuples, lists and other regular Elixir data structures.
This means a function such as `File.read/1` can be typed
as:
def read(binary()) :: {:ok, binary()} | {:error, atom()}
The type system is based on union and intersection types.
The concept of union is quite simple. For example, if an argument
can be either an integer or an atom, we can express it as:
integer() | atom()
The concept of intersection is a bit more interesting. Generally
speaking, intersections do not make much sense, for example,
the intersection between the types `integer()` and `atom()` is
empty. The intersection between `atom()` and `:foo` is the atom
`:foo` itself. However, the concept of intersection is quite
interesting for functions, as they allow us to express functions
with multiple clauses, which is very common in Elixir.
For example, a function that receives an integer and returns an
integer would inhabit the type `(integer() -> integer())`. One
of such functions would be:
fn x :: integer() -> -x end
Another of such functions is:
fn x :: integer() -> -x
x :: boolean() -> not x end
Even though the function above has multiple clauses, it is still
capable of receiving an integer and returning another integer.
Similarly, a function that receives a boolean and returns a boolean
would inhabit the type `(boolean() -> boolean())`. One of such
functions would be:
fn x :: boolean() -> -x end
Another of such functions is:
fn x :: integer() -> -x
x :: boolean() -> not x end
As you can see, the function with two clauses above inhabits both
the type `(integer() -> integer())` and `(boolean() -> boolean())`.
This means that, if there is a function that receives an integer and
returns an integer as well as receive a boolean and returns a boolean,
it requires both types, which means that function exists in the
intersection between the types `(integer() -> integer())` and
`(boolean() -> boolean())`.
In the type system, we simply write that as a type with multiple
clauses:
(integer() -> integer(); boolean() -> boolean())
The intersection types literature has many interesting examples
where intersection types can be used to infer the types where
classic Hindley Milner type systems wouldn't. For example:
fn x -> {x.(0), x.(:foo)} end
has the type:
((0 -> a; :foo -> b) -> {a, b})
Elixir currently implements a subset of rank 2 intersection types,
as it only allows intersections that can be expressed as function
clauses and in a way there is no dependency between those multiple
clauses.
## Literature
We will now describe the literature that has been relevant to the
current implementation.
### Introductory
Those references contain introductory material on type system for
those not familiar with the concepts, nomenclature and implementation:
* Types and Programming Languages, 3rd edition (Benjamin C. Pierce)
* On Understanding Types, Data Abstraction, and Polymorphism (Luca Cardelli)
* How OCaml type checker works (Oleg Kiselyo) - a very accessible look
into generalization and possible optimizations.
### Intersection types
The following papers explore the ides behind intersection types.
* What are principal typings and what are they good for? (Trevor Jim)
This paper describes rank 2 intersection type systems. Elixir
implements a restricted rank 2 intersection types where intersections
can only be expressed as independent function clauses with shared
variables only in the body.
This means we can't infer the type for `x.(x)`, as it has the type
`(a ^ (a -> b))`, which is the intersection between a type variable
and a function. Similarly, `x.(x.(y))` would have an intersection
type `(a -> b) ^ (b -> c)` which has a dependency between a body and
a head variable.
We don't infer the first case for simplicity when using the type
system. We don't infer the second because type checking those functions
are expensive and complex, as they require a permutation of all possible
clauses that could match `(a -> b) ^ (b -> c)`.
In those scenarios, we infer the same type as in a Hindley-Milner system.
For all others, such as `{x.(:foo), x.(:bar)}`, we infer the proper
intersection type `(:bar -> a) ^ (:foo -> b)` expressed as
`(:bar -> a; :foo -> b)`. The recursive typing rules are also taken
from this paper, with the difference that recursion over intersection
types (i.e. between different clauses) is not allowed and converted
to a single clause.
### Erlang papers
The following papers are important because they describe other type
systems implemented for Erlang:
* Practical Type Inference Based on Success Typings (Tobias Lindahl, Konstantinos Sagonas)
The reference paper on Dialyzer and its trade-offs
"""
## Patterns
# 1. adding types/patterns to receive
# 2. mixing typed with non-typed
# 3. the cost of having duplicate syntax
## Function annotations
# 1. Annotations may have multiple clauses. Each clause must have at least one matching implementation.
# 2. Should we force a explicit type on fn true -> true; _ -> x end? If so, what to do on catch all?
## Guards
# Must perform exhaustion check based on patterns
# Must perform exhaustion check for base types (integers, atoms, floats, etc)
# Pattern matches {a, a} also require an exaustion check
# TODO: Use inline_list_funcs for performance.
## Forbidden
# [foo | bar] (developers must use cons(...) to avoid ambiguity)
## Built-in Patterns
# pattern number() :: integer() | float()
## Built-in Types
# type list(a) :: empty_list() | cons(a, list(a))
# type improper_list(a) :: empty_list() | cons(a, list(a) | a)
## Implemented Patterns
# pattern boolean() :: true | false
# pattern atom()
# pattern integer()
end
defmodule Types.CheckerTest do
use ExUnit.Case, async: true
alias Types.{Checker, Union}
defp format({:ok, types, %{inferred: inferred}}) do
types
|> Checker.bind_matching(inferred, inferred)
|> Union.to_iodata()
|> IO.iodata_to_binary()
end
defmacro quoted_of(expr) do
quote do
Checker.of(unquote(Macro.escape(expr)))
end
end
describe "of/1" do
test "atoms" do
assert quoted_of(nil) |> format() == "nil"
assert quoted_of(:foo) |> format() == ":foo"
assert quoted_of(true) |> format() == "true"
assert quoted_of(false) |> format() == "false"
end
test "tuples" do
assert quoted_of({:ok, :error}) |> format() == "{:ok, :error}"
end
test "lists" do
assert quoted_of([]) |> format() == "empty_list()"
assert quoted_of([true | false]) |> format() == "cons(true, false)"
assert quoted_of([true, false]) |> format() == "cons(true, cons(false, empty_list()))"
end
test "match" do
assert {:error, _, {:disjoint_match, _, _}} =
quoted_of({:ok, a :: atom()} = {:ok, 0})
assert {:error, _, {:disjoint_match, _, _}} =
quoted_of(fn a :: atom() -> :ok = a end)
end
test "generalization" do
assert quoted_of((y = fn x -> x end; y.(y))) |> format() ==
"(a -> a)"
assert quoted_of((y = fn x -> x end; z = y; {z, z})) |> format() ==
"{(a -> a), (b -> b)}"
assert quoted_of((y = fn x -> x end; fn z -> fn w -> {y, y} end end)) |> format() ==
"(a -> (b -> {(c -> c), (d -> d)}))"
assert quoted_of((z = fn x -> fn y -> y end end; {z, z})) |> format() ==
"{(a -> (b -> b)), (c -> (d -> d))}"
assert quoted_of((z = (fn x -> fn y -> y end end).(:foo); {z, z})) |> format() ==
"{(a -> a), (b -> b)}"
assert quoted_of((w = (fn x -> z = fn y -> y end; {z, z} end); {w, w})) |> format() ==
"{(a -> {(b -> b), (c -> c)}), (d -> {(e -> e), (f -> f)})}"
assert quoted_of(fn x -> y = (fn z -> z end).(x); {y, y} end) |> format() ==
"(a -> {a, a})"
assert quoted_of(fn x -> y = fn z -> x.(z) end; {y, y} end) |> format() ==
"((a -> b) -> {(a -> b), (a -> b)})"
assert quoted_of((y = (fn x -> fn z -> x.(z) end end).(fn w -> w end); {y, y})) |> format() ==
"{(a -> a), (b -> b)}"
assert quoted_of((y = fn x -> fn y -> x.(x.(y)) end end; {y, y})) |> format() ==
"{((a -> a) -> (a -> a)), ((b -> b) -> (b -> b))}"
assert quoted_of((w = fn x -> fn y -> fn z -> x.(y.(z)) end end end; {w, w})) |> format() ==
"{((a -> b) -> ((c -> a) -> (c -> b))), ((d -> e) -> ((f -> d) -> (f -> e)))}"
assert quoted_of(fn x -> y = x; y end) |> format() ==
"(a -> a)"
assert quoted_of(fn x -> z = fn y -> {x, y} end; {z, z} end) |> format() ==
"(a -> {(b -> {a, b}), (c -> {a, c})})"
end
end
describe "of/1 apply" do
test "simple" do
assert quoted_of((fn false -> true; true -> false end).(false)) |> format() ==
"true"
assert quoted_of((fn false -> true; true -> false end).(true)) |> format() ==
"false"
assert quoted_of((fn y :: atom() -> y end).(:foo)) |> format() ==
":foo"
assert {:error, _, {:disjoint_apply, _, _, _}} =
quoted_of(fn x :: atom() -> (fn :foo -> :foo end).(x) end)
assert {:error, _, {:disjoint_apply, _, _, _}} =
quoted_of(fn x :: boolean() -> (fn true -> true end).(x) end)
end
test "with inference" do
assert quoted_of(fn x -> (fn y -> y end).(x) end) |> format() ==
"(a -> a)"
assert quoted_of((fn y -> y end).(fn x -> x end)) |> format() ==
"(a -> a)"
assert quoted_of(fn x ->
(fn y :: boolean() -> y end).(x)
end) |> format() == "(false | true -> false | true)"
assert quoted_of(fn x ->
(fn y :: boolean() -> y end).(x)
(fn true -> true; false -> false end).(x)
end) |> format() == "(false | true -> false | true)"
assert quoted_of(fn x ->
(fn y :: boolean() -> y end).(x)
(fn y :: boolean() -> y end).(x)
end) |> format() == "(false | true -> false | true)"
assert quoted_of(fn x :: boolean() ->
(fn y -> y end).(x)
end) |> format() == "(false | true -> false | true)"
assert quoted_of(fn x ->
fn z ->
(fn y :: boolean() -> y end).(x)
end
x
end) |> format() == "(a -> a) when a: false | true"
assert quoted_of(fn x ->
(fn true -> true end).(x)
(fn z ->
(fn true -> true end).(z)
z
end).(x)
end) |> format() == "(true -> true)"
assert quoted_of(fn x ->
(fn {true, z} -> z end).({x, x})
end) |> format() == "(true -> true)"
assert quoted_of(fn x ->
(fn {z, true} -> z end).({x, x})
end) |> format() == "(true -> true)"
end
test "with inference on multiple clauses" do
assert quoted_of(fn x ->
(fn true -> true; false -> false end).(x)
(fn false -> false end).(x)
end) |> format() == "(false -> false)"
assert quoted_of(fn x ->
(fn false -> false end).(x)
(fn true -> true; false -> false end).(x)
end) |> format() == "(false -> false)"
assert quoted_of(fn x ->
(fn false -> false; nil -> nil; _ -> true end).(x)
end) |> format() == "(false | nil | a -> false | nil | true)"
assert quoted_of(fn x :: :foo ->
(fn :foo -> :bar; y :: atom() -> :baz end).(x)
end) |> format() == "(:foo -> :bar)"
assert quoted_of(fn x ->
(fn :foo -> :bar; y :: atom() -> :baz end).(x)
end) |> format() == "(atom() -> :bar | :baz)"
assert quoted_of(fn x :: atom() ->
(fn :foo -> :bar; y :: atom() -> :baz end).(x)
end) |> format() == "(atom() -> :bar | :baz)"
assert quoted_of(fn x :: atom() ->
(fn y :: boolean() -> :bar; z :: atom() -> :baz end).(x)
end) |> format() == "(atom() -> :bar | :baz)"
assert quoted_of(fn x ->
(fn :foo -> :bar; y -> y end).(x)
end) |> format() == "(:foo | a -> :bar | a)"
assert quoted_of((fn x ->
(fn :foo -> :bar; y -> y end).(x)
end).(:baz)) |> format() == ":bar | :baz"
assert quoted_of(fn x :: atom() ->
(fn :foo -> :bar; y -> y end).(x)
end) |> format() == "(a -> :bar | a) when a: atom()"
assert quoted_of((fn x :: atom() ->
(fn :foo -> :bar; y -> y end).(x)
end).(:baz)) |> format() == ":bar | :baz"
assert quoted_of(fn x :: boolean() ->
(fn true -> :foo; y -> y end).(x)
end) |> format() == "(false | true -> false | :foo)"
assert quoted_of(fn x :: integer() | atom() ->
(fn y :: integer() -> :foo; z -> {:bar, z} end).(x)
end) |> format() == "(integer() | a -> :foo | {:bar, a}) when a: atom()"
assert quoted_of(fn x ->
fn y :: boolean() ->
(fn {z, true} -> z; {:foo, false} -> false end).({x, y})
end
end) |> format() == "(:foo | a -> (false | true -> false | a))"
assert quoted_of(fn x ->
fn y :: boolean() ->
(fn {:foo, false} -> false; {z, true} -> z end).({x, y})
end
end) |> format() == "(:foo | a -> (false | true -> false | a))"
end
# TODO: Make this pass. See notes in union.ex.
# test "with inference on same vars" do
# assert quoted_of(fn {a :: integer(), b :: atom()} ->
# (fn {x, y} -> {x, y} end).({a, b})
# end) |> format() == ""
#
# assert quoted_of(fn {a :: integer(), b :: atom()} ->
# (fn {x, x} -> x end).({a, b})
# end) |> format() == ""
#
# assert quoted_of(fn {a :: integer(), b :: atom()} ->
# (fn {x, x} -> {x, x}; {x, y} -> {x, y} end).({a, b})
# end) |> format() == ""
# end
# Although intersection types do not require let polymorphism,
# we implement them to avoid having to rearrange ASTs into let
# formats. Papers such as "Let should not be generalized" argue
# against this in terms of simplicity on type systems that have
# constraints (although we haven't reached such trade-offs yet).
test "on variable" do
assert {:error, _, {:disjoint_apply, _, _, _}} =
quoted_of((
x = fn :bar -> :bar end
x.(:foo)
))
assert quoted_of((
x = fn y -> y end
x.(:foo)
)) |> format() == ":foo"
assert quoted_of((
x = fn y :: atom() -> y end
x.(:foo)
)) |> format() == ":foo"
assert quoted_of((
x = fn y -> y end
{x.(:foo), x.(:foo)}
)) |> format() == "{:foo, :foo}"
assert quoted_of((
x = fn y -> y end
{x.(:foo), x.(:bar)}
)) |> format() == "{:foo, :bar}"
assert quoted_of((
x = fn y, z -> {y, z} end
{x.(:foo, :bar), x.(:bar, :baz)}
)) |> format() == "{{:foo, :bar}, {:bar, :baz}}"
end
test "with function argument" do
# ((a -> b) -> (a -> b)) match
assert quoted_of((fn x -> fn y -> x.(y) end end).
(fn :foo -> :bar end)) |> format() ==
"(:foo -> :bar)"
# ((a -> b) -> (a -> b)) superset
assert quoted_of((fn x -> fn y -> x.(y) end end).
(fn x :: atom() -> x end)) |> format() ==
"(atom() -> atom())"
# ((a -> b) -> (a -> b)) multiple clauses
assert quoted_of((fn x -> fn y -> x.(y) end end).
(fn :foo -> :bar; :bar -> :bat end)) |> format() ==
"(:bar | :foo -> :bar | :bat)"
# ((a -> a) -> (a -> a)) match
assert quoted_of((fn x -> fn y -> x.(x.(y)) end end).
(fn :foo -> :foo end)) |> format() ==
"(:foo -> :foo)"
# ((a -> a) -> (a -> a)) no match
assert {:error, _, {:disjoint_apply, _, _, _}} =
quoted_of((fn x -> fn y -> x.(x.(y)) end end).
(fn :foo -> :bar; :bar -> :baz end))
# ((a -> a) -> (a -> a)) superset
assert quoted_of((fn x -> fn y -> x.(x.(y)) end end).
(fn x :: atom() -> x end)) |> format() ==
"(atom() -> atom())"
# ((a -> a) -> (a -> a)) multiple clauses
assert quoted_of((fn x -> fn y -> x.(x.(y)) end end).
(fn :foo -> :foo; :bar -> :bar; :no -> :match end)) |> format() ==
"(:bar | :foo -> :bar | :foo)"
assert quoted_of((fn x -> fn y -> x.(x.(y)) end end).
(fn :foo -> :foo; :bar -> :bar end).
(:foo)) |> format() ==
":foo"
# (((b -> b) -> a) -> a) matches
assert quoted_of((fn x -> x.(fn y -> y end) end).
(fn x -> {x.(:foo), x.(:bar)} end)) |> format() ==
"{:foo, :bar}"
assert quoted_of((fn x -> x.(fn y -> y end) end).
(fn x -> {x, x.(:foo), x.(:bar)} end)) |> format() ==
"{(:bar -> :bar; :foo -> :foo), :foo, :bar}"
assert quoted_of((fn x -> {x, x.(fn y -> y end)} end).
(fn x -> {x.(:foo), x.(:bar)} end)) |> format() ==
"{((:bar | :foo -> :bar | :foo) -> {:foo, :bar}), {:foo, :bar}}"
end
test "with function argument and type-recursive" do
# # Generalization
assert quoted_of((
y = (fn x -> fn y -> x.(x.(y)) end end).(fn z -> z end)
{y, y}
)) |> format() == "{(a -> a), (b -> b)}"
# Multiple clauses
assert quoted_of((
y = (fn x -> fn y -> x.(x.(y)) end end).(fn :foo -> :foo; z -> z end)
{y, y}
)) |> format() == "{(:foo | a -> :foo | a), (:foo | b -> :foo | b)}"
# Multiple applications
assert quoted_of((fn x -> fn y -> x.(x.(y)) end end).
(fn z -> z end).
(fn :foo -> :foo; :bar -> :bar end)) |> format() ==
"(:foo -> :foo; :bar -> :bar)"
end
test "on intersection types" do
assert quoted_of((fn x ->
x.(:foo)
end).(fn y -> y end)) |> format() == ":foo"
assert quoted_of((fn x ->
{x.(:foo), x.(:bar)}
end).(fn y -> y end)
) |> format() == "{:foo, :bar}"
# Same clauses
assert quoted_of((fn x ->
{x.(:foo), x.(:bar)}
end).(fn :foo -> :x; :bar -> :y end)
) |> format() == "{:x, :y}"
# More clauses
assert quoted_of((fn x ->
{x.(:foo), x.(:bar)}
end).(fn :foo -> :x; :bar -> :y; :baz -> :z end)) |> format() == "{:x, :y}"
# Less clauses
assert {:error, _, {:disjoint_apply, _, _, _}} =
quoted_of((fn x ->
{x.(:foo), x.(:bar), x.(:baz)}
end).(fn :foo -> :x; :bar -> :y end))
# Supertype
assert quoted_of((fn x ->
{x.(:foo), x.(:bar), x.(:baz)}
end).(fn y :: atom() -> y end)
) |> format() == "{:foo, :bar, :baz}"
# Does not restrict functions
assert quoted_of((
c = fn y -> y end
(fn x -> {x.(:foo), x.(:bar)} end).(c)
c
)) |> format() == "(a -> a)"
# Works at multiple levels
assert quoted_of(
(fn x ->
{x.(:foo).(:baz), x.(:bar).(:bat)}
end).(fn x -> fn y -> y end end)
) |> format() == "{:baz, :bat}"
end
test "on intersection types with subsets" do
assert quoted_of(fn z ->
(fn {x, y :: atom()} ->
x.(y)
end).({fn :foo -> :bar; w :: atom() -> :baz end, z})
end) |> format() == "(atom() -> :bar | :baz)"
end
test "on intersection types with free variables" do
assert quoted_of(fn z ->
(fn x -> {x.({:ok, z}), x.({:error, z})} end).
(fn {:ok, :ok} -> :bar; {:error, :ok} -> :foo end)
end) |> format() == "(:ok -> {:bar, :foo})"
assert {:error, _, {:disjoint_apply, _, _, _}} =
quoted_of(fn z ->
(fn x -> {x.({:ok, z}), x.({:error, z})} end).
(fn {:ok, :ok} -> :bar; {:error, :error} -> :foo end)
end)
end
test "on intersection types with multiple arguments" do
# First arg
assert quoted_of((fn x, y -> {x.({:foo, y}), x.({:bar, y})} end).
(fn {:foo, :ok} -> :bar; {:bar, :ok} -> :foo end, :ok)) |> format() ==
"{:bar, :foo}"
assert quoted_of(fn z ->
(fn x, y -> {x.({:foo, y}), x.({:bar, y})} end).
(fn {:foo, :ok} -> :bar; {:bar, :ok} -> :foo end, z)
end) |> format() == "(:ok -> {:bar, :foo})"
assert {:error, _, {:disjoint_apply, _, _, _}} =
quoted_of((fn x, y -> {x.({:foo, y}), x.({:bar, y})} end).
(fn {:foo, :ok} -> :bar; {:bar, :error} -> :foo end, :ok))
assert {:error, _, {:disjoint_apply, _, _, _}} =
quoted_of(fn z ->
(fn x, y -> {x.({:foo, y}), x.({:bar, y})} end).
(fn {:foo, :ok} -> :bar; {:bar, :error} -> :foo end, z)
end)
# Second arg
assert quoted_of((fn y, x -> {x.({:foo, y}), x.({:bar, y})} end).
(:ok, fn {:foo, :ok} -> :bar; {:bar, :ok} -> :foo end)) |> format() ==
"{:bar, :foo}"
assert quoted_of(fn z ->
(fn y, x -> {x.({:foo, y}), x.({:bar, y})} end).
(z, fn {:foo, :ok} -> :bar; {:bar, :ok} -> :foo end)
end) |> format() == "(:ok -> {:bar, :foo})"
assert {:error, _, {:disjoint_apply, _, _, _}} =
quoted_of((fn y, x -> {x.({:foo, y}), x.({:bar, y})} end).
(:ok, fn {:foo, :ok} -> :bar; {:bar, :error} -> :foo end))
assert {:error, _, {:disjoint_apply, _, _, _}} =
quoted_of(fn z ->
(fn y, x -> {x.({:foo, y}), x.({:bar, y})} end).
(z, fn {:foo, :ok} -> :bar; {:bar, :error} -> :foo end)
end)
end
test "with lazy inference" do
# Binding are lazy (z is true and not true | false)
assert quoted_of(fn z ->
(fn true -> true; false -> false end).(z)
x = z
(fn true -> true end).(z)
x
end) |> format() == "(true -> true)"
assert quoted_of(fn z ->
(fn true -> true end).(z)
x = z
(fn true -> true; false -> false end).(z)
x
end) |> format() == "(true -> true)"
# Match types cannot be not lazy though
assert quoted_of(fn x ->
z = (fn true -> true; false -> false end).(x)
(fn true -> true end).(x)
z
end) |> format() == "(true -> false | true)"
assert quoted_of(fn x ->
(fn true -> true end).(x)
z = (fn true -> true; false -> false end).(x)
z
end) |> format() == "(true -> true)"
# z must be nil
assert quoted_of(fn z ->
(fn x -> nil = x.(:any) end).(fn y -> z end)
z
end) |> format() == "(nil -> nil)"
# z conflicts with external value
assert {:error, _, {:disjoint_apply, _, _, _}} =
quoted_of(fn z ->
(fn true -> true; false -> false end).(z)
(fn x -> nil = x.(:any) end).(fn y -> z end)
end)
# z conflicts with internal value
assert {:error, _, {:disjoint_apply, _, _, _}} =
quoted_of(fn z ->
(fn x -> true = x.(:foo); false = x.(:bar) end).(fn y -> z end)
z
end)
# z conflicts with internal value and multiple clauses
assert {:error, _, {:disjoint_apply, _, _, _}} =
quoted_of(fn z ->
(fn x -> true = x.(:foo); false = x.(:bar) end).(fn :foo -> z; :bar -> z end)
end)
end
end
describe "of/1 with variable tracking" do
test "tuples" do
assert quoted_of(({x = :ok, y = :error}; y)) |> format() == ":error"
end
test "blocks" do
assert quoted_of((a = :ok; b = a; b)) |> format() == ":ok"
end
test "pattern matching" do
assert quoted_of((a = (a = true; b = false); a)) |> format() == "false"
end
test "with binding" do
assert quoted_of((x :: boolean()) = true) |> format() ==
"true"
assert quoted_of(fn y -> x = y; x end) |> format() ==
"(a -> a)"
assert quoted_of(fn y :: atom() -> x = y; x end) |> format() ==
"(a -> a) when a: atom()"
assert quoted_of(fn y -> (x :: atom()) = y; x end) |> format() ==
"(a -> a) when a: atom()"
assert {:error, _, {:disjoint_match, _, _}} =
quoted_of(fn y -> (x :: atom()) = y; (x :: integer()) = y; y end)
assert {:error, _, {:disjoint_match, _, _}} =
quoted_of(fn y :: atom() -> (x :: boolean()) = y; y end)
assert {:error, _, {:disjoint_match, _, _}} =
quoted_of(fn x -> true = (fn y :: boolean() -> y end).(x) end)
end
end
describe "of/1 fns" do
test "with no args" do
assert quoted_of(fn -> :ok end) |> format() ==
"(-> :ok)"
end
test "patterns" do
assert quoted_of(fn x -> x end) |> format() ==
"(a -> a)"
assert quoted_of(fn {x :: integer(), x} -> x end) |> format() ==
"({integer(), integer()} -> integer())"
assert quoted_of(fn {x :: integer(), x :: integer()} -> x end) |> format() ==
"({integer(), integer()} -> integer())"
assert quoted_of(fn x :: boolean() -> x end) |> format() ==
"(false | true -> false | true)"
assert quoted_of(fn {:ok, x :: boolean()} -> x end) |> format() ==
"({:ok, false} | {:ok, true} -> false | true)"
assert {:error, _, {:bound_var, _, _, _}} =
quoted_of(fn {x, x :: boolean()} -> x end)
assert {:error, _, {:bound_var, _, _, _}} =
quoted_of(fn {x :: integer(), x :: boolean()} -> x end)
end
# TODO: Handle duplicate clauses
# test "duplicate clauses" do
# assert quoted_of(fn 0 -> 0; 1 -> 1 end) |> format() == "(integer() -> integer())"
# end
test "late propagation" do
assert quoted_of(fn x ->
z = x
(fn 0 -> 0 end).(x) # TODO: This should emit a warning for being non-exaustive.
z
end) |> format() == "(integer() -> integer())"
end
test "free variables" do
assert quoted_of(fn x -> x end) |> format() ==
"(a -> a)"
assert quoted_of(fn x -> fn y -> y end end) |> format() ==
"(a -> (b -> b))"
assert quoted_of(fn x -> fn y -> x end end) |> format() ==
"(a -> (b -> a))"
assert quoted_of(fn x -> x.(fn y -> y end) end) |> format() ==
"(((a -> a) -> b) -> b)"
assert quoted_of(fn x -> fn y -> x.(y) end end) |> format() ==
"((a -> b) -> (a -> b))"
assert quoted_of(fn x -> fn y -> y.(x) end end) |> format() ==
"(a -> ((a -> b) -> b))"
assert quoted_of(fn x -> fn y -> x.(x.(y)) end end) |> format() ==
"((a -> a) -> (a -> a))"
end
test "rank 2 inference" do
assert quoted_of(fn x -> {x.(:foo), x.(:foo)} end) |> format() ==
"((:foo -> a) -> {a, a})"
assert quoted_of(fn x -> {x.(x.(:foo)), x.(x.(:bar))} end) |> format() ==
"((:bar -> :bar; :foo -> :foo) -> {:foo, :bar})"
assert quoted_of(fn x -> fn y -> {x.(y), x.(:foo), x.(:bar)} end end) |> format() ==
"((:bar -> a; :foo -> b; c -> d) -> (c -> {d, b, a}))"
assert quoted_of(fn x -> fn y -> {x.(:foo), x.(y), x.(:bar)} end end) |> format() ==
"((:bar -> a; :foo -> b; c -> d) -> (c -> {b, d, a}))"
assert quoted_of(fn x -> fn y -> {x.(:foo), x.(:bar), x.(y)} end end) |> format() ==
"((:bar -> a; :foo -> b; c -> d) -> (c -> {b, a, d}))"
assert quoted_of(fn x -> fn y -> {x.(:foo), x.(x.(y))} end end) |> format() ==
"((:foo -> a; b -> b) -> (b -> {a, b}))"
assert quoted_of(fn x -> fn y -> {x.(y), x.(y)} end end) |> format() ==
"((a -> b) -> (a -> {b, b}))"
assert quoted_of(fn x -> fn y -> fn z -> {x.(y), x.(z)} end end end) |> format() ==
"((a -> b; c -> d) -> (a -> (c -> {b, d})))"
assert quoted_of(fn x -> fn y -> {x.(x.(y)), x.(:foo)} end end) |> format() ==
"((:foo -> a; b -> b) -> (b -> {b, a}))"
assert quoted_of(fn x -> fn y -> {x.(x.(y)), x.(x.(y))} end end) |> format() ==
"((a -> a) -> (a -> {a, a}))"
assert quoted_of(fn x -> {x.(:foo), x.(:bar)} end) |> format() ==
"((:bar -> a; :foo -> b) -> {b, a})"
assert quoted_of(fn y -> fn x -> {x.(:foo), x.(:bar)} end end) |> format() ==
"(a -> ((:bar -> b; :foo -> c) -> {c, b}))"
assert quoted_of(fn x -> {x.(:foo).(:baz), x.(:bar).(:bat)} end) |> format() ==
"((:bar -> (:bat -> a); :foo -> (:baz -> b)) -> {b, a})"
# With supertypes
assert quoted_of(fn x ->
z = (fn z :: atom() -> z end).(:bar)
{x.(:foo), x.(z)}
end) |> format() == "((:bar -> a; :foo -> b) -> {b, a})"
assert quoted_of(fn x ->
z = (fn z :: atom() -> z end).(:bar)
{x.(z), x.(:foo)}
end) |> format() == "((:foo -> a; :bar -> b) -> {b, a})"
assert quoted_of(fn x, y ->
z = (fn z :: atom() -> z end).(y)
{x.(z), x.(:foo)}
end) |> format() == "((:foo -> a; atom() -> b), atom() -> {b, a})"
assert quoted_of(fn x, y ->
z = (fn z :: atom() -> z end).(y)
{x.(:foo), x.(z)}
end) |> format() == "((:foo -> a; atom() -> b), atom() -> {a, b})"
assert {:error, _, {:occurs, _, _, _, _}} =
quoted_of(fn x -> fn y -> {x.(y), y.(x)} end end)
assert {:error, _, {:self_var_apply, _, _, _}} =
quoted_of(fn x -> x.(x) end)
assert {:error, _, {:self_var_apply, _, _, _}} =
quoted_of(fn y -> x = y; x.(x) end)
assert {:error, _, {:disjoint_var_apply, _}} =
quoted_of(fn x -> {x.(:foo), x.(:foo, :bar)} end)
assert {:error, _, {:recursive_var_apply, _}} =
quoted_of(fn x -> x.({:foo, x.(:foo)}) end)
end
test "multiple arguments" do
assert quoted_of(fn x, y -> x.(y) end) |> format() ==
"((a -> b), a -> b)"
assert quoted_of(fn x, y -> y.(x) end) |> format() ==
"(a, (a -> b) -> b)"
assert quoted_of(fn x, y -> {x.(y), y.(x)} end) |> format() ==
"((a -> b), (c -> d) -> {b, d}) when c: ((c -> d) -> b), a: ((a -> b) -> d)"
end
test "multiple clauses" do
assert quoted_of(fn false -> false; nil -> nil; _ -> true end) |> format() ==
"(false -> false; nil -> nil; a -> true)"
end
test "binding" do
assert quoted_of(fn x -> fn y :: atom() -> y end end) |> elem(1) ==
[{:fn,
[{[[{:var, {:x, nil}, 0}]],
[{:fn,
[{[[{:var, {:y, nil}, 1}]],
[{:var, {:y, nil}, 1}]
}], %{1 => [:atom]}, 1}]
}], %{0 => []}, 1}]
assert quoted_of(fn x -> fn y -> y end end) |> elem(1) ==
[{:fn,
[{[[{:var, {:x, nil}, 0}]],
[{:fn,
[{[[{:var, {:y, nil}, 1}]],
[{:var, {:y, nil}, 1}]
}], %{1 => []}, 1}]
}], %{0 => []}, 1}]
assert quoted_of(fn x -> fn y -> x end end) |> elem(1) ==
[{:fn,
[{[[{:var, {:x, nil}, 0}]],
[{:fn,
[{[[{:var, {:y, nil}, 1}]],
[{:var, {:x, nil}, 0}]
}], %{1 => []}, 1}]
}], %{0 => []}, 1}]
assert quoted_of(fn x -> fn y -> x.(y) end end) |> elem(1) ==
[{:fn,
[{[[{:fn, [{[[{:var, {:y, nil}, 1}]], [{:var, {:x, nil}, 2}]}], %{}, 1}]],
[{:fn, [{[[{:var, {:y, nil}, 1}]], [{:var, {:x, nil}, 2}]}], %{}, 1}]
}], %{1 => [], 2 => []}, 1}]
assert quoted_of(fn x -> fn y :: atom() -> x.(y) end end) |> elem(1) ==
[{:fn,
[{[[{:fn, [{[[{:var, {:y, nil}, 1}]], [{:var, {:x, nil}, 2}]}], %{}, 1}]],
[{:fn, [{[[{:var, {:y, nil}, 1}]], [{:var, {:x, nil}, 2}]}], %{}, 1}],
}], %{1 => [:atom], 2 => []}, 1}]
assert quoted_of(fn x -> fn y -> x.(x.(y)) end end) |> elem(1) ==
[{:fn,
[{[[{:fn, [{[[{:var, {:y, nil}, 1}]], [{:var, {:y, nil}, 1}]}], %{}, 1}]],
[{:fn, [{[[{:var, {:y, nil}, 1}]], [{:var, {:y, nil}, 1}]}], %{}, 1}],
}], %{1 => []}, 1}]
assert quoted_of(fn x -> fn y -> fn z -> x.(x.(z)) end end end) |> elem(1) ==
[{:fn,
[{[[{:fn, [{[[{:var, {:z, nil}, 2}]], [{:var, {:z, nil}, 2}]}], %{}, 1}]],
[{:fn,
[{[[{:var, {:y, nil}, 1}]],
[{:fn, [{[[{:var, {:z, nil}, 2}]], [{:var, {:z, nil}, 2}]}], %{}, 1}],
}], %{1 => []}, 1}]
}], %{2 => []}, 1}]
assert quoted_of(fn x -> fn y -> fn z -> x.(y.(z)) end end end) |> elem(1) ==
[{:fn,
[{[[{:fn, [{[[{:var, {:y, nil}, 3}]], [{:var, {:x, nil}, 4}]}], %{}, 1}]],
[{:fn,
[{[[{:fn, [{[[{:var, {:z, nil}, 2}]], [{:var, {:y, nil}, 3}]}], %{}, 1}]],
[{:fn, [{[[{:var, {:z, nil}, 2}]], [{:var, {:x, nil}, 4}]}], %{}, 1}],
}], %{2 => []}, 1}],
}], %{3 => [], 4 => []}, 1}]
assert quoted_of((fn x -> fn y -> x.(x.(y)) end end).
(fn :foo -> :foo; :bar -> :bar end)) |> elem(1) ==
[{:fn, [{[[{:var, {:y, nil}, 1}]], [{:var, {:y, nil}, 1}]}], %{}, 1}]
assert quoted_of(recur = fn {:+, num} -> recur(num); num -> num end) |> elem(1) ==
[{:fn,
[{[[{:tuple, [{:atom, :+}, {:var, {:num, nil}, 0}], 2}]],
[{:var, {:apply, Types.Checker}, 3}]},
{[[{:var, {:num, nil}, 2}]],
[{:var, {:num, nil}, 2}]}],
%{0 => [{:tuple, [{:atom, :+}, {:var, {:num, nil}, 0}], 2},
{:var, {:apply, Types.Checker}, 3}],
2 => [],
3 => []}, 1}]
end
end
describe "of/1 lists" do
test "matching cons" do
assert quoted_of((fn [x | y] -> {x, y} end).([:foo])) |> format() ==
"{:foo, empty_list()}"
assert quoted_of((fn [x | y] -> {x, y} end).([:foo | :bar])) |> format() ==
"{:foo, :bar}"
assert quoted_of((fn [x | y] -> {x, y} end).([:foo, :bar, :baz])) |> format() ==
"{:foo, cons(:bar, cons(:baz, empty_list()))}"
assert quoted_of((fn [x, y, z] -> {x, y, z} end).([:foo, :bar, :baz])) |> format() ==
"{:foo, :bar, :baz}"
assert {:error, _, _} =
quoted_of((fn [x, y, z, w] -> {x, y, z, w} end).([:foo, :bar, :baz]))
assert {:error, _, _} =
quoted_of((fn [x | y] -> {x, y} end).([]))
end
end
describe "of/1 recur" do
test "single variable recursive tuples" do
# Free variables
assert quoted_of(recur = fn
{:+, num} ->
recur(num)
num :: integer() ->
num
end) |> format() == "({:+, a} -> integer(); integer() -> integer()) when a: integer() | {:+, a}"
# Free variables idempotency
assert quoted_of(recur = fn
{:+, num} ->
recur(num)
recur(num)
num :: integer() ->
num
end) |> format() == "({:+, a} -> integer(); integer() -> integer()) when a: integer() | {:+, a}"
# Invert free variables ordering
assert quoted_of(recur = fn
num :: integer() ->
num
{:+, num} ->
recur(num)
end) |> format() == "(integer() -> integer(); {:+, a} -> integer()) when a: integer() | {:+, a}"
# Superset variables
assert quoted_of(recur = fn
{:+, num} ->
(fn x :: integer() -> x; y :: atom() -> y end).(num)
recur(num)
num :: integer() ->
num
end) |> format() == "({:+, integer()} -> integer(); integer() -> integer())"
# Untyped variable
assert quoted_of(recur = fn
{:+, num} ->
recur(num)
num ->
num
end) |> format() == "({:+, a} -> b; c -> c) when a: {:+, a} | b"
assert quoted_of(recur = fn
{:+, num} ->
recur(num)
{:-, num} ->
num
end) |> format() == "({:+, a} -> b; {:-, b} -> b) when a: {:+, a} | {:-, b}"
# Disjoint input
assert {:error, _, {:disjoint_apply, _, _, _}} =
quoted_of(recur = fn
{:+, num} ->
(fn x :: atom() -> x end).(num)
recur(num)
num :: integer() ->
num
end)
# Disjoint output
assert {:error, _, {:recur_return, _, _}} =
quoted_of(recur = fn
{:+, num} ->
(fn x :: atom() -> x end).(recur(num))
num :: integer() ->
num
end)
# Superset output
assert {:error, _, {:recur_return, _, _}} =
quoted_of(recur = fn
{:+, num} ->
(fn true -> true end).(recur(num))
num :: atom() ->
num
end)
end
test "multiple variables recursive tuples" do
# Multiple variables
assert quoted_of(recur = fn
{:+, left, right} ->
{:+, recur(left), recur(right)}
num :: integer() ->
num
end) |> format() == "({:+, a, b} -> {:+, c, d}; integer() -> integer()) " <>
"when a: integer() | {:+, a, b}, b: integer() | {:+, a, b}, " <>
"c: integer() | {:+, c, d}, d: integer() | {:+, c, d}"
# # Multiple variables over multiple clauses
assert quoted_of(recur = fn
{:+, num} ->
{:+, recur(num)}
{:-, num} ->
{:-, recur(num)}
num :: integer() ->
num
end) |> format() == "({:+, a} -> {:+, b}; {:-, c} -> {:-, d}; integer() -> integer()) " <>
"when a: integer() | {:+, a} | {:-, c}, " <>
"b: integer() | {:+, b} | {:-, d}, " <>
"c: integer() | {:+, a} | {:-, c}, " <>
"d: integer() | {:+, b} | {:-, d}"
# Multiple variables over multiple clauses with free variable
assert quoted_of(recur = fn
{:+, num} ->
{:+, recur(num)}
{:-, num} ->
{:-, recur(num)}
num ->
num
end) |> format() == "({:+, a} -> {:+, b}; {:-, c} -> {:-, d}; e -> e) " <>
"when a: {:+, a} | {:-, c} | f, " <>
"b: {:+, b} | {:-, d} | f, " <>
"c: {:+, a} | {:-, c} | g, " <>
"d: {:+, b} | {:-, d} | g"
end
test "applied on recursive tuples" do
assert quoted_of((recur = fn
{:+, num} ->
recur(num)
{:-, num} ->
num
end).({:+, {:-, :foo}})) |> format() == ":foo"
assert quoted_of(fn z ->
(recur = fn
{:+, num} ->
{:+, recur(num)}
{:-, num} ->
{:-, recur(num)}
num :: integer() ->
num
end).(z)
end) |> format() ==
"(integer() | {:+, a} | {:-, b} -> integer() | {:+, c} | {:-, d}) " <>
"when a: integer() | {:+, a} | {:-, b}, " <>
"c: integer() | {:+, c} | {:-, d}, " <>
"b: integer() | {:+, a} | {:-, b}, " <>
"d: integer() | {:+, c} | {:-, d}"
assert {:error, _, {:disjoint_apply, _, _, _}} =
quoted_of((recur = fn
{:+, num} ->
recur(num)
{:-, num} ->
num
end).({:+, {:*, 1}}))
end
test "unified with intersection type on recusive tuples" do
assert quoted_of((fn x ->
{x.({:-, :one}), x.({:+, {:-, :two}}), x.({:+, {:+, {:-, :three}}})}
end).(recur = fn
{:+, num} ->
recur(num)
{:-, num} ->
num
end)) |> format() == "{:one, :two, :three}"
assert {:error, _, {:disjoint_apply, _, _, _}} =
quoted_of((fn x ->
x.({:+, :error})
end).(recur = fn
{:+, num} ->
recur(num)
{:-, num} ->
num
end))
end
test "recursive on cons" do
# Free variables
assert quoted_of(recur = fn
[h | t] ->
[h | recur(t)]
[] ->
[]
end) |> format() == "(cons(a, b) -> cons(a, c); empty_list() -> empty_list()) " <>
"when b: empty_list() | cons(a, b), " <>
"c: empty_list() | cons(a, c)"
end
end
end
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment