The chief difficulties I am running into are:
1) How to do intersections on functions and maps (this is in the article):
f(integer) -> integer is not usable as f(any) -> integer
2) not all of the erlang bytecode instructions are well documented
3) I still haven't figured out how to deal with circular dependencies at the module level.
Erlang makes this easy in these ways:
1) compiled module structure is simple and the way branching works makes the mechanics of type inference trivial.
2) erlangs concurrency makes dealing with, for example in-module dependencies trivial
3) there are only a handful of types in erlang so, aside from functions, their subtyping relationships are very straightforward.
Elixir makes this easy in these ways:
1) Typechecking structs can be more straightforward than records.
2) Writing a composable type logic (mavis) is super easy with elixir's protocols
3) I built (and am refining) a very easy dsl that makes creating and testing logic for the beam opcodes less of a hair-tearing experience:
https://github.com/ityonemo/mavis_inference/blob/main/lib/ty...
1. I think you have to see typing as helpful information. Like:
-spec add(integer(), integer()) -> integer(). add(A, B) -> A + B.
Technically, nothing prevents add from accepting number() or float(). It's too much specification.
2. I was surprised how much there actually is but also disappointed that a lot of errors were in until OTP 23. Gradualizer also overrides some definitions [2]
3. Haven't encountered a problem with this yet with gradualizer, would need to test.
[1] https://github.com/josefs/Gradualizer [2] https://github.com/josefs/Gradualizer/blob/master/priv/prelu...
> I think you have to see typing as helpful information
Indeed. Selectrix will allow you to chain your inference with fallbacks, so, maybe the first level is a fast cache, second level is checking files for user overrides, third level is dialyzer specs, fourth level is inference.
I think it should also be possible to create an addon module with Mavis that lets you type inbound messages for GenServers, given a set of constraints (all possible calls and casts are present in the module itself as an API)
[0] it's a big problem that in elixir, Enumerable protocol destroys typing information, so I want to make an typing override for Enumerable an "example" typing override system.
Although not entirely the same Dialyzer always seemed to be strange and quirky in its design choices - in the same way other parts of Erlang syntax can be a bit odd sometimes. The kind of thing I assume inspired Elixir in the first place (although in general I like Erlang as a language, it’s small enough and my complaints are few - it just feels syntactically quirky sometimes).
But I never felt inspired to use Dialyzer largely for these reasons. Never seemed to “fit” the syntax entirely and made it quite ugly IMO.
Which is why I’m happy to see these modern attempts, they look much better.
Good luck with the project. It should be an excellent learning process regardless.
That is usually dealt with by distinguishing between interface and implementation (cf. dependency inversion principle), which should eliminate the circularity. Disclaimer: I know very little about Erlang and Elixir.
This the question that needs resolution:
f = (x) => (...) ? Foo : g(x)
g = (x) => (...) ? Bar : f(x)
Obviously the type of the result of f should be Foo | Bar but figuring that out is not trivial because there is a circular dependency.[1] https://gleam.run/news/gleam-v0.12-and-gleam-otp-v0.1-releas...
I'm glad someone is trying, though.
https://webcache.googleusercontent.com/search?q=cache:JkQRku...
You do have to get to grips with pattern matching and processes as objects being such core concepts, but I found that once I got it, it is wonderful.
% a good old list length counter
count(A=[_|_]) -> count(A, 0).
count([], C) -> C;
count([_|T], C) -> count(T, C+1).
What is the type of count/2? Arguably, it's "(list, any | number) -> any | number", which means that count/1 has type "list -> any | number". Well, that's bloody pointless, isn't it? What you probably want is "(list, any) -> any | (list, number) -> number" for count/2, so you could give count/1 its useful type "list -> number", but intersection function types are notoriously difficult to infer or typecheck, even with manual annotations. 1> c(test_count).
{ok,test_count}
2> test_count:count([], bang).
bangOutside of the famous builtin process model/BEAM (plus the subsequent ‘crash first’ style design of programs which adds resiliency) the pattern matching is what makes Erlang one of the best languages and the one thing I wish every new language copied.
You kinda get it in Haskell and Rust with the maybe style pattern matching. Rust in particular makes good use of it.
But it’s one thing I miss the most not writing Erlang/Elixir for a living... so far. It makes functions and data handling into these clean trees instead of conditionals (not to start a language flamewar but boo Golangs conditional obsession which seems to be the polar opposite in many ways for error handling, or at least it used to be I haven’t tried it recently).
There’s a lot to like and learn from in Erlang. Static typing will give it wider adoption IMO. And I’m happy to see so many developers working on it.
In Erlang you can define the following:
equal(X, X) -> true;
equal(_, _) -> false.
In Haskell, the following does not compile: equal x x = True
equal _ _ = False
instead, we need to write something like equal x y | x == y = True
| otherwise = False
A subtle difference, but in some cases the structural semantics really do make patterns a lot cleaner (shorter without sacrificing readability).
I think that this style of pattern-matching semantics is a consequence of Erlang's roots in Prolog, which works similarly (and not only checks for structural equivalence but even does unification when necessary).Discovered it last year and started using it. The refinement portion handles unions and guards very well. It's not perfect but I'm integrating it in our codebase with some interesting successes. I'm hoping more people use it on their codebase and can find any bugs they have with it so it can be improved further.