<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Sat, Apr 26, 2014 at 9:28 PM, David Fox <span dir="ltr"><<a href="mailto:dsf@seereason.com" target="_blank">dsf@seereason.com</a>></span> wrote:<br>



<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div class="gmail_extra"><div class="gmail_quote"><div>On Thu, Apr 24, 2014 at 10:27 AM, Kyle Murphy <span dir="ltr"><<a href="mailto:orclev@gmail.com" target="_blank">orclev@gmail.com</a>></span> wrote:<br>




<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">It's an interesting feature, and nice if you want that sort of thing, but not something I'd personally want to see as the default. Deviating from the standard ASCII set of characters is just too much of a hurdle to usability of the language.</div>




</blockquote><div><br></div></div><div>On the other hand, maybe if its good enough for the entire field of Mathematics since forever there might be some benefit in it for us. </div></div></div></div>
</blockquote></div><br>Chris spoke of his choice of Idris over Agda related to not going overboard with unicode. The FAQ he linked to has this to say:<br><br clear="all">| And I'm sure that in a few years time things will be different and 
software will <br>| cope better and it will make sense to revisit this.
For now, however, I would <br>| prefer not to allow arbitrary unicode symbols 
in operators.<br><br></div><div class="gmail_extra"><br></div><div class="gmail_extra">1. I'd like to underscore the 'arbitrary'.  Why is ASCII any less arbitrary -- apart from an increasingly irrelevant historical accident -- than Arabic, Bengali, Cyrillic, Deseret? [Hint: Whats the A in ASCII?]  By contrast math may at least have some pretensions to universality?<br>

</div><div class="gmail_extra">

<br></div><div class="gmail_extra">2. Maybe its a good time now to 'revisit'?  Otherwise like klunky-qwerty, it may happen that when the technological justifications for an inefficient choice are long gone, social inertia will prevent any useful change.<br>



<br><br><div class="gmail_extra"><div class="gmail_quote">On Sun, Apr 27, 2014 at 3:00 PM, Ben Franksen <span dir="ltr"><<a href="mailto:ben.franksen@online.de" target="_blank">ben.franksen@online.de</a>></span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">The main problem with special Unicode characters, as I see it, is that it is<br>
no longer possible to distinguish characters unambiguously just by looking<br>
at them. Apart from questions of maintainability, this is also a potential<br>
security problem: it enables an attacker to slip in malicious code simply by<br>
importing a module whose name looks like a well known safe module. In a big<br>
and complex piece of software, such an attack might not be spotted for some<br>
time.<br>
</blockquote></div><br></div><div class="gmail_extra">Bang on!<br><br></div><div class="gmail_extra">However the Pandora-box is already open and the creepy-crawlies are all over us. <br><br>Witness:<br><br><span style="font-family:courier new,monospace">GHCi, version 7.6.3: <a href="http://www.haskell.org/ghc/">http://www.haskell.org/ghc/</a>  :? for help<br>

Loading package ghc-prim ... linking ... done.<br>Loading package integer-gmp ... linking ... done.<br>Loading package base ... linking ... done.<br>Prelude> let а = 1<br>Prelude> a<br><interactive>:11:1: Not in scope: `a'<br>

Prelude> </span><br><br></div><div class="gmail_extra">In case you cant see it the two a's are different unicode characters:<br>CYRILLIC SMALL LETTER A<br></div><div class="gmail_extra">vs<br>LATIN SMALL LETTER A<br>

<br></div><div class="gmail_extra"></div>Regards<br>Rusi<br></div><div class="gmail_extra"><br>
</div></div>