Dee Mon. Былое и думы

Ссылки на избранные посты, чего тут было интересного.

Про язык ATS и зависимые типы:
https://thedeemon.livejournal.com/41035.html - можно начать тут
https://thedeemon.livejournal.com/tag/ats и дальше набор постов по тэгу. 2011

Про Clean и уникальные типы. 2011

Об информации. 2011
"... выведем некоторые важные факты теории информации и напишем на чистом функциональном языке компрессор, который будет сжимать лучше, чем zip, rar, bzip2 и 7z в их дефолтных режимах. Потом оглядимся вокруг, в том числе на физику, и в результате, надеюсь, что-то поймем об информации."

свобода, равенство, унивалентность! - про гомотопическую теорию типов. 2013

Я вижу квантовые операторы - 3D визуализация волновых функций и операторов с объяснениями и онлайн демкой. 2016

Общая теория относительности: время, черные дыры. 2015
https://thedeemon.livejournal.com/97291.html
https://thedeemon.livejournal.com/97778.html

В искривленном пространстве: визуализация неевклидовых пространств изнутри. 2018
https://thedeemon.livejournal.com/127151.html
https://thedeemon.livejournal.com/127473.html (часть картинок протухла, спасибо битбакету)
https://thedeemon.livejournal.com/127697.html

Пишем неправильный компилятор. 2010
https://thedeemon.livejournal.com/9712.html - серия постов начинается тут.
https://thedeemon.livejournal.com/tag/leo - и другие посты про него же.

Категорические вычисления (язык CPL) 2012
и продолжение/дополнения раз два три.

Про Йонеду и про должения 2012

Про язык Dafny 2015

Про корейский язык 2021

Installed some Pfizer mRNA today. Feeling fine, no side effects so far. The NHS booking site was giving 10 minute slots, and I booked one with specific time. Yet there was a queue outside the centre where I spent first 10 Minuten, then inside des vaccination zentrum even longer queue für mehr als 20+ Minuten. Other people haben früher berichtet, wie good everything in these Zentren organisiert ist, and how fast und ordentlich alles dort abläuft. Dies ist nicht ganz das, was ich beobachtet habe. Wo ist diese beworbene militärische Organisation?

Вот список имеет вид
data List a = Nil | Cons a (List a)
т.е.
F(x) = 1 + x * F(x)
а значит
F(x) - x * F(x) = 1
(1-x) * F(x) = 1
F(x) = 1 / (1-x)
и действительно, если мы такую функцию разложим в ряд, то получим
F(x) = 1 + x + x*x + x*x*x + x*x*x*x + ...
т.е. как раз тип описывает списки из х разной длины.

Но вот что любопытно,
F(F(F(x))) = 1 / (1 - (1 / (1 - 1 / (1 - x)))) = ... = x
можете на бумажке проверить или вот тут увидеть.
Это что же значит, [[[a]]] = a? ;)

Холода закончились, ставлю время от времени камеру во дворе. Интересно, будут ли в этом году новые лисята. Пока не видно.

У меня новая игрушка. Недавно в рамках праздных раздумий о языкостроении пошел я с пустым ведром зачерпнуть мудрости у лиспоакадемиков. Стал смотреть на Racket (который вырос из PLT Scheme), почитал книжку Beautiful Racket и немного поигрался с описанными там инструментами. А тут еще как раз Racket 8 вышел с новым бэкендом. В предыдущих версиях там компилятор делал байткод, а тот уже в рантайме JITился. А в 8.0 они перешли на компилятор и бэкенд от Chez Scheme, где сразу нативный код генерится.
Сам Racket преподносится как платформа для создания языков. И стандартный рецепт, которому придерживается Beautiful Racket, это если захотел ты сделать свой бэйсик, то регистрируешь свой пакет basic из двух определенных частей (парсер и экспандер), потом пишешь исходник на бейсике, ставишь в нем первой строчкой #lang basic и используешь компилятор Racket. Тот видит первую строчку, достает твой пакет, скармливает остаток файла твоему парсеру (тут у тебя полная свобода по синтаксису), твой парсер производит parse tree, которое передается второй части твоего пакета, которая то дерево преобразует в дерево кода на самом Рэкете. Полученный код на Рэкете уже компилируется, и вот твой бэйсик и скомпилирован.
Но есть один момент, который та книжка почти не упоминает, но который позволяет не опираться на компилятор Рэкета. Дело в том, что в Рэкете есть eval, и вся машинерия компилятора уже содержится в твоем бинарнике. Можно сделать свой один бинарник, который будет парсить новый язык, также разворачивать его в конструкции Рэкета, и тут же выполнять через eval. Под капотом там генерация нативного кода, и скорость получается ничуть не хуже.
В качестве proof of concept сделаем интерпретатор, который сможет выполнять код такого вида:

fac(n) => if n < 2 then 1 else n * fac(n-1);

fib(n) => 
  if n < 2 then 1 
  else {
    a = fib(n-1);
    b = fib(n-2)
    in a + b 
  };

loop(x) => 
  if x < 20 then {
    print(fib(x), fac(x))
    in loop(x+1)
  } else 0;

loop(1)

( Collapse )

