Re: [Agda] Why does Data.Product have � for the type constructor?

[Peter Berry]

2008/5/10 Bengt Nordstrom <bengt at chalmers.se>:
> On my mac the symbol in question looks like a circle with a flying bird
> inside.

It should be a capital Greek sigma. Like this: ∑. The other "strange"
character should be a capital pi, like this: Π

> Either there is something wrong with my computer or there is a need for a
> lot of explanation why anyone would have bothered
> to find such a strange symbol for something which we already have at least 4
> other symbols for.

I guess that's an encoding problem. The OP is in ISO-2022-JP, a
Japanese encoding, which happens to contain Greek. Your email is in
Microsoft codepage 932, another Japanese encoding, which doesn't. This
email should be in UTF-8 (an 8-bit encoding of Unicode, which contains
basically everything, including both Japanese and Greek). Translating
between various encodings is hard to get right - probably you've found
a bug in Mail.app (or one of the libraries it uses).

Seems Gmail doesn't get it right either:

> On 10 maj 2008, at 10.21, Marcin Benke wrote:
>
>> 2008/5/9 Samuel Bronson <naesten at gmail.com>:
>>>
>>> Why does Data.Product have ㊥ for the type constructor? Wouldn't Π be
>>> more appropriate? I guess that might have other connotations,
>>> though... still, ㊥???

For some reason it's translating ∑ into the character ㊥, which is
Unicode U+32A5 CIRCLED IDEOGRAPH CENTRE (see
http://www.fileformat.info/info/unicode/char/32a5/index.htm - which I
suppose does look a bit like a circle with a flying bird inside,
though my fonts seem to be giving some kanji glyph instead), though it
displays that email properly... bizarre.

-- 
Peter Berry <pwberry at gmail.com>
Please avoid sending me Word or PowerPoint attachments.
See http://www.gnu.org/philosophy/no-word-attachments.html