That’s true for basic types but pretty much a nightmare for everything else. I can easily assert that something is a list. It is expensive to assert that something is a list of only As and Bs. Other times it is just plain impossible (guarantee that X is a stream capable of emitting only Y). Or assert module Z coming from runtime implements a certain behaviour or protocol.
josevalim
Creator of Elixir
OvermindDL1
That would be assuming recursiveness, rather it should be dynamic fully internally, so a list would only contain a list of dynamics, each of those you’d test out (would would be very simple if they only expect one thing). Typing to a full resolved type is one of those things I keep saying is not efficient or good to do on dynamic/typed interaction boundaries. ALL integration points should be entirely dynamic typed, thus in OCaml’ize something like:
let sum_ints bb =
let open BeamTypes in
match bb with
| List lst ->
lst |> List.fold_left 0 (fun acc v-> match v with
| Integer i -> i+acc
(* See below *)
)
(* Passing in an unhandled type will crash at runtime in OCaml so I will leave it,
though you also get a compile warning...
*)
Thus Every-Single-Dynamic-Location has to be matched out only to the BeamTypes types, so a BeamTypes.List gets you a list of more beamtypes. This is really the only safe way to do it on something like the BEAM VM. You can of course make some kind of macro (or in OCaml terms, a PPX) that generates conversion and check functions if you don’t mind the runtime checking cost, but it’s not any more expensive then checking them in the BEAM as well, and if you just handle a single type each, like in the above example, then the codegen can just treat it like it straight anyway without any checks if it shows the usage confirms the type that it will be (I.E. that it would crash if invalid type). Or the user could define a default case and handle the errors any way they want (which would always put in a guard test at codegen).
Only atomically built units of modules could be fully properly typed. Message boundaries and so forth absolutely could not be. And manually hot-code loading non-atomic module-sections is of course ‘undefined behaviour’ (but a rare case even nowadays). ^.^
1
josevalim
Creator of Elixir
Right, that would require the type-safe code to do conversions and inline code until the traversal point, which violates the modules boundaries. Or am I missing something? To me violating the module semantics is a no-no.
0
OvermindDL1
Rather on bounds that are designed to be called by untyped code or is calling out to (and getting back) untyped values then they’d need to be matched on by the author of the code, this requires the author to do it with whatever efficiency they deem best for that location. If untyped code calls typed code with a value that does not match the typespec then it is of course undefined behaviour (crash whenever it gets used in an unexpected way). 
I.E. you only get the type safety when calling from typed to typed code, otherwise it’s essentially the same as normal elixir/erlang calling normal elixir/erlang. It enhances usage, but does not require it (since the beam doesn’t enforce it anyway, meaning don’t try to hide it like alpaca is doing, instead embrace it).
0
josevalim
Creator of Elixir
Sure, you could do that, but it is also a trade-off you have to make and some people will be genuinely surprised by not type checking at the boundaries.
2
OvermindDL1
Could always be configurable as well. Perhaps a unique internal call that does not test types if not necessary, and a public interface that does test them (thus incurring the cost only when necessary) that way you have both (though it duplicates the public function count in modules that are marked as such).
0
damncabbage
delete(['a], 'a) :: 'a
This is
delete(list(a), a) :: list(a) when a: varin elixir specs.
As far as I can tell, unfortunately, it’s not. The type “variables” don’t seem to ensure consistency between uses, leading to cases like the example below, where declaring a variable swap has no effect:
(This program crashes every time you call example/1, and Dialyzer gives it the thumbs-up even with stricter options flipped on.)
@spec flip(a, b) :: {b, a} when a: var, b: var
def flip(a, b) do
{a, b}
end
def example do
case flip(123, "def") do
{string, number} ->
IO.inspect(string)
number + 77
end
end
2
OvermindDL1
That’s because your spec is wrong. When you define a spec then dialyzer assumes that you are correct and won’t check the body of the function with the spec, in this case your body is wrong. You are more wanting a unification typer but dialyzer is a positive typer, very different things with different uses.
0
damncabbage
That’s because your spec is wrong.
Okay. I fixed the spec, as far as I can tell. It still always crashes when you call Hello.example.
@spec flip(a, b) :: {b, a} when a: var, b: var
def flip(a, b) do
{b, a} # Fixed this line; this function does what it says it does now.
end
def example do
case flip(123, "def") do
{string, number} ->
IO.inspect(string) # => "def"
IO.inspect(number) # => 123
string + 77 # always crashes
end
end
As far as I can tell, there’s no continuity between the two uses of a (or the two uses of b) in flip’s spec.
(I would love for this to be like delete(['a], 'a) :: 'a, but I honestly don’t know how to make this work, if it’s even possible with Dialyzer as it is. Suggestions very welcome.)
0
jeremyjh
This is correct. dialyzer does not unify type variables. Type variables are only really useful for specifying constraints via a when clause, and do not provide most of what people expect generics to do for them.
This is mentioned in this answer by one of the developers of dialyzer.
4