?

Log in

язык, на котором не говорят [entries|archive|friends|userinfo]
beroal

[ website | personal website ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]
[ tags | journal tags ]

in English [Jul. 1st, 2020|12:00 am]
beroal
[Tags|]

Welcome!

Posts in English in this blog.

Functional programming, computer science, mathematics.

My favorite links from Diigo: RSS, HTML.

OpenSearch plugin for searching on:

Short proofs in Coq.

test link
Link2 comments|Leave a comment

по-русски [Jun. 1st, 2020|12:00 am]
beroal
Добро пожаловать!

Для обратной связи пишите сюда комментарии. Если я вас не добавляю в друзья, это не значит, что я вас не читаю.

Этот блог узкотематический. У меня есть и другие блоги, просто оставьте запрос.

Поисковые системы на платформе Google Custom Search Engine:
против мошенничества

only Haskell (the programming language)

OpenSearch plugin (то есть для Firefox) для поиска по:

Математические доказательства на языке Coq. В основном мелочь, среди крупных модулей можно выделить CategoryTheory, IntBipart (целые числа как кольцо Гротендика), TakeDrop («take» и «drop» из Haskell.Data.List).

Лента выбранных мною из чужих блогов записей: RSS, HTML. Содержание примерно такое же, как и у данного блога, то есть функциональное программирование, программирование в целом, информатика, реже математика и физика. Надеюсь, вы найдёте в ней интересных людей.

Кто не является моим другом, должен вводить CAPTCHA при добавлении комментария. Я добавляю в друзья всех вменяемых комментаторов, поэтому стукните мне, если я конкретно о вас забыл.

У меня есть личный веб-сайт.
Link6 comments|Leave a comment

аннотации к ссылкам [Dec. 3rd, 2016|01:02 pm]
beroal
[Tags|, , ]

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

Обоснование правила следующее. Если контент вам нравится и вдохновляет вас, я уверен, вы найдёте для его описания более красочные и живые слова, чем «это» и «почитайте». Если вам не нравится контент, почему он может понравиться мне?
LinkLeave a comment

анализ и защита от атаки XSRF [Dec. 2nd, 2016|06:22 pm]
beroal
[Tags|, ]

Теоретическая часть. Хотя я стараюсь обходить веб стороной, недавно мне пришлось изучить атаку «межсайтовая подделка запроса» (сross-site request forgery, XSRF). Атака выглядит так. Если пользователь веб-браузера вошёл на сайт X, то открытая в веб-браузере веб-страница веб-сайта Y может отправить HTTP-запрос к веб-сайту X с паролем пользователя. То есть веб-сайт Y может выполнять команды от имени пользователя, например, отправить его, пользователя, деньги.

Читати даліCollapse )
Link1 comment|Leave a comment

утилитаризм философии, а не философия утилитаризма [Nov. 30th, 2016|09:27 pm]
beroal
[Tags|, , , ]

Я долго шёл к пониманию, чем мне не нравятся философия и философы.

Я люблю, чтобы беседа была полезной. Ну, чтобы время было потрачено не зря. Беседа полезна iff из неё следует какой-то вывод. Мы к чему-то пришли. Например, узнали, «кто виноват» или «что делать». Этот вывод очень похож на математическую теорему, потому что он стоит в конце цепочки логических рассуждений.

Читати даліCollapse )
Link8 comments|Leave a comment

достаточно одной функции [Nov. 28th, 2016|10:26 am]
beroal
[Tags|, ]

Из свойства суммы морфизмов (например, для 3-местной суммы: A_0+A_1+A_2→B ≅ (A_0→B)×(A_1→B)×(A_2→B)) следует, что несколько функций можно заменить на одну. Говоря языком простых программистов, семейство функций можно заменить на одну глобальную функцию, которая принимает имя функции из этого семейства и аргумент и вычисляет функцию, имя которой приняла.

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

goto в функциональном программировании [Nov. 21st, 2016|09:26 pm]
beroal
[Tags|, , ]

Нет, заголовок поста не получен из генератора случайных текстов. ☺ Сейчас вы поймёте его смысл. Когда компилятор оптимизирует хвостовой вызов функции, вызов превращается в тот самый goto. Благодаря этой оптимизации в чистейшем функциональном япе можно написать такую программу, что её скомпилированная версия будет содержать только цикл. Но почему останавливаться на циклах? Взаимная хвостовая рекурсия даст так называемую «лапшу», которая есть зло. Пожалуй, надо прочитать ту самую статью, где объясняется, почему goto есть зло, потому что я перестал понимать это.
Link2 comments|Leave a comment

структурированный формат данных [Nov. 21st, 2016|08:42 am]
beroal
[Tags|]

Возвращаясь к теме форматов данных, я не раз слышал от программистов термин «структурированный формат данных». Я считаю, что любой формат задаёт структуру, то есть любой формат структурированный. ☺ Выходит «масло масляное», лишний термин. Если вы с мной не согласны, дайте определение этого термина. Как принято в моём блоге, постарайтесь сформулировать как можно более формальное определение. (В этом деле хорошо пользует математика.) Особое внимание уделите отличию структурированного формата от неструктурированного. (В общем, приучайтесь мыслить логически, а не ассоциативно.)
Link3 comments|Leave a comment

сумма типов и динамическая система типов [Nov. 19th, 2016|06:03 pm]
beroal
[Tags|]

В ЯП с динамической системой типов вместо суммы типов используются атомы — уникальные значения, обозначаемые произвольными словами. Например, foo и bar. Каждый атом равен себе и только себе. foo=foo, foo≠bar.

Я придумал следующее ограничение синтаксиса ЯП с динамической системой типов. В ветвлении у каждой ветки есть шаблон и тело. Если анализируемое значение есть частный случай шаблона, вычисляем тело. Это то, что мы имеем. Пусть разрешены только ветвление, где шаблоны есть атомы, и ветвление, где шаблоны есть кортежи. Нет ветки «по умолчанию», которая вычисляется, если остальные ветки не годятся.

Тогда программист вынужден конструировать данные так же, как в языках с статической системой типов! Например, не получится использовать значения

  • a_0 = nil;
  • a_1 = (0, nil);
  • a_2 = (0, (0, nil));
  • a_3 = (0, (0, (0, nil)))

в качестве списков. Если использовать атом-ветвление, a_1, a_2, a_3 приведут к завершению программы из-за того, что анализируемое значение имеет недопустимый тип. Допустимы только атомы, а значение есть кортеж. Если использовать кортеж-ветвление, a_0 повлечёт это же самое. Список надо записать в виде a_3 = (cons, (0, (cons, (0, (cons, (0, (nil, ()))))))).
LinkLeave a comment

SEO-акция ШОК ЦЕНЫ НИЖЕ ПЛИНТУСА [Nov. 19th, 2016|10:13 am]
beroal
[Tags|]

Обидно, что LiveJournal превращается в гетто под давлением пейсбуков и фьюиттеров. У меня есть собственное доменное имя. Я решил с помощью него помочь другим людям: опубликовал на моём сайте список блогов моих друзей в LiveJournal. Вы можете изменить или добавить ссылку на свой блог и аннотацию к блогу. Разумеется, бесплатно. Это надо делать через комментарии к этой записи. Не обижайтесь, если я откажусь добавлять ваш блог.
Link5 comments|Leave a comment

navigation
[ viewing | most recent entries ]
[ go | earlier ]