Стендап Сьогодні

Що я зробив, що я хочу зробити, і що це все значить.
Повсякденні здобутки в форматі стендапу.
Детальніше в статті

08.08.2023

Пригоди з оновленням Ruby

Сьогодні вирішив оновити на проєкті Ruby з 3.1 на 3.2. Якщо не знаєте, то нова мінорна версія Ruby виходить щороку на Різдво — тобто давно пора оновлюватись.

Але вийшло, що Rails 6.1 - які, до речі, вийшли в грудні 2020 - припинили отримувати оновлення ще минулого вересня. Та з Ruby 3.2 не працюють. Проблеми зʼявляються навколо використання названих аргументів — а саме, якщо в Ruby 3.1 функцію з названими аргументами можна було викликати з хешем аргументів, то в 3.2 це вже дві різні конструкції та такий виклик призводить до помилки.

Значить, потрібно також оновитись до Rails 7 (які вийшли в грудні 2021 та являють собою останню мінорну версію на цей день.) Змін не так вже й багато. Цікаво, що Rubocop також включає декілька правил для Rails 7, наприклад, Rails/UniqueValidationWithoutIndex.

Але не все так просто — з Rails 7 припинив працювати Webpacker - бо він взагалі більше не підтримується. Є декілька альтернатив - jsbundling-rails та інші — проте найпростіша в переході бібліотека shakapacker. Назва дивакувата, зате Shakapacker є прямим нащадком Webpacker та без великих зусиль підтримує ту саму конфігурацію, що й Webpacker 6.0rc6, що я перевірив порівнянням результатам збірки. Конфігурація була дуже складна, тому й не став все переробляти на кардинально новий конвеєр — бо все, що я хотів, це оновити Ruby.

07.08.2023

Як кодувати міста в програмній системі?

Вправа: користувач має змогу обрати своє місто та країну, з автодоповненням. Далі адміністратор може побачити користувачів за обраним містом та країною. Як би я реалізував таку функціональність?

Варіант наївний. Робимо два текстових поля, автодоповнення зі списку країн та великих міст — або свій варіант. Відповідно, адміністратор робить запити за текстовим збігом. Плюси: мінімум зусиль; покриває буквально всі міста у світі — поточні, минулі та майбутні. Мінуси: у даних будуть розбіжності — помилки, альтернативні назви, назви різними мовами, та інше. Такий варіант підходить для невибагливих систем — наприклад, мапа мешкання спільноти не потребує прямо стовідсоткової повноти.
Варіант специфічний. Часто список міст цілком конкретний. Наприклад, в поштовій системі це можуть бути міста з відділеннями. Тут можна зробити табличку в базі та дати обирати міста зі списку. Плюси: максимальна чіткість, простота для користувача. Мінуси: вимагає наявності готового переліку. Тут треба запитати: чи дійсно потрібно дозволити користувачу обрати будь-яке місто? Чи є в цьому користь для продукту?
Варіант утопічний. Моделюємо всі міста у світі, скориставшись, напевно, деякою готовою базою даних. Тут, на мою думку, баланс “витрати — користь” непрактичний. В реальних географічних даних купа ускладнень. Єдине місто може називатись різними іменами: Krakow, Cracow чи Krakau? Навпаки — є сила-силенна міст-тезок: у США 5 Лондонів, а у Херсонській області — три Новодмитрівки. Фактично, така проста ззовні функція вибору міста перетворюється на повноцінний продукт. Тому…
Варіант аутсорсингу. Варто звернутись до готових рішень: API. Наприклад, API Google Maps. Він повідомить дві назви: main_text - назву міста, та secondary_text - уточнюючу локацію — наприклад, “Новодмитрівка” та “Білозерський район, Херсонська область”. Цей API вже знає й різні мови, й альтернативні назви. Окрім того, він повертає place_id - унікальний ідентифікатор, який можна зберігати у свою базу та легко за ним фільтрувати.

До речі: цікава гра “Скільки міст ти знаєш?”. Мені подобається, що вона повідомляє, який відсоток населення живе у вказаних тобою містах.

06.08.2023

Мова емоцій

Прочитав (або точніше, прослухав) книжку The Language of Emotions, дізнався про яку, як це не дивно, зі статті Кента Бека — творця Agile Programming. На мою думку, ця книга добре підходить для айтівців, оскільки надає аналіз та інтелектуальну інтерпретацію емоцій — тобто як їх розуміти “головою”. Таким чином, книга вчить інтелектуальну та емоціональну частину особистості співпрацювати, причому вчить досить прямим та дієвим підходом. Це дуже важливо, бо наша субкультура вимагає тверезого та аналітичного мислення та спілкування, де емоції ніби зайві — при тому, що, на мою думку, вони потрібні не тільки для чемного спілкування, а й для ефективної роботи (бо код, проєкти та сервіси теж викликають емоції, які теж варто розуміти.) На думку автора книги, емоції cлід не оцінювати як хороші чи погані, а слухати як сповіщення від несвідомої частини нашого розуму.

