Pull to refresh
45
0
Александр Рулёв @Rulexec

Пользователь

В языках программирования с поддержкой зависимых типов очень просто решается проблема останова.

Мы просто разрешаем существовать только гарантированно выполнимым функциям. Проворачивается это каким-нибудь таким способом:

recursive :
  A → B:(A → U) → C →
  order:TotallyOrdered C →
  HasLowerBound C order →
  IsDiscrete C order →
  extract:(A → C) →
  
  (a:A →
   (x:A → Lesser order (extract x) (extract a) → B x)
   → B a)
   
  → a:A → B a


Мы хотим получить функцию A → B (принимающую значение типа A, возвращающее значение типа B), в которой хотим использовать рекурсию.

Для этого мы просим наличие типа C, элементы которого линейно упорядочены, имеющий нижнюю границу (меньше которой элементов не существует) и для которого выполняется дискретность (есть гарантии того, что между двумя любыми элементами конечное количество элементов, т.е. например, это целые числа, а не рациональные).

И ещё просим функцию A → C, которая «оценит вес текущего значения A».

Затем принимаем функцию, которая принимает значение типа A и функцию, которая делает рекурсивный вызов, но которая принимает не только значение типа A, но и доказательство того, что у переданного значения вес меньше, чем у предыдущего. Тогда, очевидно, рекурсия не сможет продолжаться бесконечно, т.к. когда-нибудь она упрётся в нижнюю границу.

И все наши программы будут завершаться когда-нибудь (если никто не будет вычислять что-нибудь невероятно долгое, вроде функций Аккермана — ограничивать по времени выполнения куда сложнее, придётся описывать виртуальную машину и ограничивать количество выполняемых инструкций).
Можно, один из них — теория типов.

У вас сейчас статически типизированные программы типизированы не полностью. Т.е. у вас в наличии функции типа «принимает массив с элементами типа T и число, возвращает элемент типа T или создаёт исключение».

А в более мощных системах типизации (где есть зависимые типы) можно иметь функции типа «принимает массив длины n с элементами типа T, число m, которое больше либо равно нуля, строго меньше n, возвращает элемент типа T».

И тогда вам нужно будет передавать в эту функцию значения типа «m меньше n», чтобы ваша программа вообще смогла скомпилироваться.

И так можно описывать абсолютно что угодно, включая то, как должны обрабатываться внешние события, хотя никто не верит.
Посмотрел, очень интересно, явное всегда лучше неявного. Спасибо большое, мне нравится этот подход, посмотрим как-нибудь.
Да, так и есть, нужно будет делать что-то вроде .then(checkedForCancel(function(data) { ... })), где checkedForCancel будет возвращать функцию, которая будет проверять какую-нибудь переменную, и только если она всё ещё хорошая, выполнять переданную.
> Тут пользователь снова жмёт «удалить», очень резко, настолько резко

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

Всё это дело понеслось, а тут пользователь нажимает на ссылку, старый контент уже никому не нужен, нужно загружать новый. Окей, создаём новый промис, повторяем накидывание обработчиков. Постойте-ка, у нас в процессе выполнения старый. И тут оказывается, что у Promises/A+ нет никаких вариантов обработки отмены промиса.

Нам остаётся три пути:

  • В каждом обработчике проверять, а не устарел ли запрос на действие, может результат уже никому не нужен.
  • Сделать так, чтобы результат выполнения ВСЕГО промиса был проигнорирован (хотя и выполнен).
  • Использовать 3rd party промисы или пилить свои.


Пока не особо думал об этом, на данный момент отошёл от промисов, давно не использовал, но пока выглядит так, что отмена должна найти стык, где промис ещё в процессе резолвинга, подменить ему then'ы на пустышки, и послать внутрь самого промиса сигнал отмены, который он может обработать, чтобы прекратить своё выполнение, если может (к примеру, если там промис, который просто спит сколько-то времени, то в обработчике отмены он может просто сделать clearTimeout).

Это всё ещё можно снабдить специальным сахаром для обработки отмен, чтобы можно было обрамлять некоторые куски цепочки операций, чтобы обрабатывать некоторые специфические случаи.

