OvermindDL1
Typed Elixir
Just got an idea on how we could get a strongly typed elixir ‘now’. Imagine this:
import TypedElixir
defmodulet TypedTest do
@moduledoc false
@spec hello() :: String.t
def hello, do: "world"
end
Or whatever for a name instead of defmodulet (I’m horrible with names) right now it is just a typed version of defmodule. It could start by enforcing @specs, then another pass to ensure that the inner function calls also follow the spec of the function by checking the specs of the other calls. Any calls that are not @specd outside of the enforced defmodulet bounds would require some type of @spec elsewhere. You could also @spec variables inside a function if so wished (better debugging to make sure you are passing things around right), but otherwise make sure that they are used properly in the function. If your spec does not match the def/defp usage then it would error, giving both what it detects it should be and what it is.
Even if I have to @spec everything in my program, I would so far beyond love getting compiler errors for mis-using types. Absolutely requiring @spec on def/defp when within a defmodulet makes type inference within the function significantly easier to reason about both for the coder and for the TypedElixir library.
It would indeed by quite nice if such type checking was added to the base defmodule, we could even pass in a @strict_types as a module attribute or so to enforce the above (require accurate @specs, not too generic, etc… etc…) but otherwise backwards compatible to now but with occasional helper messages at compile-time like This will always fail as you cannot add an integer and a string as these bindings will always be an integer and a string or so. A default compile would not cross-module type-check unless a special flag would be added or @strict_types were specified or so, which would then cause the compiler to load the other modules to acquire their typespecs, which could increase compiling time admittedly, but only one level deep may not be noticable.
My motivation for this is 95% of my bugs in Elixir/Erlang are due to using types wrong, like I may slightly change a tuple format somewhere but do not update it elsewhere and dialyzer does not catch it because the prior library state was in its cache that I then need to rebuild, in addition to dialyzer can take a long time to run. And honestly I just do not want an incorrect program to compile at all, I want it to be noisy and fail at compile-time, not run-time. Even a little bit of extra checking then would save so much pain.
Either-way, I made a TypedElixir library of the above, only thing it does so far is check that @specs exist on each def/defp as I play around with it (literally mix new’d it <5 minutes before this post), does not expand macros first or anything yet (should probably be next step). I’m curious on ideas on if this is a good idea or if I should not bother with the effort?
EDIT0: The expansion and some clean-up done, still only checking that @specs exist, nothing else yet…
Most Liked
OvermindDL1
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
OvermindDL1
That is the challenge, I am curious if it is even possible in Elixir. So unless someone finds a case that is truly beyond difficult or impossible, I may work on it little by little over time. 
Oh, and in that case with receive, I’d try to throw some error like (in the optimal case):
Function: Module.foo
Location: file.ex:76
Must return a type of: string
However it returns a type of: any()
Suggestion: Change or add a case from receive that adds a `when is_binary` condition
Or something like that. I want to be forced to put typing on anything and everything that is ambiguous, that is how you catch a lot of bugs.
OvermindDL1
Been playing with more, slowly building a DHM inference engine with dependent types (mostly a learning exercise), not working yet but would be nice to get something like this:
defmodule Testing do
@spec div(number, (d is number if d != 0)) :: number
def div(x, y), do: x / y
end
Not my preferred syntax but the Elixir parser is unforgiving for what I would prefer (without resorting to strings, blehg). This would define a Testing.div/2 function that accepts any number in its first argument, any number that is not 0 in its second, and can return any number. Basically if you tried to do something like:
case Integer.parse(getInputFromUser()) do
{i, ""} -> Testing.div(40, i) # Boom
_ -> return nil
end
Then on the line with the Boom comment it would fail to compile due to unmatched constraint or so, you would have to do something like this instead:
case Int.parse(getInputFromUser()) do
{i, ""} when i != 0 -> Testing.div(40, i) # Boom
_ -> return 0
end
Or something that would actively refine the constraints of i to not include 0.
I doubt I will finish this, I think I’d be more apt to write an OCaml backend to Elixir, but this is still a fun very-slow-moving-project. ^.^
EDIT: Yeesh, this was two months later? I really do have about no time… Wish I could get paid to do this. >.>
Popular in Discussions
Other popular topics
Latest on Elixir Forum
Sponsor Spotlight
Develop your skills with books, videos, and courses.
Categories:
Sub Categories:
Forums
Popular Tags
- #ecto
- #liveview
- #troubleshooting
- #learning-elixir
- #deployment
- #library
- #erlang
- #testing
- #genserver
- #mix
- #absinthe
- #remote-other
- #otp
- #plug
- #how-to-question
- #macros
- #postgres
- #channels
- #elixirconf
- #exunit
- #discussion
- #code-sync
- #javascript
- #podcasts
- #onsite
- #dialyzer
- #docker
- #authentication
- #umbrella
- #full-time-contract
- #podcasts-by-brainlid
- #ecto-query
- #elixir-ls
- #phoenix_html
- #iex
- #blog-post
- #graphql
- #genstage
- #ai
- #websockets
- #supervisor
- #elixirconf-us
- #advent-of-code
- #distillery
- #processes
- #forms
- #api
- #metaprogramming
- #security
- #hex
Our Sponsors
Build Elixir applications with speed and confidence.
Supporting innovation across the BEAM ecosystem.
We build reliable cloud platforms for business-critical systems.
Catch errors, track performance, monitor hosts and more.
Error tracking for Elixir devs who love to ship. Start your free account.
Practical resources that improve the lives of professional developers.
Producing high quality Elixir screencasts since 2017.
The deployment platform built for Elixir: PaaS ease, VPS control.
The team behind Membrane, Popcorn, LiveDebugger. Available for hire.
Courses that'll move you from confusion to "Aha, now I get it!"