Напевно понад усе мені запамʼяталася глава про страх. Вона каже, що страх — це відчуття підвищеної уваги до нашого оточення. Я раніше думав, що страх — це коли відбувається щось загрозливе, а виходить, що страх починається раніше. В мене така аналогія: тривога — це коли ти збираєшся йти до лісу, де живуть ведмеді; страх — коли ти в лісі; а коли вже тікаєш від ведмедя — то паніка. З цього ракурсу я зміг зрозуміти, що значить, що українці живуть зі страхом; бо хоч в містах нашому життю рідко загрожує безпосередня небезпека, але ти завжди прислуховуєшся до звуків на вулиці, причому абсолютно автоматично. Це і є страх.

Ще приклад страху — коли дивишся код та отримуєш неприємне відчуття, що це місце спричинить проблеми в майбутньому. А тривога — коли пишеш код, але остаточного розуміння задачі немає. Моя історія про відволікання - це теж тривога та дизасоціація, яку вона спричиняє. Тож якщо навчитись краще помічати за собою такі емоції, то можна стати кращим розробником… ну як, продав вам “мʼякі навички”?

05.08.2023

CouchDB - база даних з крутою реплікацією

Є така база даних - CouchDB - про яку майже ніхто не знає. Вона була помірно популярна десь біля 2010-го, але й досі отримує регулярні оновлення, причому досить вагомі. Я використовував її в маленькому сайд-проєкті, де робив з нею багато, проте у світ проєкт не вийшов, тож як воно в справжньому продакшні, сказати не можу.

З першого погляду, CouchDB - документна СУБД з максимально простою структурою, яка, до речі, схожа з OpenSearch. Документи складаються в бази даних, бази даних живуть на серверах. Цікавий момент — баз даних може бути скільки завгодно, наприклад, по базі на користувача.

Але що насправді цікаво, це як вона працює з реплікацією. Модель реплікації CouchDB підтримує скільки завгодно вузлів, причому не обовʼязково постійно підключених. Тобто це ідеальна база для роботи офлайн. Наприклад, мобільний пристрій може працювати зі своєю локальною базою, попри стан підключення, а оновлювати коли це стає можливо.

Що робити з конфліктами? Власне, вирішати нам — в CloudFlare потужний механізм розвʼязання конфліктів. Можна робити це автоматично, за правилами переваги, а можна й написати код зі специфічною логікою.

А ще, реплікувати можна не всю базу, а частину документів за правилом. Наприклад, може ми хочемо завантажувати на сервер тільки опубліковані документи. А ще можна обмежити реплікацію тільки одним з напрямків. А ще реплікувати багато баз в одну або навпаки — одну в декілька…

Окрім самої CouchDB, є ще повноцінна реалізація на JavaScript - PouchDB. Її можна запускати в браузері або в React Native, та синхронізувати з сервером CouchDB.

04.08.2023

Бітові поля в базах даних та чому це погана ідея

Розкажу про одну зі своїх поганих ідей. Треба було зберігати в базі для кожного рядка набір булевих відміток. А потім — шукати за комбінацією цих відміток. Все це являло собою такий собі скінченний автомат.

Мені здалося дуже розумно не робити по стовпчику на кожну відмітку, а зробити бітове поле. Тоді можна додавати біти операцією OR, а шукати на кшталт bits AND 0b101 != 0. Бітові поля — крута технологія, та дозволяє розвʼязувати задачі, які здаються неможливими. Тільки історія не про це, а про те, як любов до крутої технології мене підвела.

В чому ж проблема? В пошуці. Як думаєш, яким чином можна здійснити пошук по такому стовпчику? Якщо відкрити перелік індексів в PostgreSQL, то знайдеш багато корисного. От тільки індексів по бітовому полю немає. На практиці це значить, що доведеться завантажити кожне значення та перевірити його на відповідність умові. Іншого шляху фізично немає.

Далі все залежить від того, скільки рядків треба перебирати. Якщо є додаткові (та більш ефективні) умови — добре. Якщо ж цей скінченний автомат лежить в серці логіки та фільтрувати доведеться мільйони записів — погано.

А в OpenSearch - базі, що побудована навколо ефективного пошуку — взагалі немає можливості шукати за бітовими операціями. Щоб не кортіло.

У цьому стародавньому треді знайшов гарну альтернативу — зробити замість бітового поля масив цілих чисел — множину. Та побудувати для нього індекс GIN.

03.08.2023

Міграції в OpenSearch