К примеру, есть метод, удаляющий некий item, возвращающий промис о завершении. Внутри он отправляет запрос на сервер, плюс делает какие-то действия с моделью. Пользователь жмёт «удалить», метод вызывается, промис начинает работу. Тут пользователь снова жмёт «удалить», очень резко, настолько резко, что запрос даже не успел уйти на сервер (окей, может, у нас есть какая-нибудь логика группировки запросов, или окна общения с сервером, поэтому он не уходит сразу). Тогда мы должны отменить промис удаления. Но произвёв отмену, нам бы хорошо знать, ушёл запрос на сервер или нет. Поэтому мы можем вставить в место, где совершается непосредственно запрос, специальный обработчик, например, .onCancel, который вызовется только когда чейн промисов в состоянии отмены и в него передастся, какое состояние у промиса, на который он непосредственно был накинут (т.е. начал он резолвится или ещё нет). Где каким-то образом куда-нибудь сообщим, что да как. И, например, если запрос уже ушёл, то нам нужно посылать второй в догонку, мол, «сервер, пользователь передумал это удалять, верни как было, пожалуйста».

Я пока не могу придумать, как можно типизированно сделать, чтобы тот, кто инициировал отмену мог подоставать данные из этих обработчиков с любой глубины, ибо структура чейна промисов может быть совсем любая, и мы не всегда сможем сказать, какие данные наши, какие не наши (например, если в чейне делается несколько запросов, у всех из которых есть обработчики отмены, генерирующие данные, мы отменяем чейн и хотим в результатате операции отмены знать результат отмены конкретного типа запроса). Пока думается, что можно при инициации отмены передавать таблицу Symbol→обработчик, а потом очень аккуратно и обдуманно в обработчиках отмен посылать туда данные, если в сигнале отмены в таблице присутствует некоторый символ.

Ох, что-то случайно прорвало.
Как запросов будет всё больше, кто-нибудь да заметит даунтайм.

Я бы подумал, как бы делать всё это дело бесшовно. На вскидку:

  1. Делаем так, чтобы могло работать два экземпляра сервера одновременно (проблемы в данном случае, как я понимаю, могут быть в основном из-за эксклюзивного доступа к файлам, в которые пишите)
  2. Запускаем приложение на каком-нибудь левом порту, например, 8001
  3. Настраиваем iptables на форвардинг 80 → 8001
  4. Когда хотим обновиться, поднимаем второй экземпляр, например, на порту 8002
  5. Перенастраиваем iptables на форвардинг 80 → 8002
  6. Посылаем первому экземпляру сигнал на завершение, на который оно должно дообработать текущие запросы, а больше и не придёт.
  7. Done.


Тут главное разобраться с iptables, чтобы оно случайно на половине TCP соединения не стало пакеты перебрасывать, а только новые. Если нельзя так — придётся свой роутер пилить.
Деплоитесь всё так же? kill, restart?
О да. Я не особо осилил лексеры/парсеры, а как увидел PEG — влюбился в них.

Вот, например, можно потыкать онлайн — http://pegjs.org/online.
В итоге выяснится, что даже если там есть квантовые процессы, они используются для внутреннего генератора случайных чисел, чтобы принимать решения.
Это проблемы недостаточной проницательности компиляторов. Можно без проблем написать на ФП тот же квиксорт, который будет работать с вектором и использовать только операции перестановки элементов местами. Компилятор должен увидеть, что копий массива не создаётся и что можно использовать тот же самый.

С хештаблицами то же самое. Это лишь массив списков. Если компилятор сможет увидеть, что к старым версиям таблицы не обращаются и существует только одна последняя — нет проблемы сгенерировать код равный императивному.

Со слабыми хештаблицами сложнее, ибо в ФП нет никакой памяти, объектов по указателям, ибо мы от всего этого абстрагировались. Нужно или вручную, или вводить в ЯП тип объектов, держащих значения, плюс тип слабых ссылок, конструктор которого принимает объект и любое значение и функцию, которая будет должна подменить значение и заменить следящий объект, если объект подвергается сборке мусора. Тогда делаем список на этих слабых ссылках, указывая фактором разрушения объект, хранящиеся в следующем элементе. Как вызывается коллбек — выбрасываем звено с этим объектом.
Функция с побочными эффектами это функция, принимающая значение состояния нашей Вселенной и возвращающая некий результат, плюс новое состояние Вселенной.

Доказывать то, что некие данные появились из I/O, а не от балды легко — ввести типов вроде IsStringFromStdin, значения которых будут возвращаться только из встроенных функций для работы с I/O. С гарантиями записи так же.

