Typed Elixir

Just so you know, the problem Philip Wadler found when he tried to type erlang :

  • message
  • pid and process in particular self ()

The other question is… how do you deal with distributed message. You can get a message from a node that do not follow the comtract you assigned. So your type checking is useless in that case…

1 Like

Another thing that makes typing erlang/elixir really difficult is dynamic loading of modules. The function you’re using may actually not exist yet when you’re writing it, the module may be loaded later. Not to mention hot upgrades that completely mess stuff up.

3 Likes

The papers on dialyzer and success types include a lot of the pitfalls in trying to build an ML type system for Erlang: https://it.uu.se/research/group/hipe/papers/succ_types.pdf.

@OvermindDL1 Have you looked into multi-party session types? http://groups.inf.ed.ac.uk/abcd/index.html. That research seems like it could be a promising way forward.

1 Like

Already have a test library for that (in OCaml). A quick overview:
Message is just typed as Erlang.t, which is a blackbox unknown erlang type.
Pid is an Erlang.Pid.t, which is also a blackbox erlang type that you know is a pid, you can do something like Erlang.Pid.send somePid someMessage as an example.

The Erlang module would have testing like Erlang.is_int something as well as reifiers like Erlang.reify something that can be used like:

let open Erlang in
match reify something with
| Int i -> doSomethingWithInt i
| Binary b -> doSomethingWithBinary b
| Tuple [ Int i; Float f ] -> doSomethingWithIntAndFloat i f
| _ -> doSomethingAsDefaultCase

Or so forth, and those are only the primitives, can build up better matchers on top of that pretty easily (including dynamically creating arbitrary depth decoders based on types of, say, a receive call). This is pretty easy to do in OCaml and I already have this part done (as I was playing around to see how easy it is). I was planning something similar in this once I figured up a good API but I do think I’d end up having to enforce a new language or so…

Eyup, this would only typecheck at compile-time, at runtime it would all still be elixir and you gotta deal with the changes you make, if you do non-atomic hot code swapping and you change your API, then just like in normal erlang be prepared to deal with the consequences (and exceptions, :EXIT’s, etc…). This is less to ensure safety at runtime (erlang does that pretty well already) and more to help ensure that I do not screw up at compile-time by passing things in the wrong order or so, that is my primary use of statically typed languages. Trying to statically type it all at runtime is a fools errand and not something I would even attempt except for occasionally throwing in is_int's or so in when clauses. I want something to help me code, not ensure safety at runtime (as stated, erlang does that well enough itself via OTP).

Yeah I ran across that long ago, and is one of the reasons I started by thinking of a way to black-box a type like my above Erlang.t type, that way I can always fall back to that and force the user (I.E. me) to do proper tests to reify it and use what they want and handle the cases where they get what they do not want.

Hmm, that is not something I’ve come across, seems like a decoder of the Erlang.t type could fit within that, it either succeeds or fails given a pattern, which is defined manually if you wish like:

let myDecoder =
  let open Erlang.Decoders in
  Tuple
    [ Literal.Atom `Something
    ; Atom
    ; Validate Int (fun i -> i >= 0 && i < 10)
    ; Binary
    ]

(* Use it like: *)
match Erlang.Decoders.decode myDecoder something with
| Some (_, someAtom, someInt, someBinary) -> doSomething someAtom someInt someBinary
| Error _e -> ()

Which in Elixir would be the same as:

case something do
  (:Something, someAtom, someInt, someBinary) when
    is_atom(someAtom) and
    is_int(someInt) and
    is_binary(someBinary) and
    someInt>=0 and someInt<10 ->
      doSomething(someAtom, someInt, someBinary)
  _ -> nil
end

Thus modules can define decoders (and with mapping and such can transform the data as well during decoding) that can be used elsewhere to parse data. If I made an ocaml backend (I would so love to get the time for that!) then reify could reify a whole tree so you could match on something like this as well:

let rec blah something v in
  let open Erlang in
  match Erlang.reify something with
  | Tuple [ Atom `Something; Int i ] -> i + v
  | List [] -> v
  | List (Int i :: rest) when i<10 -> blah rest (i + v)
  | _ -> v

Which in Elixir would be:

def blah something v do
  case something do
    (:Something, i) when is_int(i) -> i + v
    [] -> v
    [i | rest] when is_int(i) and i<10 -> blah(rest, v + i)
  end
end

