One day Phil phoned me up and announced that a) Erlang needed a type system, b) he had written a small prototype of a type system and c) he had a one yearâs sabbatical and was going to write a type system for Erlang and âwere we interested?â Answer ââYes.â
Phil Wadler and Simon Marlow worked on a type system for over a year and the results were published in [A practical subtyping system for Erlang]. The results of the project were somewhat disappointing. To start with, only a subset of the language was type-checkable, the major omission being the lack of process types and of type checking inter-process messages.
The dialyzer method of typing is success typing, it only ensures that what you type is sensible and logical, but it falls back to assuming the programmer knows what they are doing when it hits something that it cannot figure out. This is a perfectly reasonable typing system, however it has absolutely zero/zilch/nil/none/etc of the capabilities of, say, an HM typing system, which allows you to do type specific calls, like for example:
f.(x)
Right now you have to do this, because if you do f(x) then it does a direct function call because it does not not know what âfâ should be, like if it is a string then it knows it could instead call a direct version, but it does not know, hence why Elixir does a LISP-2 style system where functions and bindings are different scopes to work around it. If, however, the system itself was typed well enough to know that f is a binding and it binds to a function type then you could just do f(x) and it would call the binding if the binding was a function or a direct call if it were not, thus unifying the syntax and scopes now that you can safely do so thanks to the type information.
Plus a lot more like conditional branching at compile-time based on types, conditional compile-time dispatch (without the âvirtual callâ of anonymous functions or the testing of the type) based on type, etc⌠etcâŚ
Alpaca is more traditionally HM, but they are making a couple odd decisions in my opinion⌠^.^;
Everyone talks about processes when discussing static typing, but even typechecking on function atguments would already be pretty good.
Iâve used receive exacly once in real code. Iâd be vey happy if someone could type everything except that receive
Lisp-1 vs Lisp-2 has little to do with a type system, though. Elixir could easily be a lisp-1 language, but there was a design choice for it to be a lisp-2 one.
Little to do yes, but I was trying to (way too verbosely after reading it overâŚ) say that LISP-2 style is easier when you donât know the types, but LISP-1 is easier when you do know the types, so LISP-2 style makes sense for Elixir. ^.^
Really though, you could probably base it on Bucklescriptâs plugin and gain immediately useful things like itâs head optimizer (in traditional ML everything is a single arg function with a single return, in javascript it is multi-arg, bucklescript has a pass that optimizes known head sizes to call directly instead of currying, an optimization).
If somebody develops such a source to source converter in order to get static types into Elixir - which development steps would be on the plan in order to benefit from this in terms of speed?
Since the BEAM is completely dynamically typed today.
The main problem seems to be lack of inlining, not types. Lack of inlining leads to an overhead in function calls, which slows down the program. The BEAM could optimize this by taking hints form the Java VM, which does some clever things to inline classes (Java´s version of modules), which the BEAM doesnât and could do.
I doubt that any compiler that compiles to Elixir could give you significant speedups except by avoiding protocols and âslowâ stuff like that (i.e., always call :lists.reverse/1 instead of Enum.reverse/1). For the real optimizations youâd have to change the BEAM to support inlining as I said above. @OvermindDL1 has been playing with languages that compile to Elixir, so heâs probably the right person to answer this.
In any case, I think having static types is a benefit in itself, even if they donât make your program faster.
Yeah youâd be able to inline some calls via the other translater, and make some potentially dynamic calls actually static (which could be quite a speed boon in recursion), but otherwise the BEAM would not be able to do much otherwise.
I think typing Elixir would be pretty hard⌠The types that arise naturally from dynamic code can get pretty ugly when stated explicitly
Maybe gradual typing could be an interesting approach? Like giving no false positives that a piece of code type checks⌠so if it does type-check it is correct
Which is usually a great indication of poor code though!
Look at Gradualizer, it works on BEAM files, thus yes it works with elixir, just need someone to make a good mix plugin for it to simplify itâs elixir use (like Dialyxir does with dialyzer). ^.^
Agree that good code is typable but things like returning a tuple or a value can already be difficult to type clearly without proper sum types I think (if i recall correctly we would need intersection types and those are a pain to work with) although they are common in elixir code
