<div dir="ltr"><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">On Mon, Jul 23, 2018 at 3:32 PM Dmitry Belyaev <<a href="mailto:be.dmitry@gmail.com">be.dmitry@gmail.com</a>> wrote:<br></div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div>How does it mess with types? The andalso and orelse operators should only care about the type of the first operand and it always is boolean.<br>
<br></div></blockquote><div><br></div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default">​Assume a GADT or dependently typed language. Then we have something like (forgive me the rust on the Agdaish notation used here):</div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default"><br></div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default">data Ty where</div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default">  Bool : Ty</div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default">  Int : Ty</div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default"><br></div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default">data Expr (t : Ty) : Set where</div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default">  andAlso : Expr Bool -> Expr Bool -> Expr Bool</div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default">  orElse : Expr Bool -> Expr Bool -> Expr Bool</div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default">  ...</div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default"><br></div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default">​and this is the normal canonical definition most statically typed languages use. You propose</div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default"><br></div><div style="font-family:arial,helvetica,sans-serif" class="gmail_default"><div style="" class="gmail_default">data Expr (t : Ty) : Set where</div><div style="" class="gmail_default">  andAlso : Expr Bool -> Expr t -> Expr ?</div><div style="" class="gmail_default">  orElse : Expr Bool -> Expr t -> Expr ?</div><div style="" class="gmail_default">  ...</div><div style="" class="gmail_default"><br></div><div style="" class="gmail_default">but the complication is that you have to be able to tell the system what the '?' should be. It is some union type over either Bool or t for any type t, but this easily complicates the type rules of the language. This is why I say it is a "mess". You might come up with a solution, but that solution will usually lead to an acceptance of a larger body of programs in which some of the programs will be weaker from a type perspective. Or it will lead to programs which has to do more runtime checking which are slower programs.</div><div style="" class="gmail_default"><br></div><div style="" class="gmail_default">Finally, in a dynamically typed language like Erlang, you indeed can give it a somewhat meaningful result by your proposal. But my view, as it often does, comes from 15 years of statically typed programming in Standard ML, OCaml and Haskell.<br></div><br></div><br></div></div>