Хоч в OpenSearch й немає жорстко заданої структури даних, потреба в однорідності даних залишається. Ну, може, не у всіх застосунках, може десь є проєкт, який просто індексує аби який JSON - але зазвичай все ж таки ми очікуємо бачити в документах певні атрибути.

Та, як всі знають, сьогодні атрибути одні — завтра можуть бути інші. Що робити з тими документами, які вже існують? На відміну від бази SQL, де можна легко додати новий стовпчик зі значенням за замовчуванням, в OpenSearch готового рішення немає.

Найпростіший технічно варіант — це нічого не робити, а при читанні чи пошуку враховувати, що поле може бути порожнім (тобто null). Не знаю, як ви, а я дуже не люблю перевірки на null “про всяк випадок”. Особливо коли воно скероване не бізнес-логікою, а невпевненістю бази даних.

Можна ввести версії схеми документів. Тобто в кожному документі є атрибут версії. При читанні документа робиться міграція до поточної версії (та, можливо, запис її в базу.) Так я робив, тільки не в OpenSearch, а в CouchDB - моделі документів в них дуже схожі. Впровадження явної версії спрощує обробку порожніх полів. Вона нагадує міграції бази, як в Rails, тільки на рівні кожного документа. (Особливо цікаво воно в розподіленій базі CouchDB, бо старі документи можуть бути приховані на вузлі, який давно не синхронізувався.)

Нарешті, є механізм Update by query, який, здається, і призначений робити міграції даних. Тут можна запустити масову операцію оновлення — хоч для всіх документів. Є тільки одна проблема — на відміну від SQL бази, ця операція не є атомарною або транзакційною. Вона обробляє документи поступово, та ті документи, що встигли помінятись іншим шляхом, не будуть оброблені взагалі.

02.08.2023

Як Kafka гарантує послідовність повідомлень

Ну, годі про формальну верифікацію. Я нещодавно був вражений простим, але дієвим підходом Kafka до послідовності повідомлень.

Для побудови простої в розумінні системи бажано, щоб послідовність подій на виході була така сама, як на вході. Втім, зазвичай зі збільшенням масштабу гарантія послідовності втрачається. Це відбувається тому, що повідомлення можуть бути отримані різними вузлами в кластері. А при читанні послідовність обробки вузлів також не визначена, тому може перемішатись ще й там.

Розглянемо приклад. де нам треба обробляти журнал у форматі “запит”-“відповідь”. Через втрату гарантій послідовності ми не можемо очікувати, що побачимо повідомлення “запит” раніше, ніж “відповідь”, та нам доведеться додатково продумати, що робити з відповіддю, яка прийшла раніше свого запита.

Звісно, рішення існують — наприклад, в AWS SQS є режим FIFO - хоч і суворо обмежений - 300 повідомлень в секунду проти мільйонів у Кафки.

Що робить Кафка? У Кафки одиниця масштабування — це розділ. Кожна “черга” (topic) ділиться на розділи (partition). На рівні розділу послідовність повідомлень гарантована. Кожний розділ призначений до конкретного вузла, який приймає всі записи в нього. Зі збільшенням масштабу кількість розділів та вузлів може зростати стільки, скільки треба, зі збереженням гарантій.

Ключовим є те, що виробники можуть самі вирішувати, в який розділ писати кожне повідомлення. Наприклад, якщо ми пишемо журнал подій, та їх треба групувати за субʼєктом, можна зробити ID субʼєкта ключем розподілу. А в системі “запит”-“відповідь” - просто стежити, щоб відповідь була записана в той самий розділ. (Єдине розумне обмеження — щоб розподіл був рівномірним та не створював “гарячих розділів”.)

А з боку споживача існує механізм групи споживачів. Група споживачів ділить між собою всі розділі топіка — кожний розділ дістається тільки одному клієнту з групи. Таким чином, кожний споживач отримує “скибочку” повідомлень. Послідовність в скибочці гарантована. як і відсутність конфліктів. Коли клієнти підключаються чи відключаються, призначення у групі балансуються наново.

Така от неочевидна архітектурна перевага (а я спочатку думав — навіщо ті розділи?)

01.08.2023

Формальна верифікація: перетворення виразів

Всі ці теореми та конʼюнктивні нормальні форми звучать дуже абстрактно, але що воно являє собою та як з ним працювати. Думаю, не буде новиною, якщо я скажу, що тут теж синтаксичне дерево. Ну, або ж просто дерево, бо воно не відповідає ніякому синтаксису.

В ліспах взагалі код та структура мають буквально ідентичний вигляд. Хіба що для того, щоб якось відрізняти, я використовував не списки, а масиви як вузли дерева. (Може здаватись дивно, що масиви, а не обʼєкти, але в ліспі працювати з масивами природніше.) Операції пишуться в польській нотації, тобто спочатку йде оператор, а потім операнди.

