<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Oct 31, 2013 at 11:58 AM, Anthony Ramine <span dir="ltr"><<a href="mailto:n.oxyde@gmail.com" target="_blank">n.oxyde@gmail.com</a>></span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">At least that's how I see success typing as opposed to more traditional type systems.</blockquote></div><br>The original paper has the description which is precise, but from my memory:</div>

<div class="gmail_extra"><br></div><div class="gmail_extra">Suppose we have a function f. We notate</div><div class="gmail_extra"><br></div><div class="gmail_extra">f : A -> B</div><div class="gmail_extra"><br></div><div class="gmail_extra">

as a success type iff whenever f terminates with a result of type B, then the input must have been of type A.</div><div class="gmail_extra"><br></div><div class="gmail_extra">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.</div>

<div class="gmail_extra"><br></div><div class="gmail_extra">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.</div>

<div class="gmail_extra"><br></div><div class="gmail_extra">-- <br>J.
</div></div>