Typed Elixir

Chat / Discussions
24

So… :slight_smile: why is nobody talking about this two recently published papers on session types?:

3 Likes
25

Sadly they don’t fit the BEAM ecosystem well, because both the code can mutate (hot-code reloading) and even within a single process the variety of types that it can take in a message is unbounded as you can spin up a new receive call at any time to receive anything you want, even through anonymous function calls and more. The really only good method to handle messages in a backwards compatible way on the beam is to black-box them and match out what you need at the time.

26

I can see how code replacement complicates many aspects of a type checker but even then I can’t imagine any fundamental reason to why the Multiparty Session Types framework couldn’t be implemented for a typed Elixir. Anyway, I believe your second concern is addressed in Exceptional Asynchronous Session Types (linked in my previous post) with their variant of the Gay-Vasconcelos language, EGV.

There is also some previous work on session types focused on Erlang specifically such as Let It Recover: Multiparty Protocol-Induced Recovery, which is quite interesting :slight_smile:

1 Like
27

I’ve had a question pop up repeatedly while reading this thread. I don’t mean to derail the conversation, but this seems as good a place as any to ask.

I’ve always been puzzled by the fascination that some people have with static typing and I’m hoping someone here can give some insights.

Personally, I’ve written code professionally in:

  • Statically/weakly typed languages (C and C++)
  • Statically/stongly typed languages (C#, Java, and F#, and a little bit in Scala and Haskell)
  • Dynamically/strongly typed languages (Python, Ruby, Elixir, Clojure)
  • Dynamically/weakly typed languages (Perl and JavaScript)

I can definitely see the value in strongly typed languages over weakly typed languages, like Perl and JavaScript. Nobody wants to deal with “5” + 5 having any kind of meaning, but the desire for static typing in a strongly-typed language is a complete mystery to me. In fact, I much prefer working with dynamically/strongly typed languages than statically/strongly typed languages because I don’t have to type a bunch of bits of boilerplate code all over the place (e.g. “This is an int,” “This is a string,” etc.)

I’ve never once thought, “Man, if only this strongly-typed language had static typing, all my woes would disappear.” It just has never been an issue for me. I’ve never missed static typing when switching between Elixir and Java, for instance. Actually, it has always been quite the contrary. I find Java’s typing annoying and unnecessary, especially when I’m using guards and pattern-matching in Elixir. I cannot think of anything I’d actually want less in Elixir than static typing.

So, what am I missing here?

28

Welcome @innocentoldguy! I think the key thing here is that Java is probably a good example of a language where types are a pain to use. There are other languages however that have substantially better type inferencing, and this allows you for example to simply add types at the function definition level, and internally they’re all inferred.

The value of going to this effort is that you get a faster, higher fidelity feedback loop for a broad variety of bugs (note I’m not saying all bugs). Are you sometimes passing nil into a function that always expects a number? Compiler has your back. Are you trying to access fields on a struct value? The editor easily knows what type you’ve got and has your back.

Beyond the basics though, you can also use types to help enforce rules about your program. Here is a good article on the subject: Designing with types: Making illegal states unrepresentable | F# for fun and profit

6 Likes
29

Thanks for your reply! I think I see what I’m missing.

I’ve always coded with a mostly vanilla setup of Vim. The only plugins I use are for color schemes and code indenting. I don’t ever use any of the hand-holding features found in other editors/IDEs, like VSCode, even though Vim does support them. Instead, I read the code and write my additions accordingly. That’s probably why I’ve never seen the value in static typing and why it has never been an issue for me.

Thanks! Now I know.

1 Like
30

I don’t agree with the affirmation that Elixir is a dynamic strongly typed language.

I know it has pattern matching and guards, but that is not enough.

When they add native support to type a struct, so that it cannot be created/modified with the wrong type, then I will agree with the statement. Yes I know you have libraries to help with this or you can use Dializer, but that can all be bypassed at runtime.

31

This seems like the beginning of a separate thread to me.

Setting that aside, I think whether you consider structs to be proper types or not will affect whether you think Elixir is strongly or weakly typed. The types provided by the BEAM are definitely strongly typed (int / float coercion notwithstanding). The question then is whether Elixir’s structs intend to be real types, or merely a convention, in the same way that records (tagged tuples) are.

2 Likes
32

I actually have an old blog post describing those if curious, as well as some pro’s and con’s:

For a multitude of reasons, including but not limited to:

  • Biggest reason! Catch whole varieties of bugs at compile-time, instead of in production some time down the road while breaking users interfaces or losing data.
  • Refactor far more easily since if you make a change then you know all places that you need to update to, no surprise suddenly wrong datatypes.
  • Code Generation based on types means substantially less code to type at times.
  • The compiler can generate significantly faster code.

Java is absolutely a very bad example of static typing, it’s OOP style (not all OOP systems are bad, but Java’s/C#'s/C++'s/etc… are exceptionally bad) basically shoehorns things into an Object tree, which is technically statically typed but everything is so virtually dispatched that it’s basically dynamic typing. That model without Java’s (admittedly impressive) JIT would be horribly slow, and it allows entire classes of bugs that the usual strong typing systems just wouldn’t allow at all.

Elixir is absolutely dynamically strongly typed.

3 Likes