<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I feel that this is similar to expressing value constraints in the type system, e.g. ranges or squareness of matrixes. Yes it can be done in Haskell's type system, yes it does typecheck beautifully, but the type declarations behind these kinds of feats will just make any ordinary programmer go MEGO. Even the bright ones.<br>
I conclude that the type system isn't the right place for that kind of checking. To be understandable, such constraints need to be expressed as boolean assertions, not as some inductive construct. YMMV</blockquote><div><br></div><div>Two words: refinement types.</div><div><br></div><div>Best regards,</div><div>Marcin Mrotek </div></div></div></div>