[erlang-questions] Type specs expressivity

[Kostis Sagonas]

On 09/09/11 15:00, Olivier BOUDEVILLE wrote:
>
> I would have three small questions regarding what can be expressed with
> type specs:

These are all very good questions!  Perhaps we should make sure they 
find their way verbatim in an FAQ in dialyzer's website.

> - we can define immediate constants and even ranges for integer values
> (ex: '-spec f() -> 42.' or '-spec f() -> 0..42.'), but apparently we
> cannot do the same for floats? Is there any particular reason for that
> (besides the lack of meaning of exact comparisons for floating-point
> numbers), or maybe it is a planned enhancement?

Admittedly, the decision has been quite arbitrary. We first started with 
atoms as singleton types and then extended this capability to integers 
because they were many natural cases where this turned out handy (e.g. 
bits_in_word() :: 32 | 64). Then we added integer ranges and integer 
range analysis to the system. We've stopped there.

Call me unimaginative, but the only cases where we could see singleton 
floats as handy were constants like pi() :: 3.141592653589793, epsilon() 
and all their other Greek relatives ;) so we never bothered implementing 
singleton types for floats in the type system. But we can change that, 
easily I think. So, if you have a convincing example where you need 
singleton floats, I would love to hear about it, even off list and 
possibly put singleton floats on the list of planned extensions.

Aside: there is no support for singletons in binaries, bitstrings or 
strings either...

> - it is a still more minor point, but we are using a hashtable type in
> pure Erlang, which is implemented as a tuple containing buckets. The
> number of elements of the tuple is determined at run-time (depending on
> a targeted ideal load factor, based on the expected number of elements
> to be stored in the hashtable). We can define a type for bucket(), but
> for the hashtable is there any way of expressing a more precise
> declaration than '-opaque hashtable() :: tuple()', i.e. to tell that
> even if we do not know the size of the tuple, we know it will contain
> bucket() instances at each position?

Currently, there is no tuple(T) type where T is a type. Perhaps there 
should be one but I have to think more of the consequences here.

Incidentally, the opaque declaration all it does is to detect whether 
code *outside* the defining module (the module containing the 
declaration) somehow depends/checks the structure of the data structure 
that has been declared as opaque.

> - what is the recommended way of handling functions that may or may not
> throw exceptions? If otherwise returning a type T, should we use T |
> none() or T | no_return() as return type, or should we consider that
> type specs focus on actual return types under normal circumstances, and
> that exceptions are in "another dimension"? I suppose it is the latter
> option, but then one could imagine that type specs for functions could
> be enriched with exception specifications, for example to check whether
> a catch clause has any chance of being triggered at all?

Exceptions are in "another dimension" as you write. For a long time it 
has been on my TODO list to add a -throws attribute (perhaps as part of 
the spec declaration) so that functions can declare their explicitly 
thrown exceptions.

In any case, you should definitely NOT add none() or no_return() to the 
return type if the function has some other return type under normal 
circumstances. There is no harm but this none() or no_return() will 
simply be ignored by the analysis.

Note that in Erlang all functions that do not have any() as their input 
type T have an implicit none() in their return type (for calls with 
inputs that do not belong to T) so, in some sense, the none() is always 
there. I think that the proper way to specify exceptions is by explicit 
declarations in a -throws like attribute. Alas, currently such a 
declaration exists only in the Edoc language...

Kostis