Доведення виразу буде успішнішим, якщо спростити його. Вручну зрозуміло, як це робити: якщо ми бачимо вираз X || false, то відразу можемо замінити його просто на X. Щоб досягти такого результату автоматично, я побудував рушій пошуку зразків у виразі та заміни їх. Це виявилося зручною абстракцією - залишилось тільки зібрати словник відомих алгебраїчних тотожностей. Також рушій спрощення знаходив фрагменти виразу, де всі операнди є константами, та заміняв на результат обчислення.

Що мені особливо подобалось, так це те, як зручно обробляти деревоподібні структури функціональним кодом. А також те, що в Clojure всі структури даних мають порівняння за значенням. Це корисно, наприклад, коли треба шукати піддерева, що повторюються для пошуку зразків.

Код для цієї частини

31.07.2023

Формальна верифікація: доведення теореми

Коли в нас є теорема про вірність програми, залишається її довести. Що то взагалі значить — довести? В логіці теорема — це просто логічний вираз з невідомими. Довести — значить, показати, що для будь-якого набору значень невідомих теорема буде вірною. Як приклад: A || ~A (A або не A) буде вірним завжди, як можна побачити тривіально. На жаль, теореми про вірність виходять не такими простими. Тож як можна довести теорему — та ще й автоматичним шляхом?

Якщо невідомих небагато, можна довести повним перебором — тобто обчислити значення теореми для кожної комбінації та перевірити, що воно завжди буде істиною. Складність доведення росте експоненційно; для десяти невідомих це тривіально, для пʼятдесяти — нереально. (Кожний логічний вираз в програмі — рівність чи нерівність — стає невідомою в теоремі, та ще й деколи в різних варіаціях.) Я використовував такий метод до 20 невідомих.

А для складніших теорем я використовував метод резолюцій. Це підхід до доведення від оберненого: щоб довести нашу теорему, ми знаходимо підтвердження тому, що обернена теорема хибна. Для цього в оберненій теоремі треба знайти суперечність.

Пошук суперечностей відбувається за ітеративним алгоритмом. Спочатку теорему перетворюємо на конʼюнктивну нормальну форму — отримуємо, просто кажучи, ззовні AND, а всередині OR -дизʼюнкти. Достатньо знайти пару дизʼюнктів, які є протилежностями, щоб їхній AND ніколи не був істиною. Якщо з першої спроби не виходить - “схрещуємо” наявні дизʼюнкти, поки не знайдемо протилежні.

Буває й таке, що суперечність знайти неможливо — тоді теорема не буде доведеною, відповідно, вірність програми неможливо встановити. На жаль, остаточну відповідь “ні” ми не отримуємо — тільки відсутність успіху.

Код до цієї частини

30.07.2023

Формальна верифікація: найслабкіша передумова

Після того, як отримали синтаксичне дерево програми, починається його обробка, а саме, як я писав на початку, створення теореми про вірність. Для цього використовується така модель як семантики перетворення предикатів.

Починаємо з післяумови, яка вже повинна бути задана. (До речі, я про це не згадав, але одна додаткова синтаксична функція моєї граматики — оголошення перед- та післяумов у коментарях.) Далі беремо останню команду та перетворюємо післяумову на найслабкішу передумову, яка гарантує справдження післяумови після цієї команди.

Розглянемо найпростіший приклад. Якщо команда — це присвоєння x = y+1, то всі згадки про x у післяумові треба замінити на y+1. Якщо післяумова була x > 0, то найслабкіша передумова - y+1 > 0.

Так рухаємось від останньої команди до першої, та послідовно перетворюємо умову. Перетворення для умовного оператора if лише трохи складніше та являє собою поєднання двох гілок. Перетворення для циклу суттєво складніше та потребує від нас оголошення інваріанта та обмеженої змінної. Інваріант — це умова, яка справджується після кожної ітерації циклу. Обмежена змінна — зобовʼязана зменшуватись з кожною ітерацією, але бути додатною. Ці анотації допомагають довести, що цикл закінчиться.

Нарешті, отримуємо найслабкішу передумову для всієї програми. Залишається тільки поєднати її з оголошеною передумовою знаком “випливає” (⇒) та теорема про вірність готова!

Мабуть, потрібно подумати про те, що така теорема стверджує. Вона обмежена тим змістом, який вклав програміст; без хорошої перед- та післяумови доведення не буде корисним — або навпаки, не буде можливим. У цьому формальна верифікація схожа на юніт-тести - “правильність” програми все одно залежить від людського розуміння. Різниця в тому, що юніт-тести перевіряють обмежений набір випадків, а формальна верифікація — буквально всі.

Код для цієї частини

Раніше

Пізніше