Issues

This page hints at some issues I foresee in creating Typed Elixir. I'm neither a Clojure nor an Elixir "language lawyer", so some of the following may be incomplete or even incorrect. No problem; just let me know about any problems you notice...

Approach

Dialyzer's type checking approach is based on "success typing" (discussed below); I'm not sure how Typed Clojure stands on this issue.

Generally speaking, analyzers will want to actually prove that there will be no type errors at run time, as in mathematically prove. This means that in a few circumstances, the type checker will disallow certain practically valid operations for the sake of removing uncertainty that could lead to crashes. ... The other option is then to have a type system that will not prove the absence of errors, but will do a best effort at detecting whatever it can. You can make such detection really good, but it will never be perfect. ...

-- Success Typing, in Type Specifications and Erlang

Data Structures

Erlang's set of built-in data types is very small (e.g., atoms, binaries, lists, tuples). However, this has been augmented by assorted functions. Elixir extends this further, using both functions and macros.

Elixir and Erlang have multiple ways of encoding strings (e.g., binaries, character lists, IO lists). This could complicate certain forms of type checking.

Clojure, Elixir, and Erlang all support persistent data structures. However, the details vary and Clojure's version is a couple of decades newer than the others, so some behavior is likely to be different.

Immutability

Clojure's approach to state is characterized by the concept of identities, which are represented as a series of immutable states over time. Since states are immutable values, any number of workers can operate on them in parallel, and concurrency becomes a question of managing changes from one state to another. For this purpose, Clojure provides several mutable reference types, each having well-defined semantics for the transition between states.

-- Philosophy, in Clojure (WP)

So, Clojure encourages the use of immutable data, but allows some (carefully controlled) wiggle room. Erlang takes a very strict approach: values are immutable and variables may only be assigned once. Elixir relaxes this somewhat, allowing variables to be reassigned.

Note: It is common in functional programming (e.g., in Clojure, Elixir, and Erlang) to use tail recursion, passing a mutated state to the called instance of the function. Elixir and Erlang's actors, in particular, use this strategy.

Lazy Evaluation

Neither Clojure nor Elixir supports lazy evaluation, per se. However, both have constructs that fill a similar role. For example, Clojure has sequences and Elixir has streams.

Macros

Macro definitions are ignored. The type checker operates on the macro-expanded form from the Compiler's analysis phase.

-- Quick Guide to core.typed

Macros are so fundamental to Elixir's implementation and programming paradigm that this decision might be worth revisiting for Typed Elixir.

Messages

From what I read, Dialyzer makes no attempt to analyze message types. Messages are so fundamental to the Elixir and Erlang programming model that this decision might be worth revisiting for Typed Elixir.

In Detection of Asynchronous Message Passing Errors Using Static Analysis, Maria Christakis and Konstantinos (aka Kostis) Sagonas discuss extensions to Dialyzer that address this issue. Kostis Sagonas also shows off some related technology in Cool Tools for Modern Erlang Program Development.

Optimization

There is some chance that Typed Elixir could help to optimize runtime behavior. José Valim notes:

For example, we could skip protocol dispatch and invoke the implementation directly if we know what is the type of the argument. We could also inline many functions in stdlib (like the Enum module), optimize calls like map.foo, simplify comparisons, and much more.

Pattern Matching

Elixir and Erlang both make extensive use of pattern matching. Indeed, Clojure's destructuring support looks a bit like a special case of this. Typed Elixir would have to handle pattern matching in a wide variety of contexts.

Runtime Support

Robert Virding says:

One problem with doing a Typed Elixir is that there is basically no support for this at run-time. The system allows you to load/reload any module you want, whenever you want and containing whatever you want. Usually this is not a problem as projects have some discipline. However, doing checks at compile- and build-time is definitely possible, which is how dialyzer works.

Tooling Support

Some concern has been expressed that Typed Elixir might siphon off support for Dialyzer. However, José Valim responds:

... We should definitely improve Dialyzer and any effort in this direction is definitely welcome. Erlang 18 will already be a huge improvement because we will be able to tag code that is generated by the compiler and reduce false positive warnings. However, there are still many pending tasks to make Dialyzer first class:

  • Most error messages in dialyzer are cryptic and go directly against Elixir's philosophy of good and clear error messages. We need to at least add our own reporting on top of Dialyzer.

  • Typespecs are optional, which means a lot of times folks simply won't do it and we have very little control in streamlining it.

  • The Elixir team cannot use typespecs in the compiler to optimize code, because they are not enforced.

I definitely would like to see those improved, but that should not affect Typed Elixir. We need to discuss and study different options before choosing something as the de facto solution. Having Dialyzer today is helpful, but I am nowhere confident it is the best solution for the problem at hand.

Folks are also interested in improving the behavior and integration of tools such as Alchemist, Neovim, Spacemacs, and Syntastic.


This wiki page is maintained by Rich Morin, an independent consultant specializing in software design, development, and documentation. Please feel free to email comments, inquiries, suggestions, etc!

Topic revision: r7 - 04 Apr 2016, RichMorin
This site is powered by Foswiki Copyright © by the contributing authors. All material on this wiki is the property of the contributing authors.
Foswiki version v2.1.6, Release Foswiki-2.1.6, Plugin API version 2.4
Ideas, requests, problems regarding CFCL Wiki? Send us email