Я раньше любил изучать какие-нибудь экзотические языки программирования и потом тут про них рассказывать, будь то Clean, ATS, CPL, Idris, Dafny и пр. Но некоторое время назад обнаружил, что как-то больше не вижу особо интересных ЯП, одни языки все повторяют один и тот же набор фич, другие углубляются в направления для меня не шибко интересные.
Но зуд-то остался. Пришла мысль, что хорошо бы поучить интересный язык не программирования. Настоящий. Только европейские языки какие-то скучные. Японский слишком большой. Китайский в чем-то проще, но тоже зубрить тысячи иероглифов, плюс сложная фонетика, плюс тона, а тонов мне в тайском хватило, больше не хочется. Зато вон есть японокитайский-лайт: корейский. Там нет тонов, там письменность, которая хоть внешне и похожа на иероглифы, на самом деле очень простая и учится за час. Там вполне доступная/привычная для русского человека фонетика (мы умеем говорить "ы"!) А больше я про него ничего и не знал на тот момент. Но решил попробовать.

К слову о фонетике, вот в меру разборчивый и не слишком быстрый пример. Кажется, что текст можно было бы записать русскими буквами, ничего особенно сложного в произношении не заметно.

(тут субтитры тайскими буквами, не обращайте внимания)

Поставил на телефон обучающие приложения, начал и... увлекся! В отличие от европейских языков, где нам многие слова знакомы и понятны, тут все поначалу максимально незнакомо, язык выглядит как шифр, как пазл. Тем интересней этот пазл решить, научиться этот шифр понимать. О чем поют корейские красавицы? Какие слова и обороты используют? Если просто взять перевод песни, видишь уже конечный результат трансляции, результат черного ящика, а интересно же понять внутреннюю логику языка, что конкретные слова означают и как соединяются в фразы. О занятных находках сегодня и поговорю.

В процессе оказалось, что многие слова все-таки знакомы. Вот слово звучит как монада. Вот слово звучит как JSON, теперь мы знаем как он переводится, похоже на правду. :) А вот "пукан" - так южнокорейцы называют Северную Корею. ( Collapse )

Позапускал тут одну свою программку (тупое решение Project Euler #300, много простых операций с интами, умещающимися в кэше) на двух ноутах. На одном Intel Core i7, на другом Apple M1. Так вот, даже в режиме эмуляции x86_64 M1 немного быстрее. А в родном для него arm64 - много быстрее.

                        L=13 1-thread  parallel ; L=14 parallel
 Intel Core i7 2.6 GHz           20.0      4.06 ;         22.02
 M1 running x86_64              15.65      3.15 ;         18.06
 M1 running arm64               11.84      2.44 ;         13.7
                                       time in seconds

https://gist.github.com/thedeemon/ec45c44e14c3205075f66d4bc3f92abf
Компилятор на обоих - LDC (LLVM-based).

Кстати, про Project Euler. Вы решили задачку #100? Я чего-то туплю, не решил пока.

Месяца полтора назад меня навели на мысль поискать что-то по этой теме. В браузере на тот момент было открыто около 150 вкладок, многие висели там месяцами или дольше, будучи когда-то открытыми, недочитанными и так оставленными когда-нибудь потом к ним вернуться. Это, конечно, самообман. Новые открытые вкладки добавляются в этот reading list быстрее, чем я к ним возвращаюсь, процесс не сходится. Поискав совсем чуть-чуть, быстро нашел расширение для браузера под названием Tab Wrangler. Он есть и для хрома, и для файрфокса. Принцип работы простой: если вкладка открыта где-то фоном, но на нее не переключались уже больше некоторого времени Т, то скорее всего там что-то не очень-то и нужное. Тогда она тихонько закрывается, а ссылка помещается в специальный список. В любой момент можно этот список посмотреть и если там все же что-то нужное, открыть оттуда вкладку обратно. Есть там так же настраиваемый белый список сайтов, которые он закрывать не будет, например, то что чисто по работе.
Я себе сделал период Т = 1 сутки. К чему сутки не возвращался, то тихонько исчезает из поля зрения и больше глаза не мозолит. Доставать что-то из списка закрытых, по моему опыту, приходится довольно редко. После шести недель в таком режиме, пожалуй, я доволен. Голова разгружается, фокус улучшается, хлам не хламится. Рекомендую!

Мой старый ноут с HDD последнее время работал все медленнее и медленнее во всем, что касалось работы с диском, особенно после перезагрузки долгие минуты был неюзабелен, да и сама перезагрузка занимала много времени. Несколько лет назад все было нормально, а потом медленно и плавно стало хуже. Я уж было думал, это винда виновата, совсем там разработчики расслабились на SSD и не проверяют, как ужасно все на HDD работает. Совсем там многочисленные фоновые сервисы жить не дают. Но потом меня все же осенило посмотреть S.M.A.R.T. диагностику. Оказалось, это просто жесткий диск захворал и потихоньку собирался загнуться. Узнал, что на амазоне можно за сотню денег взять терабайтный SSD и USB-SATA проводок и в домашних условиях спокойно переписать данные и заменить диск. Для замены оперативки там в ноуте есть маленькая дверца с винтиком, но оказалось, что для замены диска нужно снимать все днище. Раскрутил все винтики по периметру, но крышка не снималась, что-то продолжало держать. Хорошо на ютюбе есть ролик на любую тему, в том числе про нужную мне операцию. Там подсказали, что есть еще пара секретных винтиков, например один скрыт под резиновой ножкой, которую надо снять сперва. В итоге, все получилось, заменил HDD на SSD, теперь все летает.