<div dir="ltr">On Tue, Oct 29, 2013 at 4:33 PM, Jesper Louis Andersen <span dir="ltr"><<a href="mailto:jesper.louis.andersen@gmail.com" target="_blank">jesper.louis.andersen@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div dir="ltr"><div class="gmail_extra"><div class="im"><br><div class="gmail_quote">On Tue, Oct 29, 2013 at 8:51 PM, Chris King <span dir="ltr"><<a href="mailto:colanderman@gmail.com" target="_blank">colanderman@gmail.com</a>></span> wrote:<br>


<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">No it's not.  Unless you define the input type as :- type order() :: eq | lt | gt.  Well, you can do the same thing with integers in Erlang: :- type order() :: -1 | 0 | 1.</blockquote>


</div><br></div>Depending on the type system, this is either possible or it is not. A type system based on success types can allow it, but then you have the problem that it isn't a traditional type system.</div></div>
</blockquote><div><br></div><div>I know.  I used OCaml for years before coming to Erlang.  A smattering of Coq too.</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div dir="ltr"><div class="gmail_extra">If you want a traditional static type system, then I'd bet that it won't be trivial to handle -1 | 0 | 1 as a subtype of the integers.</div></div></blockquote><div><br></div>
<div>OCaml manages it for atoms with polymorphic variant types.  Checking integer subtypes in the presence of arithmetic is more difficult, yes, but that's not an issue here (both because (a) we're not doing arithmetic and (b) Dialyzer's type engine is complete but not sound).</div>
<div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div class="gmail_extra">I really dislike not using atoms for this. Intuitively and because of the inherent type complexity (yes, I have a bias here).</div>
</div></blockquote><div><br></div><div>Having migrated from the ML camp after living in it for a decade, I think the perceived complexity is an artifact of the HM type system.</div></div>