* * *

Jul. 8th, 2017 03:50 pm
bamalip: (Default)
[personal profile] bamalip
хвалебные песни языку Идрис
https://news.ycombinator.com/item?id=14551330

UPD
http://docs.idris-lang.org/en/latest/faq/faq.html#will-there-be-support-for-unicode-characters-for-operators
неприязнь Брейди к юникоду выглядит либо личной идиосинкразией, либо даже ложной гордостью англосакса тем фактом, что в мире все якобы пользуются только латинским алфавитом. до определенной версии у них даже тип String не поддерживал юникод, что для 2000-х довольно странно. а уж эти отговорки по ссылке выглядят совершенно притянутыми за уши: якобы броузеры до сих пор плохо поддерживают юникод, лол. это при том, что даже инженерская Java с самого начала поддерживала юникод как в данных, так и в идентификаторах.
но пользователи все равно находят способы обойти авторские ограничения:
https://github.com/Heather/idris-unicode/blob/master/Control/Unicode.idr

Date: 2017-07-08 01:52 pm (UTC)
From: [personal profile] sassa_nf
юнікод в ідентифікаторах - зло, поки не придумали зручного способу їх вводити.

Date: 2017-07-08 05:11 pm (UTC)
From: [personal profile] sassa_nf
Та про агду мені теж відомо, через те й зауважую.

Математично, може, й красиво, але якби у всіх юнікодних символів був синонім, який би легко можна було взнати із вигляду символа, я б не заперечував. Скажімо, мені не болить ввести ∈ (наприклад), якщо я хочу, щоб виглядало естетично. Тут з назви зрозуміло, що саме мається на увазі. А от коли починається → чи ⇒ - от тут-то юнікод заважатиме, бо з вигляду стрілки ⇒ не можна сказати, як її пишуть. Це ж як китайські єрогліфи. ↝ ⇀ ⇏ взагалі назв не мають.
Edited Date: 2017-07-08 05:12 pm (UTC)

Date: 2017-07-09 03:36 pm (UTC)
From: [personal profile] sassa_nf
навіть не чув про ibus. Ось є: https://github.com/acevery/ibus-table/blob/master/tables/additional/latex.txt

Здається, таким чином можна додати, що хочеш?..

Date: 2017-07-09 04:25 am (UTC)
thedeemon: (Default)
From: [personal profile] thedeemon
В faq'e все правильно написано про причины. Для меня отсутствие необходимости возиться с юникодом - большой плюс идриса по сравнению с агдой.
И да, не везде все символы хорошо отображаются, например в линуксе я не вижу вот этого: 🍅 🍅 🍅, а в винде вижу. Не хотелось бы в исходниках такие проблемы иметь.

Date: 2017-07-10 05:11 am (UTC)
thedeemon: (Default)
From: [personal profile] thedeemon
Но сперва топологию! Юникод уже после.

Date: 2017-07-09 07:22 pm (UTC)
pbl: (Default)
From: [personal profile] pbl
Вот не надо в нашем уютненьком Идрисе эту вашу Агду разводить. Кышть! кышть!

Date: 2017-07-10 08:52 am (UTC)
pbl: (Default)
From: [personal profile] pbl
А мы запретим! как топологию. Помнится, была тут такая тема. Или разрешим, но только с взрывающимся ошейником. Как только определил лигатуру "!#$%>=@^" - оно бдыщ, и все.

Profile

bamalip: (Default)
шерстяной ленин

September 2017

S M T W T F S
      1 2
3 4 5 6 7 8 9
1011 12 13 14 1516
1718 1920212223
24252627282930

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Sep. 20th, 2017 01:52 am
Powered by Dreamwidth Studios