Static Elixir

erlang
otp
ocaml
#1

Reading this post of @OvermindDL1, I realise that I like to use a statically typed language like OCaml:

OCaml comparison with Elixir

And it is possible with ease, to combine the strengths of both languages:

It is more easy to intelligible the OCaml code, while Elixir offers the benefit of the ErlangVM.

And i think that the implementation as a PPX combines the static type safety concept with the dynamic one, since the compilation happens in OCaml’s type system, while the execution happens in ErlangVM.

What is your opinion on this topic?

Is anybody interested to write this PPX? :heart_eyes:

Thanks a lot ^-^

2 Likes
Typed Elixir
#7

It is not a small amount of work. ^.^;

2 Likes
#8

Given on what has gone on before

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.

Alpaca’s approach is probably more practical.

2 Likes
Why aren't there any successful ML-family language based on BEAM?
Is it possible to transpile Elixir into ReasonML/BuckleScript/JavaScript?
#9

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… ^.^;

1 Like
#10

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

#11

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.

1 Like
#12

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. ^.^

#13

:stuck_out_tongue:

#14

almost trivially easy to extend

Be sure to include all context. :wink:
And it is, but choosing what elixir and how to represent the elixir and such is, well, an entire language. :wink:

2 Likes
#15

So, will you sound like its easy to translate it into Javascript and difficult to do the same with Elixir? :stuck_out_tongue:
run and hide

#16

You do know the javascript version took about 6 months to become viably useful yes? :wink:

#17

This seems like an extraordinarily low amount of time, given the task :stuck_out_tongue:

1 Like
#18

Well get started on it! :wink:

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).

1 Like
#19

I like types, but I have other priorities right now :stuck_out_tongue:

2 Likes
#20

This guy here also likes to see this:

1 Like
#21

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.

#22

This thread discusses speedon the BEAM: https://elixirforum.com/t/elixir-is-too-slow-and-you-wont-believe-suggestion-5/6805/15?u=tmbb

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.

2 Likes
#23

Thanks a lot, that makes it clear to me. :slight_smile:

#24

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.

1 Like
#25

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

1 Like