Elm <~ FRP ~ Magic

Добрался до Web:) А именно до Elm, который построен на идиоме функционального реактивного программирования. Это такой подход в котором с одной стороны функциональная чистота и декларативность, а с другой удобность построения интерактивного графического интерфейса. Вещи, которые могут изменятся, представляются в виде сигналов. А вся программа представляется в виде pure functional зависимостей между сигналами.

Erlang: Dynamic vs Static

Имел как-то я неосторожность обмолвится, что Erlang — не совсем динамически типизирован, даже немножко статически.

Но давайте смотреть.

Матан для лямбда-исчисления

Интересная и очень полезная вещь мне открылась в Haskell.

Разбираясь с Cont монадой, я не мог понять, почему первое приближение оператора bind в виде простой аппликации плохое, то есть:

m >>= f = m f

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

m >>= f = \k -> m (\a -> f a k)

Мне хотелось быстро сравнить два подхода и понять предельно чисто, где кроется суть. Но как? И тут пришло просветление. Нужно как в матане перебрать все варианты аргументов и посмотреть какие будут результаты.

Легко и непринужденно пишем Regex

Итак мы уже поняли зачем Эрик использует список и ничто нам не мешает двигаться дальше. Как вы уже знаете парсер имеет тип Parser a, где a – это тип значения, которое может вернуть парсер, если ему скормить строку, а что если a – это Parser 'a, то есть все целиком имеет тип Parser (Parser a)?

Why laziness matters

По мотивам лекции. Там Эрик пишет функциональный парсер, а для типа возвращаемого значения использует список. Я решил углубиться в реализацию, поэкспериментировать, начал писать, но не имея понятия зачем там список, решил использовать Maybe.

Как я на Erlang'е OOP делал

Написал в учебных целях утилиту для разбора build-output'а (Visual Studio/Incredibuild). Код тут.

Uniqueness types in Agda

Сразу линк. Данная реализация уникальных типов на Agda базируется на явном управлении контекстом. Каждый оператор рассматривается как преобразователь контекста (Transformer в коде). Преобразователь характеризуется сигнатурой (Types) входа (то, что он употребляет, consumes, и удаляет с контекста) и сигнатурой выхода (то, что добавляет в контекст).