Typespecs: function types

Is there a way to define a function type and use it later in the specs? Something like

@type task :: fun(any) -> {:ok, pid} | {:error, term} # How?

later

@spec register(task) :: reference

1 Like
@type task :: (any -> {:ok, pid} | {:error, term})

maybe?

4 Likes

Or the general practice is to define the task type as an alias to fun() and use typedocs to describe what is expected from the task type.

3 Likes

Dialyzer (Dialyxir) doesn’t process typedocs - so being as specific as possible on the spec is inherently more useful.

3 Likes

Great, many thanks. I think the syntax is worth mentioning explicitly in
https://elixir-lang.org/getting-started/typespecs-and-behaviours.html

1 Like

That’s primarily a tutorial. The standard library documentation has more complete coverage.
Typespecs, i.e.

                                  ## Functions
  | (... -> type)                 # any arity, returns type
  | (() -> type)                  # 0-arity, returns type
  | (type1, type2 -> type)        # 2-arity, returns type
3 Likes

BTW, is there a way to specify the expected type of a named function when it is passed as module, atom, args as in, say, Task.async

1 Like

Yup, I had a quick look actually, but totally missed it. I think the syntax deserves a small section with a header “Function types” or something which should make it easier to find.

2 Likes

How would static analysis utilize that information given that the result type for await/2 and apply/3 is entirely dependent on information that is generated completely at runtime?

I guess you could wrap an apply in a function that has a specified result type in order to let Dialyzer know what you expect - but there are no guarantees and you would still need to inspect the result type at runtime and crash if your expectation isn’t met to catch the problem at the earliest possible time.

Remember that Dialyzer is only performs success typing - it will only alert you when it can prove that you are wrong - otherwise it assumes that you know what you are doing.

2 Likes

I split out the functions types in a separate section in typespec docs (PR) and would be happy to add a paragraph on the syntax in the Getting Started guide.

Well the module can be very well specified statically. In that case the static analysis can be done to the extent that the function’s result type does not depend on the argument types/arity. For instance for functions returning pids/ports the arguments might not be really relevant.

I can also see that, in principle, one could define module types by specifying the behaviours they implement. Is that wrong?

Typespecs are also useful for humans besides being useful for static analysis.

1 Like

My issue isn’t with the module. Static analysis would have to determine all the possible module()/atom() combinations that could arrive at an apply/3 call site to infer the resulting sum type. async/3 would have a similar issue exacerbated by the fact that it would have to correlate which asyncs can end up at each await/2.

Historically adding a static type system to Erlang failed because the typing of the interprocess communication types is non-trivial and async/3/await/2 involves interprocess communication.

1 Like

That is precisely why I think alpaca’s current method and so forth is flawed. All messages really have to be black-boxed, as you never know for sure what you will get.

2 Likes

One way to start might be to formulate typed channels that are conceptually superimposed onto the mailbox but then it would become necessary to attach a channel type to each PID so that send could validate the type of the sent message. However I imagine the real challenge would likely be the analysis of the dynamic process structure and resulting message flow - much less adding any type of inference to the whole thing.

1 Like

Yep, in OCaml I’d imagine something like:

match receive do
| (~Ok, value) -> Some value
| [] -> None
| [value] -> Some value
| _ -> None

Or whatever, you’d have to match out exactly what you want, and by HM the two ‘value’ types would be unified so they’d have to be the same whether in the ok tuple or in the list (even if it does resolve to a generic ‘anything’ type that could then be matched on further later).

2 Likes

Wow, really? It doesn’t expand them when processing the specs? I had no idea.

1 Like

Did you figure it out?

It really doesn’t sound right and would come as a huge shock to me.