Would it be possible through a module attribute or macro to have the compiler insert additional pattern matching / guard clauses to check parameters and return values respect the typespecs at runtime?
Something like a combination of dialyzer and expat would be great.
Yes, I tried, it seems :underspecs not affect at all to my example
Dialyzer with flag :overspecs generated weird warning not related to problem in example
lib/hello.ex:1: Type specification 'Elixir.Hello':'__info__'('attributes' | 'compile' | 'functions' | 'macros' | 'md5' | 'module' | 'deprecated') -> atom() | [{atom(),any()} | {atom(),byte(),integer()}] is a subtype of the success typing: 'Elixir.Hello':'__info__'('attributes' | 'compile' | 'deprecated' | 'functions' | 'macros' | 'md5' | 'module') -> any()
done (warnings were emitted)
I also tried other flags, it not resolves the problem
I had a similar question in this post and got a nice answer from @peerreynders.
You could do
@type good_hello() :: map()
@type bad_hello() :: map()
@spec hello(integer()) :: good_hello() | bad_hello()
def hello(int) do
case int do
1 -> good()
_ -> bad()
end
end
@spec good() :: good_hello()
def good(), do: %{hello: "world"}
@spec bad() :: bad_hello()
def bad(), do: :wtf
This way You would catch spec error with dialyzer.
Thanks, so short answer is to not use literals for structures, maps, lists and other terms, but use functional wrapper with its own typespec which will return term as expression without any branching inside?
I was trying to port example from [Functional Programming] Domain Modeling Made Functional (Pragprog) (F#) to Elixir. Of course F# is not Elixir, but the example remains interesting.
Thanks, so short answer is to not use literals for structures, maps, lists and other terms, but use functional wrapper with its own typespec which will return term as expression without any branching inside?
Yes, and then compose into bigger types, and bigger functions. Maybe like this.
@type good_hello() :: map()
@type bad_hello() :: map()
@type any_hello() :: good_hello() | bad_hello()
@spec hello(integer()) :: any_hello()
Yes, probably it will work, but I think it looks creepy 
And of course if you will introduce new type and function every time you need branching - it will gain 3x amount of code, and will gain overhead regarding function calls in runtime
Personnally, I would have written this like that 
@spec hello(integer()) :: map()
def hello(1), do: %{hello: "world"}
def hello(_), do: :wtf
Conditional and branching are easily replaced by pattern matching
Yes, ofc I like pattern matching - it makes code shorter etc,
but it not resolves problem with typespecs and Dialyzer here - try to compile it and run checks, Dialyzer will be happy with it
Actually it does. 
@type my_dict(key, value) :: [{key, value}]
Iâd think you could?
@spec delete([t], t) :: [t]
Although Iâm unsure how well dialyzer checks that (wow the syntax highlighting is bad on ::)? But Iâm like 80% sure Dialyzer matches based on unbound names for handling passed in types.
Good thing the AST is so simple, just some primitive types, lists, 2-tuples, and 3-tuples.
/me wishes it were just 3-tuples and primitives-inside-special-3-tuples
There are ways though, and since each form of an AST node is distinct then it could be a headless sum type safely (or heads without internal named distinction, which is easy to do).
Ah yeah, the when might be necessary, unsure?
I donât. It is runtime based, not entirely compile-time, which is point defeating.
Yep yep, it is a great positive typer, it was not designed to be an actual complete typing system.
Itâs not too bad actually, especially if there is a âdynamicâ type that must be matched out for use in statically-strongly typed sections (deft as a typed def, or something that is module-wide?), then you can pretty well incrementally improve it knowing that the only unchecked areas are areas that are not typed.
At least until you define such an Option.t type or so and baked in a few common patterns.
Not any more than current code already has to do, the dynamic->typed boundaries would still use matchers and guards to safely determine what it is, which is what you have to do anyway to determine the types of something. However inside the typed area then direct calls could be made that entirely bypass guards and other such checks for known paths.
Yeah I really wish Elixir started as a typed language, erlang being dynamically typed is one of the things Iâve hated most about it, only standing it because of dializer. Elixir started from the wrong side of typing even though it was made a-new still seemed entirely broken to meâŠ
Actually I think it was @vic that made a library or two along that path. ^.^
Yep, it definitely would, though that would add overhead that the static type checking means wouldnât need to exist anyway (proper static typing can remove a lot of checks and can generate a lot better code in a few areas).
Yeah overspecs are way too noisy because the quality of the specs in the overall engine and essentially all libraries are not made quite right in a lot of places (especially once you take macroâs in mind).
Like in a real full typing system! ^.^
Typespecs donât generate code though.
/me really wants to work more on the TypedElixir experiment⊠blehg lack of timeâŠ
Yes, but in an HM typesystem you need named constructors to write your macro, even if the internal implementation strips them⊠This is not a disaster, though, and you can work around it.
I donât think it is too creepy, one liner functions, more specs and types than code, andâŠ
⊠no local variables
@type good_hello() :: map()
@type bad_hello() :: map()
@type any_hello() :: good_hello() | bad_hello()
@spec hello(integer()) :: any_hello()
def hello(1), do: good()
def hello(_), do: bad()
@spec good() :: good_hello()
def good(), do: %{hello: "world"}
@spec bad() :: bad_hello()
def bad(), do: :wtf
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.
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). ^.^
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.
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).
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.
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).
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
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.
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.)
© Copyright Elixir Forum | Terms | Privacy & Cookies