В итоге программа будет являться отображением Вселенной во Вселенную, плюс кучей типов вроде ВЭтойВселеннойБылОткрытПорт(80) и ДляПотокаБайтБылИспользованПарсер(html), ЕслиОткрывалиФайлПоЗапросуАЕгоНетВернулиHTTP404 и так далее (хотя я на самом деле этого не представляю, никто в жизни не сможет формально описать программу целиком, только её основные части).

Входящие данные обрабатываются так же как и обычно. Просто функция сравнения, например, возвращает не Boolean, а тип-сумму из доказательства или опровержения равенства. А дальше обычный switch и две ветки исполнения.
Вот сидите вы в своём энтерпрайзе глухо, десятками лет оттачиваете навыки джавы/шарпов, ходите на конференции, разрабатываете серьёзные системы и считаете, что всё так и будет и дальше, куда может деться спокойное энтерпрайзное программирование? 50 лет стояло — ещё 50 простоит.

Но я уверен, что беда придёт откуда не ждали. Функциональное программирование медленно, но верно просачивается всюду, пускает свои ростки. Вы смотрите, уже и в джаве наступает время конкурентности, а не параллельности. И лямбды, мапы, фильтры и, страшно подумать… свёртки списков!

Сейчас оно проникнет в мейнстрим и люди начнут массово мыслить «функционально».

И тут всплывёт вопрос типизации. Вот вы говорите, что язык должен быть статически типизирован. Что если я скажу вам, что с моей точки зрения типизация джавы — какое-то ребячество, позволяющее только отличить строку от числа?

Полиморфная типизация уступает зависимой в бесконечность раз. Языки, поддерживающие зависимые типы (Coq, Adga, Idris) пока только зарождаются и пока выглядят очень плохо и хило. Но есть ребята, которые двигают HoTT и в процессе формализации HoTT в HoTT получат нечто божественное.

А затем окажется, что можно один раз написать формально верифицированный код и… цена его поддержки равна нулю. В нём guaranteed by math нет багов и он работает согласно спецификации, и как бонус — в нём нет ни одной излишней динамической проверки и он работает быстрее любого си-кода, который написан человеком.

И тогда будет лишь два вида разработки — «серьёзная», где требуется надёжность. И «несерьёзная» — где можно тяп-ляп и на динамическом ЯП быстро заставить машину сделать чего нужно.

Языки «среднего класса» умрут.
Хранить бэкапы в том же датацентре — как-то неправильно.
WhatsApp на джаббере, вроде как.
Но да, это не решение проблемы. Транспорты всё равно требуют существования аккаунта на чужеземном сервисе и шумят.

Тут нужно использовать терроризм в больших масштабах, чтобы заставить создателей мессенджеров общаться между собой. Чтобы им было невыгодно не предоставлять такой возможности.
Если эти боты будут причинять много насилия мессенджерам, то их или начнут банить, или выкатят апи для интеркоммуникации.

QIP Infium во-первых просто поддерживал и jabber и аську. А вот у джаббера были божественные транспорты, через которые и icq, и ВК, и всё что угодно можно было подключить, если такой есть. И транспорты генерировали отдельные контакты, что делало общение совсем бесшовным.
Можно сделать сервис хотя бы для аггрегации контактов. Чтобы он запилил какую-нибудь хорошую систему адресации и имел ботов во всех распространённых мессенджерах.

Пользователь получает себе адрес, указывает свои контакты во всех мессенджерах, что у него есть, боты высылают подтверждения. А так же указывает главный мессенджер.

Затем когда кто-нибудь хочет обратиться к кому-нибудь — может попросить бота переключиться в режим чата с указанным адресом. Другой стороне на главный мессенджер приходит сообщение. Через какое-то время, если оно не было доставлено — уведомления на все остальные.

А так же команду, которая бы шарила всеми своими контактами с обратившимся, чтобы можно было напрямую общаться.

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

PHF не используются в рантайме. Они используются во времени компиляции, чтобы дико оптимизировать словари. Например, когда мы делаем switch-case по строкам не нужно делать O(N), проходясь по каждой строке и сравнивая её с данной, либо считать хэш от всех байт переданной строки. Достаточно найти PHF от case'овых строк, который будет смотреть всего парочку бит, которые уникально характеризуют каждую из строк, узнавать, на какую похожа переданная, а затем сравнивать их (вдруг переданная не из нашего множества вообще).
Нет, это горизонтальное масштабирование, а не BigData.

Information

Rating
Does not participate
Location
Брест, Брестская обл., Беларусь
Date of birth
Registered
Activity