> You may not change how you compose your programs<br>> overnight, but there *should* be a nagging feeling that all<br>> programming is on some level immoral. <br><br>Perhaps elaborating on this is tangential to the issue at hand, but I’d love to hear/read more behind this thought process. Could you elaborate?<br><div class="gmail_quote"><div dir="ltr">On Thu, 5 Jul 2018 at 09:05, Vanessa McHale <<a href="mailto:vanessa.mchale@iohk.io">vanessa.mchale@iohk.io</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
  
    
  
  <div text="#000000" bgcolor="#FFFFFF">
    I think the point is well worth thinking over and thinking about in
    the context of programming language design though it may not change
    the fact that I use if expressions in my programs.<br>
    <br>
    In the particular example they cite with plus, what happens is:<br>
    <br>
        A) We have a number<br>
        B) We use that number to get a boolean representing whether or
    not a proposition about that number holds<br>
        C) We use that boolean (remembering that it represents something
    about the number) to pick another number<br>
    <br>
    However, the second approach works as follows:<br>
    <br>
        A) We pattern match on the number, using something about its
    structure to pick another number.<br>
    <br>
    The value "true" or "false" tells you absolutely nothing about
    *what* it is testing. The author is not saying "well you might have
    forgotten which boolean is which and used it in the wrong place,"
    rather "we could do so much better by connecting the *process of
    proof* to the truth of a particular proposition." Because those are
    completely different things!<br>
    <br>
    The status quo is "only model theory matters, I'm going to ignore
    proof theory completely," and you shouldn't be satisfied with that!
    You may not change how you compose your programs overnight, but
    there *should* be a nagging feeling that all programming is on some
    level immoral. <br></div><div text="#000000" bgcolor="#FFFFFF">
    <br>
    <div class="m_-3161487018987884010moz-cite-prefix">On 07/05/2018 01:28 AM, PY wrote:<br>
    </div>
    <blockquote type="cite">
      
      <p>Hello, Cafe!</p>
      <p>There is an opinion that Bool type has problems. It's
        "dangerous", because it's not good to be used as flag for
        success/fail result. I read this post: <a class="m_-3161487018987884010moz-txt-link-freetext" href="https://existentialtype.wordpress.com/2011/03/15/boolean-blindness/" target="_blank">https://existentialtype.wordpress.com/2011/03/15/boolean-blindness/</a>
        and was shocked. How popular is such opinion? Is it true, that
        bool is "bad" type?</p>
      <p>As I understand arguments of the post, Bool is bad because: 1)
        you don't know what does True/False mean  2) after comparison
        you get bit (!) only but then you may need to  "recover" the
        comparing value which was "shrink" to bit already.</p>
      <p>Let's begin from 2. As I understand the author talks about one
        register computers ;) if he have to "recover" a value. But shown
        examples are in ML, where function arguments are bound to all
        function body, so you don't need to "recover" anything, what was
        bound as function argument or with "let". Sounds totally weird
        and more close to psychology than to CS :)</p>
      <p>Argument #1 is more interesting.</p>
      <blockquote>
        <p><tt><span style="color:rgb(51,51,51);font-size:12px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:left;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;display:inline!important;float:none">A
              Boolean,<span> </span></span></tt><tt><em style="color:rgb(51,51,51);font-size:12px;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:left;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial">b</em></tt><tt><span style="color:rgb(51,51,51);font-size:12px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:left;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;display:inline!important;float:none">, is
              either<span> </span></span></tt><tt><strong style="color:rgb(51,51,51);font-size:12px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;letter-spacing:normal;text-align:left;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial">true</strong></tt><tt><span style="color:rgb(51,51,51);font-size:12px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:left;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;display:inline!important;float:none">, or </span></tt><tt><strong style="color:rgb(51,51,51);font-size:12px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;letter-spacing:normal;text-align:left;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial">false</strong></tt><tt><span style="color:rgb(51,51,51);font-size:12px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:left;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;display:inline!important;float:none">;
              that’s it.  There is no<span> </span></span></tt><tt><em style="color:rgb(51,51,51);font-size:12px;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:left;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial">information</em></tt><tt><span style="color:rgb(51,51,51);font-size:12px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:left;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;display:inline!important;float:none"><span> </span>carried
              by a Boolean beyond its value, and that’s the rub.  As
              Conor McBride puts it, to make use of a Boolean you have
              to know its<span> </span></span></tt><tt><em style="color:rgb(51,51,51);font-size:12px;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:left;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial">provenance<span> </span></em></tt><tt><span style="color:rgb(51,51,51);font-size:12px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:left;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;display:inline!important;float:none">so
              that you can know what it<span> </span></span></tt><tt><em style="color:rgb(51,51,51);font-size:12px;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:left;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial">means.</em></tt></p>
      </blockquote>
      <p>Really, what does True/False mean? How to find semantic of
        True? It's very simple, because there is A) contract/interface
        which interprets True/False and also B) there is a help from
        science.</p>
      <p>A) There are a lot of languages (Unix shell, ML, Basic,
        Haskell, C/C++...) with short-circuit expressions. Ex.,</p>
      <blockquote><tt>e1 || e2</tt><tt><br>
        </tt><tt>e1 && e2</tt><tt><br>
        </tt><tt>e1 orelse e2</tt></blockquote>
      <p>where interface is described by its operations: ||, &&,
        orelse, etc and it has absolutely accurate and clear meaning:
        "||" executes e2 iff e1 <b>fails, was not success</b>.
        "&&" executes e2 iff e1 was succeeded. I don't use words
        "True" and "False". Because, in different languages marker of
        success/fail is different. For example, in Bash, the fail is any
        integer except 0. In Haskell fail is False. In C is 0... What
        does mean False (and True) is defined by contract/interface of
        short-circuit operations, related to boolean algebra. A rare
        case when type is bound with semantic! We read them literally
        (native English): e1 or-else e2!<br>
      </p>
      <p><b>This means that using of False to indicate success - is
          error! And no way to miss provenance/knowledge what True or
          False means.</b></p>
      <p>(the same: what does Right/False mean?)<br>
      </p>
      <p>B) The help from science. Math (and CS) has own history. And
        one of its mail-stones was birth of formal logic and then of
        Boolean algebra. CS implemented those in declarative languages
        (Prolog, for example). If we have some predicate in Prolog,
        "true" for that predicate means "it was achieved", as goal. If
        that predicate has side-effects, "true" means it was achieved,
        i.e. all its steps (side-effects) were successfully executed.
        Predicate write_text_to_file/2 is "true" when it wrote text to
        file. And no way to return False on success or to think about
        sacral sense of True/False :) And that sense traditionally is
        the same in all programming language. If you invert it, you deny
        contract, semantic and begin to use "inverted" logic :)</p>
      <p>We can repeat the same logic with 3.1415926.. What does it
        mean? Meaning, semantic is described, but contract/interface:
        this magic irrational was born from part of algebra, called
        trigonometry. And this algebra defines semantic of Pi, not
        programmer's usage of Pi, programming context, etc. True/False
        semantic is defining by its algebra: boolean. So, programmer
        should not change their semantic, am I right?</p>
      <p>So, my question is: is this post a april 1st trolling or author
        was serious? :)</p>
      <p>---</p>
      <p>Best regards, Paul<br>
      </p>
      <p><br>
      </p>
      <br>
      <fieldset class="m_-3161487018987884010mimeAttachmentHeader"></fieldset>
      <br>
      <pre>_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
<a class="m_-3161487018987884010moz-txt-link-freetext" href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a>
Only members subscribed via the mailman list are allowed to post.</pre>
    </blockquote>
  </div>

_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div>