Прагма REWRITE в Agda
В этой небольшой статье расскажу про прагму REWRITE, с помощью которой можно заставить компилятор считать разные определения одинаковыми, на примере сложения натуральных чисел.
Не путать с конструкцией rewrite
Scala Developer в организации торгующей членами.
В этой небольшой статье расскажу про прагму REWRITE, с помощью которой можно заставить компилятор считать разные определения одинаковыми, на примере сложения натуральных чисел.
Не путать с конструкцией rewrite
В этой статье мы определим тип списков, введем несколько базовых операций над ними и докажем для них пару утверждений(например, что reverse (reverse list) ≡ list).
В этой статье я попробую показать соотвествие между между математическими доказательствами и программами, а так же попытаюсь ненавязчиво ввести читателя в синтаксис Agda.
И да, эта статья тоже будет типо DRAFT и я ее буду дополнять.
Эта статья будет публичной, но в статусе DRAFT, скорее всего я буду ее дополнять и пересматривать, пока тут какие-то базовые определения и доказательство того, что у (λx.xx)(λx.xx) нет нормальной формы. Скорее всего тут есть некоторые неточности и даже ошибки, буду исправлять в процессе.
В этой статье решаю задачу основанную на меме от Max Howell(создатель Homebrew), которого на собеседовании в Google заставляли инвертировать бинарное дерево, но он почему-то не смог
Google: 90% of our engineers use the software you wrote (Homebrew), but you can’t invert a binary tree on a whiteboard so fuck off.
Max Howell не смог, но я верю, что вы сможете! Рекомендую решать самостоятельно.
Нашёл вот такой инстанс WriteFreely, выглядит оч прикольно, буду пользоваться. Жаль нет приложения под ведро, придётся через браузер сидеть(хотя писать всё равно логично будет с компа). И тут нет русского в списке языков, а я хочу писать именно на нём, будем надеяться, что не слишком буду выбиваться и меня отсюда не выгонят.
Вообще что планирую, хочу писать какие-нибудь образовательные статьи по теории типов, Agda и чему-нибудь такому, не то, чтобы я шарю, но должна быть какая-то мотивация, изучать это глубже и хочется какое-то комьюнити, которое будет мотивировать двигаться дальше.
Я уже несколько раз пытался, заводил бложик, что-то писал, пытался видео записывать, но как-то не складывалось. То упирался во что-нибудь, то ещё что-то мешало. Мб формат блога и каких-то минизаписок будет успешнее за счёт легковестности.
Что-нибудь более приземленное и прикладное связанное с работой мб тоже будет. У нас там Scala, ZIO, kafka и микросервисы. Тоже не плохо делиться опытом, получать фидбек типо “Вы всё делаете не так, нужно по другому”. Этого сильно не хватает, мы в своей небольшой команде барахтаемся как можем и во всём разбираемся сами, опыт довольно специфичный.
Welcome, короче!