ExType: a type checker for Elixir

ExType is a type checker for Elixir.

Rationale

Dialyzer is good and helpful. But it does not have support for some common Elixir code (e.g. Protocol) and “success typing” is too loose sometimes.

Therefore, I would like to have a type checker written in Elixir (easier to get contribution from Elixir user, like me) and designed for Elixir (support common Elixir code).

Idea

The idea is similar to this, it scans all AST of def / defp with specs and check if type matches.

Feature

  • gradual typing
  • type check for protocol and generic protocol
  • type check with intersection and union types
  • type guards
  • type assertion
  • type inspection

Example

result = Enum.reduce([1, 2, 3], 0, fn i, acc ->
  i + acc
end)

The type checker can infer that i, acc and result all have integer() type.

More concrete examples are available at here.

Project

The project is published under MIT license and it’s available at github.com/gyson/ex_type.

Would like to hear any feedback or suggestion. You can reply this thread or create github issue if it’s bug.

15 Likes