In both cases it is just a function that can take a tuple of `(:Something, 42) or a list of integers that it will then sum up each element if the element is less than 10 (OCaml has ‘when’ like in Erlang/Elixir in its pattern matching too).

I’m pretty sure I’ve worked around each usual issue that would happen by having a statically typed language compile to Erlang/Elixir, although it would be slightly more wordy what with things like the Erlang.reify work and such. But for something like receive you can pass in a decoder (that can decode a variety of types, I modeled it on Elm’s JSON Decoders/Encoders) to get back a specific type or could just call it with an identity to get back the next message as an opaque type that you can then match on to unconditionally remove from the mailbox anyway.

An update after months!

So far these all work as expected, it uses types and spec’s when it can, and infer’s it otherwise when it cannot (or complains):

iex> use TypedElixir
TypedElixir

iex> defmodulet TypedTest_Empty do
...> end
{:module, TypedTest_Empty,
 <<70, 79, 82, 49, 0, 0, 3, 244, 66, 69, 65, 77, 69, 120, 68, 99, 0, 0, 0, 94,
   131, 104, 2, 100, 0, 14, 101, 108, 105, 120, 105, 114, 95, 100, 111, 99, 115,
   95, 118, 49, 108, 0, 0, 0, 4, 104, 2, ...>>, nil}

iex> defmodulet TypedTest_Typed_Simple do
...>   @spec simple() :: nil
...>   def simple(), do: nil
...> end
{:module, TypedTest_Typed_Simple,
 <<70, 79, 82, 49, 0, 0, 4, 196, 66, 69, 65, 77, 69, 120, 68, 99, 0, 0, 0, 129,
   131, 104, 2, 100, 0, 14, 101, 108, 105, 120, 105, 114, 95, 100, 111, 99, 115,
   95, 118, 49, 108, 0, 0, 0, 4, 104, 2, ...>>, {:simple, 0}}
iex> TypedTest_Typed_Simple.simple()
nil

iex> defmodulet TypedTest_Untyped_Simple do
...>   def simple(), do: nil
...> end
{:module, TypedTest_Untyped_Simple,
 <<70, 79, 82, 49, 0, 0, 4, 176, 66, 69, 65, 77, 69, 120, 68, 99, 0, 0, 0, 129,
   131, 104, 2, 100, 0, 14, 101, 108, 105, 120, 105, 114, 95, 100, 111, 99, 115,
   95, 118, 49, 108, 0, 0, 0, 4, 104, 2, ...>>, {:simple, 0}}
iex> TypedTest_Untyped_Simple.simple()
nil

iex> defmodulet TypedTest_Untyped_Recursive_Simple_BAD_NoSet do
...>   def simple(), do: simple()
...>   def willFail() do
...>     x = simple()
...>   end
...> end
** (throw) {:INVALID_ASSIGNMENT_NOT_ALLOWED, :no_return}
    (typed_elixir) lib/typed_elixir.ex:232: TypedElixir.type_check_expression/3
    (typed_elixir) lib/typed_elixir.ex:198: TypedElixir.type_check_def_body/3
    (typed_elixir) lib/typed_elixir.ex:121: TypedElixir.type_check_body/3
    (typed_elixir) lib/typed_elixir.ex:104: anonymous fn/3 in TypedElixir.typecheck_module/4
          (elixir) lib/enum.ex:1755: Enum."-reduce/3-lists^foldl/2-0-"/3
    (typed_elixir) lib/typed_elixir.ex:103: TypedElixir.typecheck_module/4
    (typed_elixir) expanding macro: TypedElixir.defmodulet/2
                   iex:5: (file)
iex> # Cannot set the return value of a function that never returns...
nil

iex> # The extra type is to give a name to the type in simple, so the input and output become the same type.
nil
iex> # If the spec was `simple(any()) :: any()` then you could not state that the output type is based on the input type.
nil
iex> defmodulet TypedTest_Typed_Identity do
...>   @type identity_type :: any()
...>   @spec identity(identity_type) :: identity_type
...>   def identity(x), do: x
...> end
{:module, TypedTest_Typed_Identity,
 <<70, 79, 82, 49, 0, 0, 5, 48, 66, 69, 65, 77, 69, 120, 68, 99, 0, 0, 0, 191,
   131, 104, 2, 100, 0, 14, 101, 108, 105, 120, 105, 114, 95, 100, 111, 99, 115,
   95, 118, 49, 108, 0, 0, 0, 4, 104, 2, ...>>, {:identity, 1}}
iex> TypedTest_Typed_Identity.identity(42)
42
iex>
nil

iex> defmodulet TypedTest_Typed_Identity_badtype do
...>   @type identity_type :: any()
...>   @spec identity(identity_type) :: identity_type
...>   def identity(_x), do: nil
...> end
** (throw) {:NO_TYPE_RESOLUTION, %TypedElixir.Type.Const{const: :atom, meta: %{values: [nil]}}, %TypedElixir.Type.Ptr.Generic{id: 0, named: true}}
    (typed_elixir) lib/typed_elixir.ex:514: TypedElixir.resolve_types_nolinks/3
    (typed_elixir) lib/typed_elixir.ex:454: TypedElixir.resolve_types!/3
    (typed_elixir) lib/typed_elixir.ex:168: TypedElixir.resolve_fun_return_type_/4
    (typed_elixir) lib/typed_elixir.ex:146: TypedElixir.resolve_fun_return_type/4
    (typed_elixir) lib/typed_elixir.ex:127: TypedElixir.type_check_body/3
    (typed_elixir) lib/typed_elixir.ex:104: anonymous fn/3 in TypedElixir.typecheck_module/4
          (elixir) lib/enum.ex:1755: Enum."-reduce/3-lists^foldl/2-0-"/3
    (typed_elixir) lib/typed_elixir.ex:103: TypedElixir.typecheck_module/4
iex> # Since it is a named type the input and output must match
nil

iex> defmodulet TypedTest_Typed_Identity_AnyReturn do
...>   @spec identity(any()) :: any()
...>   def identity(_x), do: nil
...> end
{:module, TypedTest_Typed_Identity_AnyReturn,
 <<70, 79, 82, 49, 0, 0, 4, 248, 66, 69, 65, 77, 69, 120, 68, 99, 0, 0, 0, 152,
   131, 104, 2, 100, 0, 14, 101, 108, 105, 120, 105, 114, 95, 100, 111, 99, 115,
   95, 118, 49, 108, 0, 0, 0, 4, 104, 2, ...>>, {:identity, 1}}
iex> TypedTest_Typed_Identity_AnyReturn.identity(42)
nil
iex> # An unnamed `any()` means it can literally return anything, the input does not matter
nil

iex> defmodulet TypedTest_Untyped_Identity do
...>   def identity(x), do: x
...> end
{:module, TypedTest_Untyped_Identity,
 <<70, 79, 82, 49, 0, 0, 4, 204, 66, 69, 65, 77, 69, 120, 68, 99, 0, 0, 0, 149,
   131, 104, 2, 100, 0, 14, 101, 108, 105, 120, 105, 114, 95, 100, 111, 99, 115,
   95, 118, 49, 108, 0, 0, 0, 4, 104, 2, ...>>, {:identity, 1}}
iex> TypedTest_Untyped_Identity.identity(42)
42

iex> defmodulet TypedTest_Untyped_Identity_AnyReturn do
...>   def identity(_x), do: nil
...> end
{:module, TypedTest_Untyped_Identity_AnyReturn,
 <<70, 79, 82, 49, 0, 0, 4, 236, 66, 69, 65, 77, 69, 120, 68, 99, 0, 0, 0, 152,
   131, 104, 2, 100, 0, 14, 101, 108, 105, 120, 105, 114, 95, 100, 111, 99, 115,
   95, 118, 49, 108, 0, 0, 0, 4, 104, 2, ...>>, {:identity, 1}}
iex> TypedTest_Untyped_Identity_AnyReturn.identity(42)
nil
iex> # Since it is not typed it gets an inferred return value of `nil`
nil

iex> defmodulet TypedTest_Typed_Recursive_Counter do
...>   @spec counter(integer()) :: integer()
...>   def counter(x), do: counter(x)
...> end
{:module, TypedTest_Typed_Recursive_Counter,
 <<70, 79, 82, 49, 0, 0, 4, 248, 66, 69, 65, 77, 69, 120, 68, 99, 0, 0, 0, 148,
   131, 104, 2, 100, 0, 14, 101, 108, 105, 120, 105, 114, 95, 100, 111, 99, 115,
   95, 118, 49, 108, 0, 0, 0, 4, 104, 2, ...>>, {:counter, 1}}
iex> # Not calling it because infinite recursion...
nil

iex> defmodulet TypedTest_Untyped_Recursive_Counter do
...>   def counter(x), do: counter(x)
...> end
{:module, TypedTest_Untyped_Recursive_Counter,
 <<70, 79, 82, 49, 0, 0, 4, 224, 66, 69, 65, 77, 69, 120, 68, 99, 0, 0, 0, 148,
   131, 104, 2, 100, 0, 14, 101, 108, 105, 120, 105, 114, 95, 100, 111, 99, 115,
   95, 118, 49, 108, 0, 0, 0, 4, 104, 2, ...>>, {:counter, 1}}
iex> # Again, not calling it because infinite recursion...

iex> defmodulet TypedTest_Typed_Recursive_Counter_Bad do
...>   @spec counter(integer()) :: integer()
...>   def counter(x), do: counter(6.28)
...> end
** (throw) {:NO_TYPE_UNIFICATION, :NO_PATH, %TypedElixir.Type.Const{const: :integer, meta: %{}}, %TypedElixir.Type.Const{const: :float, meta: %{values: [6.28]}}}
    (typed_elixir) lib/typed_elixir.ex:567: TypedElixir.unify_types_nolinks/3
    (typed_elixir) lib/typed_elixir.ex:521: TypedElixir.unify_types!/3
          (elixir) lib/enum.ex:1229: Enum."-map/2-lists^map/1-0-"/2
    (typed_elixir) lib/typed_elixir.ex:250: TypedElixir.type_check_expression/3
    (typed_elixir) lib/typed_elixir.ex:201: TypedElixir.type_check_def_body/3
    (typed_elixir) lib/typed_elixir.ex:121: TypedElixir.type_check_body/3
    (typed_elixir) lib/typed_elixir.ex:104: anonymous fn/3 in TypedElixir.typecheck_module/4
          (elixir) lib/enum.ex:1755: Enum."-reduce/3-lists^foldl/2-0-"/3


iex> defmodulet TypedTest_Untyped_Recursive_Counter_RecallingDifferentType do
...>   def counter(_x), do: counter(6.28)
...> end
{:module, TypedTest_Untyped_Recursive_Counter_RecallingDifferentType,
 <<70, 79, 82, 49, 0, 0, 5, 56, 66, 69, 65, 77, 69, 120, 68, 99, 0, 0, 0, 151,
   131, 104, 2, 100, 0, 14, 101, 108, 105, 120, 105, 114, 95, 100, 111, 99, 115,
   95, 118, 49, 108, 0, 0, 0, 4, 104, 2, ...>>, {:counter, 1}}
iex> # Not calling this either, infinite recursion
nil

iex> defmodulet TypedTest_Typed_MultiFunc0 do
...>   @spec simple() :: nil
...>   def simple(), do: nil
...> 
...>   @type identity_type :: any()
...>   @spec identity(identity_type) :: identity_type
...>   def identity(x), do: x
...> 
...>   @spec call_simple(any()) :: any()
...>   def call_simple(_x), do: simple()
...> 
...>   @spec call_simple_constrain_to_nil(any()) :: nil
...>   def call_simple_constrain_to_nil(_x), do: simple()
...> 
...>   @spec call_simple_through_identity(any()) :: nil
...>   def call_simple_through_identity(_x), do: simple() |> identity()
...> end
{:module, TypedTest_Typed_MultiFunc0,
 <<70, 79, 82, 49, 0, 0, 7, 232, 66, 69, 65, 77, 69, 120, 68, 99, 0, 0, 1, 167,
   131, 104, 2, 100, 0, 14, 101, 108, 105, 120, 105, 114, 95, 100, 111, 99, 115,
   95, 118, 49, 108, 0, 0, 0, 4, 104, 2, ...>>,
 {:call_simple_through_identity, 1}}
iex> TypedTest_Typed_MultiFunc0.call_simple_through_identity(42)
nil
iex> TypedTest_Typed_MultiFunc0.call_simple(42)
nil
iex> TypedTest_Typed_MultiFunc0.identity(42)
42
iex> # call_simple_through_identity is properly typed with a return of nil as you notice
nil
11 Likes

Thanks for your work, it would be extremely great to elixir to have static type system!

2 Likes

Gradualizer is similar but it operates on the BEAM opcode level, so it both has more and less information in different ways. I can’t wait for a full release! :slight_smile:

2 Likes

So you gave up of your approach in favor of Gradualizer?

I really miss having a type system in Elixir. I know we have Dialyzer, but is not the same and is not straight forward to use.

2 Likes

I actually not miss a type system in Elixir. I absolutely hate having to work with Typescript at some work projects and wish I had Elixirs pattern matching. I guess it’s just personal preference. That said, if Elixir ever forced a type system on me, I would not use it anymore.

1 Like

Not really, I’d love to make a typed-elixir style system, I just don’t have time, at all… ^.^;

I entirely agree! A full and proper type system is not just for static type checking but for lots of other reasons as well, like code disambiguation, code generation based on types, etc… etc…

Typescript is… not really a great example of a type system, it’s awfully verbose. :wink:

2 Likes

I completely agree with you… It enables more confidence in how we code, less tests, and less code to check for stuff that should be work of the compiler or runtime.

I am looking forward to see how #gleam by @lpil will develop :slight_smile:

4 Likes

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

3 Likes

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.

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

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?

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: https://fsharpforfunandprofit.com/posts/designing-with-types-making-illegal-states-unrepresentable/

6 Likes

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

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.

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

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