[erlang-questions] Maps branch and disclaimers

[Jesper Louis Andersen]

On Thu, Oct 31, 2013 at 11:58 AM, Anthony Ramine <n.oxyde@REDACTED> wrote:

> At least that's how I see success typing as opposed to more traditional
> type systems.


The original paper has the description which is precise, but from my memory:

Suppose we have a function f. We notate

f : A -> B

as a success type iff whenever f terminates with a result of type B, then
the input must have been of type A.

Corollary: we can always say f : any() -> any(). Since if the function
terminates with any type, then we have indeed given it any value as input.
The same goes for a widening into atom() as you describe.

The goal of these annotations is to look for things which are impossible.
That is, we look for parameters passed to functions which does not match
the inferred spec. By the definition, this leads to code which will not
terminate normally and this code is often a basis for problems. It also
forms the basis for "The Dialyzer is never wrong". Because if it cannot
prove that the code will not terminate, it picks the conservative stance
that the programmer is right. Traditional type systems pick the stance that
the programmer is wrong and that the constructed term is not valid in the
programming language.

-- 
J.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20131031/9ba99457/attachment.htm>