The papers on dialyzer and success types include a lot of the pitfalls in trying to build an ML type system for Erlang: Research groups – Department of Information Technology – Uppsala University.
@OvermindDL1 Have you looked into multi-party session types? From Data Types to Session Types: A Basis for Concurrency and Distribution. That research seems like it could be a promising way forward.
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
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! 
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.
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.
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. 
So… why is nobody talking about this two recently published papers on session types?: