Russian Lambda Planet

23 февраля 2017

Максим Сохацкий

Actario: A Framework for Reasoning About Actor Systems

Shohei Yasutake, Takuo Watanabe

Coq:
CoFixpoint behvA := receive (fun msg ⇒
match msg with
| name_msg sender ⇒ me ← self; sender ! name_msg me; become behvA
|_⇒ child ← new behvB; child ! msg; become behvA
end)

Erlang:
behvA() → receive Msg → case Msg of
{name_msg, Sender} → Me = self(), Sender ! {name_msg, Me}, behvA()
     _ → Child = spawn(fun() → behvB() end), Child ! Msg behvA()
end.

_______________
[1] http://amutake.github.io/actario/AGERE2015.pdf

23 февраля 2017, 03:50

22 февраля 2017

Максим Сохацкий

CoFixpoint Extraction REPL Prototype Zero

Ну что, я таки нанписал CoFixpoint корекурсию на коке. Точнее сразу REPL для коиндуктивного типа. No OCaml was involved.
$ brew install opam
$ opam install coq
$ opam install coq-io-system

Быстрый старт предполагает наличие всех необходимых opam модулей, которые в предыдущих постах я рассказал как насетапить, а если и не рассказал, то показал какие из них необходимые.
$ git clone git://github.com/5HT/co && cd co
$ make && cd extraction && make && ./main.native
ocamlbuild main.native -use-ocamlfind -package io-system
Finished, 5 targets (5 cached) in 00:00:00.
1
Input: 1.
2
Input: 2.
3
Input: 3.
CTRL-D


Что тут происходит, тут происходит нативный с точки зрения пи калкулуса процесс квантификации операционной бесконечности, комонада спрятаная внутри тайпчекера кока, преобразует корекурсию в потенциально бесконечный процесс на OCaml.

Здесь не используются никакие биндинги, кроме Lwt.

$ cat Main.v
Require Import Coq.Lists.List.
Require Import Io.All.
Require Import Io.System.All.
Require Import ListString.All.
        Import ListNotations.

  CoInductive Co (E : Effect.t) : Type -> Type :=
    | Ret   : forall (A : Type) (x : A), Co E A
    | Bind  : forall (A B : Type), Co E A -> (A -> Co E B) -> Co E B
    | Call  : forall (command : Effect.command E), Co E (Effect.answer E command)
    | Split : forall (A : Type), Co E A -> Co E A -> Co E A
    | Join  : forall (A B : Type), Co E A -> Co E B -> Co E (A * B).

  Arguments Ret {E} _ _.
  Arguments Bind {E} _ _ _ _.
  Arguments Call {E} _.
  Arguments Split {E} _ _ _.
  Arguments Join {E} _ _ _ _.

  Definition ret   {E : Effect.t} {A : Type} (x : A) : Co E A := Ret A x.
  Definition split {E : Effect.t} {A : Type} (x1 x2 : Co E A) : Co E A := Split A x1 x2.
  Definition join  {E : Effect.t} {A B : Type} (x : Co E A) (y : Co E B): Co E (A * B) := Join A B x y.
  Definition call  (E : Effect.t) (command : Effect.command E):
                   Co E (Effect.answer E command) := Call (E := E) command.

  Notation "'ilet!' x ':=' X 'in' Y" := (Bind _ _ X (fun x => Y))
           (at level 200, x ident, X at level 100, Y at level 200).

  Notation "'ilet!' x : A ':=' X 'in' Y" := (Bind _ _ X (fun (x : A) => Y))
           (at level 200, x ident, X at level 100, A at level 200, Y at level 200).

  Notation "'ido!' X 'in' Y" := (Bind _ _ X (fun (_ : unit) => Y))
           (at level 200, X at level 100, Y at level 200).

  Definition read_line : Co effect (option LString.t) :=
    call effect ReadLine.

  Definition printl (message : LString.t) : Co effect bool :=
    call effect (Print (message ++ [LString.Char.n])).

  Definition log (message : LString.t) : Co effect unit :=
    ilet! is_success := printl message in
    ret tt.

  Definition run (argv : list LString.t): Co effect unit :=
    ido! log (LString.s "What is your name?") in
    ilet! name := read_line in
    match name with
      | None => ret tt
      | Some name => log (LString.s "Hello " ++ name ++ LString.s "!")
    end.

  Parameter infinity : nat.
  Parameter error : forall {A B}, A -> B.

  Fixpoint eval_aux {A} (steps : nat) (x : Co effect A) : Lwt.t A :=
    match steps with
      | O => error tt
      | S steps =>
        match x with
          | Ret _ v => Lwt.ret v
          | Call c => eval_command c
          | Bind _ _ x f => Lwt.bind (eval_aux steps x) (fun v_x => eval_aux steps (f v_x))
          | Split _ x1 x2 => Lwt.choose (eval_aux steps x1) (eval_aux steps x2)
          | Join _ _ x y => Lwt.join (eval_aux steps x) (eval_aux steps y)
        end
    end.

  Definition eval {A} (x : Co effect A) : Lwt.t A :=
    eval_aux infinity x.

  CoFixpoint handle_commands : Co effect unit :=
    ilet! name := read_line in
    match name with
      | None => ret tt
      | Some command =>
        ilet! result := log (LString.s "Input: " ++ command ++ LString.s ".") in
        handle_commands
    end.

  Definition launch (m : list LString.t -> Co effect unit): unit :=
    let argv := List.map String.to_lstring Sys.argv in
    Lwt.launch (eval (m argv)).

  Definition corun (argv : list LString.t): Co effect unit :=
    handle_commands.

  Definition main :=
    launch corun. (* launch run. *)

Extract Constant infinity => "let rec inf = S inf in inf".
Extract Constant error => "fun _ -> failwith ""Unexpected end""".
Extraction "extraction/main" main.


Это то что мы ребятки называем основой верифицированного ядра операционной вычислительной среды для моделирования пи калкулуса и доказательства его основных теорем о бисимуляции, модальных логик и верификации протоколов, и просто для тестирования любых математик в интерактивной среде со своим простым интерпретатором. Наша цель создать единую среду для работы математиков и программистов, где экстракты моделей сразу линкуются с высокопроизводительным CAS рантаймом и CPS интерпретатором. Проверяйте ваши датасеты сразу на моделях заэкстракченых в Rust или OCaml, которые запускаются на seL4, Xen или Mac/Linux. Такой стартап, дали бы денег? :-)

22 февраля 2017, 22:38

nponeccop

Объектоидный макропаскаль

Пришла в голову идея реально упоротого языка синтаксиса. Берём hn0 и переставляем местами функцию и её первый аргумент:
l foldl cons nil =
	acc = nil
	while l neq null
		acc := acc cons (l data) 
		l := l next
	acc
Трансляция в функциональный ЖС:
function foldl(l, cons, nil) {
	let acc = nil 
	while (l != null) {
		acc = cons(acc, data(l))
		l = next(l)
	}
	return acc
}
Преимуществ как минимум два: бесплатные инфиксные операции и автокомплит в объектном стиле. Трансляция в объектный ЖС:
function foldl(l, cons, nil) {
	let acc = nil 
	while (l.neq(null)) {
		acc = acc.cons(l.data())
		l = l.next()
	}
	return acc
}
Но это конечно же не объекты, а что? Пусть будут объектоиды! Ещё у нас все ФВП это макросы, а ":=" и общая убогость - как в паскале. Оружие массового поражения!

Лексический синтаксис любой можно налепить. Хоть как в жс.

22 февраля 2017, 21:49

Влажные мечты о категорной имплементации математики

У меня давно была мечта - чтобы было такое компактное здание математики, где определения и теоремы даются в одну строчку из более общих. Не важно в каком виде (формального текста, естественного текста, интерактивной тулзы).

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

Сегодня столкнулся с проблемой, что в Coq нет доки по структурной коиндукции и коиндуктивным типам.

Нет чтобы просто сказать, что СЕПУЛЬКАРИИ — устройства для сепуления структурная корекурсия встроена в ядро, продуктивность фикспоинтов коалгебр постулируется, а ключевое слово CoFixpoint просто говорит коку, что дальше у нас Мю Ню и коалгебра.

Вместо этого у них целый туториал как официальная дока, где рассусоливают на 5 страницах что-то про guardedness. Тьфу на них.

22 февраля 2017, 20:56

21 февраля 2017

Anton Salikhmetov

arXiv:1702.06092 [cs.LO]

https://arxiv.org/abs/1702.06092

Parallel needed reduction for pure interaction nets

Reducing interaction nets without any specific strategy benefits from constant time per step. On the other hand, a canonical reduction step for weak reduction to interface normal form is linear by depth of terms. In this paper, we refine the weak interaction calculus to reveal the actual cost of its reduction. As a result, we obtain a notion of needed reduction that can be implemented in constant time per step without allowing any free ports and without sacrificing parallelism.

comment count unavailable comments

21 февраля 2017, 04:27

20 февраля 2017

ru_declarative

Учебник теории категорий, версия 9

Видимо, на этом закончу, 400 страниц достаточно. Сделал гиперссылки и закладки

https://github.com/George66/Textbook

написал Георгий 20 февраля 2017, 18:23

ru_lambda

Учебник теории категорий, версия 9

Видимо, на этом закончу, 400 страниц достаточно. Сделал гиперссылки и закладки

https://github.com/George66/Textbook

написал Георгий 20 февраля 2017, 17:59

nponeccop

Structural Induction and Coinduction in a Fibrational Setting

Кругом одни фибрации! (Или как это по-русски?)

Чуваки категорно сформулировали (ко)индукцию для полиномиальных эндофункторов

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.7400

20 февраля 2017, 16:44

18 февраля 2017

David Sorokins WebLog

Демо-тест распределенной имитации на монадах

Создал тестовый демонстрационный пример распределенной дискретно-событийной имитации на основе своего нового продукта AivikaSim. Тест легко воспроизвести по приведенной инструкции:

https://github.com/dsorokin/aivikasim-distributed-test

Код написан на языке Haskell, но для воспроизведения теста язык программирования знать не требуется.

Для реализации мне очень помогла платформа Cloud Haskell, разработчикам которого хочу выразить отдельную благодарность.

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

Особая фишка в том, что узлы можно размещать, используя ненадежные соединения и обычные компьютеры. То есть, теоретически кластер может состоять из машин, расположенных в разных континентах, но вопрос тогда только в том, насколько быстро будет идти имитация, потому что для целей тестирования там сознательно создается очень много сообщений. Происходят постоянные откаты назад и попытки заново обработать дискретные события, потому как реализован оптимистичный алгоритм «деформации времени» (Time Warp).

Если возникнет кратковременная потеря связи на минуту или две, а я в своих тестах просто на время выдергивал Ethernet-кабель, то распределенная имитация должна сама себя излечить после восстановления связи. В принципе, время потери связи может быть и значительно дольше, но тогда надо подкрутить внешние параметры запуска.

Только стоит заметить, что восстановление имитации на Linux и macOS работает как часы, а вот на Windows немного похрамывает, но, видимо, это связано с тем, что у Haskell-сообщества Unix-системы приоритетнее, что скорее хорошо.

По приведенной ссылке лишь скромный небольшой демонстрационный пример, показывающий возможности системы AivikaSim. 

написал dsorokin (noreply@blogger.com) 18 февраля 2017, 15:29

Максим Сохацкий

Топология на 10 LOC. Определение

Definition subset (A : Type) (u v : A -> Prop) := (forall x : A, u x -> v x).
Definition union (A : Type) (B : (A -> Prop) -> Prop) := fun x : A => exists U, B U /\ U x.
Definition inter (A : Type) (u v : A -> Prop) := fun x : A => u x /\ v x.
Definition empty (A: Type) := fun x : A => False.
Definition full (A: Type) := fun x : A => True.

Structure topology (A : Type) := {
          open :> (A -> Prop) -> Prop;
          empty_open: open (empty _);
          full_open: open (full _);
          inter_open: forall u, open u -> forall v, open v -> open (inter A u v) ;
          union_open: forall s, (subset _ s open) -> open (union A s) }.

18 февраля 2017, 15:02

nponeccop

Прогресс по SVG-чартам

https://bl.ocks.org/streamcode9/raw/9fc767e29414c2d90f77da4799b9fdf0/

Проверяйте, у кого там палочки пропадали при быстром драге на андроиде!

18 февраля 2017, 05:06

Про F-алгебры из ТК

Потихоньку врубаюсь в алгебры.

Похоже что Fix это инициальная алгебра а unfix терминальная коалгебра, и оба этих случая являются свободными конструкциями.

инициальная алгебра + терминальная коалгебра = refix
алгебра + терминальная коалгебра = cata
инициальная алгебра + коалгебра = ana
алгебра + коалгебра = hylo

18 февраля 2017, 05:04

17 февраля 2017

Максим Сохацкий

Основні Поняття

Задание. На завтра нужно составить 5 возможных вариантов тайтла диссертации. Нужно быть максимально абстрактным, чтобы это было 5 корней возможной вереницы пайвотов но проникали в самую суть и кардинально решали или упрощали существующие процессы верификации ПО.

Моя суть выражается просто: испльзоваьт только три вершины лямбла куба и показать что System F / STLC, Pw и Untyped Lambda Core достаточно для пострения единой, плотно связаной и компактной системы включающей в себя полный цикл, от формулировки теорем до среды выполнения. Если идея вам кажется слишком безумной, то вот аналогичные проекты [1], и все варианты копания в метациркулярность тоже связаны с построением такого типового комплекса.

Вполне понятно что в этом комплексе нет места Сишечке, LLVM, seL4, Haskell, Scala и прочей ереси. О интертпретатор (нижний уровень, написанный на Rust) вам демонстрировался в этом журнале, жалко что проект возможно так и останется закрытый. Ядро (ОМ) уже написано. HNC и EXE как языки верхнего уровня которые шарят единую библиотеку, но имею принципиально разнын таргеты. EXE экстрактит в О написанный на EXE. А HNC экстрактит в LLVM.

Основні Поняття

Верифікація Програм (verification).
Доведення Теорем (theorem proving).
Обчислювальне середовище (runtime).
Система ефектів (effect system),
Система Користувача (user intput system).
Лінивий Інтерпретатор (continuation passing style interpreter).
Безтипового Лямбда Числення (untyped lambda calculus).
Базова Бібліотека (base library).
Гомотопічна Бібліотека (homotopic library).
Система доведення теорем (automated theorem prover).
Компіляція (compilation).
Реконструкція (reconstruction).
Редукція (reduction).
Модель потоку виконання (control flow graph).
Теорія Категорій (category theory).
Категоріальна семантика (categorial semantics).
Лямбда кодування (lambda encoding).
Обчислювані функції (computable function).
Лямбда числення (lambda calculus).
Екстракція программ (code extraction).
Абстрактне синтаксичне дерево (abstract syntax tree).

Вот такая палитра, если хотите докинуть, милости просим. Кто ебанет тайтл, за того молитву закажу, а кто ебанет тайтл который пойдет в дисер возьму в соавторы :-)

______________________________________
[1]. https://www.cl.cam.ac.uk/~mom22/itp11.pdf

17 февраля 2017, 17:37

16 февраля 2017

nponeccop

HNC опять похудел

Люблю такие коммиты! Больше строк богу удалённых строк!

[master 8f1d72b] Refactor: TH-generated HN.Intermediate.ExpressionF
2 files changed, 7 insertions(+), 22 deletions(-)

Чуваки написали TH-код, который делает в точности те 15 строк бойлерплейта, которые у меня были. Даже имена те же самые (почти, в одном месте у меня суффикс Functor, а у них F).

16 февраля 2017, 20:40

Полку кметтов прибыло

https://github.com/sjoerdvisscher

Нашёл у него потенциально полезную штуку http://hackage.haskell.org/package/algebraic-classes

Ещё free-functors например. Мне понравилось определение непустых списков как свободных полугрупп:
import Data.Functor.Free
import Data.Semigroup

-- A free semigroup allows you to create singletons and append them.
-- So it is a non-empty list.
type NonEmptyList = Free Semigroup

-- These instances make NonEmptyList a Semigroup and Show-able, Foldable and Traversable.
deriveInstances ''Semigroup
Я кончил! © Домнин Ф.А.

16 февраля 2017, 19:25

Максим Сохацкий

Coq.io Effect System

Module Effect.
  Record t := New {
    command : Type;
    answer : command -> Type }.
End Effect.

Inductive command : Type :=
| Print (message : LString.t)
| ReadLine.

Definition answer (c : command) : Type :=
  match c with
  | Print _ => unit
  | ReadLine => LString.t
  end.

Definition effect : Effect.t :=
  Effect.New command answer.

Module Computation.
  Inductive t (E : Effect.t) : Type -> Type :=
  | Ret : forall (A : Type) (x : A), t E A
  | Call : forall (command : Effect.command E), t E (Effect.answer E command)
  | Let : forall (A B : Type), t E A -> (A -> t E B) -> t E B
  | Choose : forall (A : Type), t E A -> t E A -> t E A
  | Join : forall (A B : Type), t E A -> t E B -> t E (A * B).
End C.

16 февраля 2017, 14:42

Coq.io

$ brew install opam
Warning: opam-1.2.2_2 already installed

$ opam install coq

=-=- Synchronising pinned packages =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[NOTE] Package coq is already installed (current version is 8.6).

$ opam repo add coq-released https://coq.inria.fr/opam/released

$ opam install -j4 -v coq-io-system

$ export PATH=~/.opam/system/bin:$PATH

$ opam list | grep coq-io
coq-io                  3.1.0  A library for effects in Coq.
coq-io-hello-world      1.1.0  A Hello World program in Coq.
coq-io-system           2.3.0  System effects for Coq.
coq-io-system-ocaml     2.3.0  Extraction to OCaml of system effects.

$ cat src/Main.v
Require Import Coq.Lists.List.
Require Import Io.All.
Require Import Io.System.All.
Require Import ListString.All.

Import ListNotations.
Import C.Notations.

Definition run (argv : list LString.t)
  : C.t System.effect unit :=
  let! _ : unit * unit := join
    (System.log (LString.s "Hello"))
    (System.log (LString.s "World")) in
  ret tt.

Definition main := Extraction.launch run.
Extraction "extraction/main" main.

Module Run.
  Import Io.Run.
  Definition run_ok (argv : list LString.t)
    : Run.t (run argv) tt.
    apply (Let (Join
      (Run.log_ok (LString.s "Hello"))
      (Run.log_ok (LString.s "World")))).
    apply Ret.
  Defined.
End Run.


$ cat Make
-R src repl

src/Main.v

$ coq_makefile -f Make -o Makefile

$ make
COQDEP src/Main.v
COQC src/Main.v

$ cat extraction/Makefile
build:
	ocamlbuild main.native -use-ocamlfind -package io-system
clean:
	ocamlbuild -clean

$ cd extraction && make

$ make
ocamlbuild main.native -use-ocamlfind -package io-system
Finished, 5 targets (0 cached) in 00:00:01.

$ ./main.native
World
Hello

16 февраля 2017, 14:39

14 февраля 2017

Максим Сохацкий

Запретить коммутативные объекты

"...Вот почему бурбакистская мафия, заменяющая понимание науки формальными манипуляциями с непонятными „коммутативными“ объектами, так сильна во Франции, и вот что угрожает и нам в России."

Вестник РАН, В.Арнольд, 2002. — Т. 72, № 3. — С. 245-250

Вот почему Теоркат не читался в СССР :-)

14 февраля 2017, 10:50

13 февраля 2017

Максим Сохацкий

Личинка Тополога



Новые поступлению на http://ns.synrc.com/publications/cat/Topology/
__________________
A Concise Course in Algebraic Topology.pdf
Aleksandryan,Mirzakhanyan. Basic Topology.pdf
Categorical homotopy theory.pdf
Nonabelian Algebraic Topology.pdf
On the category of groupoids.pdf
Representing Topoi by Topological Groupoids.pdf
Sheaves in Topology.pdf
TOPOLOGY AND GROUPOIDS.pdf
Topological groupoids.pdf
Алгебраическая топология.pdf

Falconer K. Fractal geometry.djvu
Halmosh P. Gilbertovo prostranstvo v zadachah (Mir, 1970) (.djvu
Klingenberg V. Lekcii o zamknutyh geodesicheskih (Mir, 1982.djvu
Борисович. Введение в топологию.djvu
Бухштабер, Панов. Торические действия в топологии и комбинаторике.djvu
Гельфанд, Манин. Методы гомологической алгебры.djvu
Годеман. Алгебраическая топология и теория пучков.djvu
Гротендик. О некоторых вопросах гомологической алгебры.djvu
Дольд. Лекции по алгебраической топологии.djvu
Картан, Эйленберг. Гомологическая алгебра.djvu
Кураторвский. Топология 1.djvu
Лекции об икосаэдре и уравнении пятой степени(Клейн).djvu
Милнор. Дифференциальная топология.djvu
Рохин, Фукс. Начальный курс топологии.djvu
Серр. Когомологии Галуа.djvu
Хьюзмоллер. Расслоённые прстранства.djvu

13 февраля 2017, 18:30

10 февраля 2017

nponeccop

Очередное прозрение

Для начала договоримся о терминах (это ещё не прозрение). Будем говорить, что катаморфизм Х - это применение алгебры Х к Х. Ну чтобы не упоминать эти базовые функторы каждый раз. Например катаморфизм списков применяет алгебру списков к спискам.

Алгебры бывают двух типов - обычные и в кодировке Чёрча. Алгебра натуральных чисел в кодировке Чёрча - это a -> (a -> a) -> a. Обычная алгебра натуральных чисел - это Maybe a -> a.

Прозрение заключается в том, что все функции, принимающие a -> (a -> a) можно отрефакторить в функции, принимающие Maybe a и наоборот. Более того, из a -> (a -> a) -> b всегда можно получить Maybe a -> b и наоборот (т.е. выходной тип не обязан быть a)

Ну и это работает для всех Х. Т.е. списочные алгебры аналогично обобщаются. Функции принимающие (a -> b -> b) эквивалентны функциям принимающим ListF a b = Cons a b | Nil (нерекурсивный базовый функтор списков)

Upd: тут подумалось что катаморфизмы не при чём. Просто тип Maybe a взаимозаменяем со своей "недочёрч-кодировкой" (b, a -> b). Аналогично тип ListF a b взаимозаменяем c (b, a -> b -> b). Ну и чёрч-кодировки нерекурсивных типов встречаются очень часто, и части тапла могут быть не рядом в списке аргументов.

Ну и море разливанное.

insertWith :: Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a

Здесь у нас затесалось data Tree = Node Tree Tree | Leaf, а точнее его базовый функтор.

Любопытное обнаружилось объяснение единственности id: это черч-кодировка бесконечного стрима юнитов, который всего один. А разные функции a -> a - это разные свёртки этого бесконечного стрима. Т.е. разные термы cata phi $ replicate () :) Как-то неправдоподобно, неужели правда

10 февраля 2017, 03:32

09 февраля 2017

nponeccop

Коан по ТК, комбинаторному исчислению и System F

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

Глава 100509 Обфускатор брейнфака путём оптимизирующей компиляции в бессмысленное подмножество хаскеля.

Это очень большой квест (хотя и прошлые по многу человеколет), так что дизайн лишь в общих чертах.

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

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

Парсинг не обязателен, считаем что код сразу на EDSL написан. Если делать - то как осмысленную тулзу.

Далее переводим интерпретатор в SKI-базис: const, <*> и id, не считая декодера, и у нас готова так сказать базовая рантайм-библиотека.

Успехом этого этапа можно считать мандельброт на брейнфак-EDSL на SKI с контролем эффектов.

Т.е. файл на хаскеле содержащий интерпретатор эффектов, код на едсл и реализацию самого едсл на SKI-подмножестве. В репе также будут написанные тулзы (обфусцировать и тулзы это уже изврат, наша же цель не изврат а путь к просветлению).

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

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

Код для бессмысленных конструкций можно прямо с хакаджа брать, либы вроде Kan-extensions даже обфусцировать не надо. Утверждает конструкции как бессмысленные "учитель", то есть я (но какой из меня учитель - я максимум могу подсказать с какого края подступиться).

Общие принципы - newtype, тайпклассы и семейства разрешены, если тела разрешены.

Тела разрешены если не используют типов-сумм и произведений (но произведения в исключительных случаях разрешены - например ну на сколько обессмыслит этот формально запрещённый тип третьего ранга кодировка Чёрча? По-моему и так достаточно бессмысленно! (запрещён он потому что тип-произведение а произведения "понятны")

data Ran' g h a = forall z. Functor z => Ran' (forall x. z (g x) -> h x) (z a)

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

В конце концов по мере добавления абсурдных конструкций у нас должен замозародиться EDSL а ля Хагино, пусть и с семантикой брейнфака.

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

09 февраля 2017, 18:36

08 февраля 2017

Максим Сохацкий

Стримы, Стейджинг и Краруп Эрланг

Кароче счас центральная тема у всех вокруг — это стрим процессинг. Это тот же LISP но в другой своей, теортетико-типовой ипостаси. Понятно что стрим процессинг на лиспе выглядит как ад, и даже кложа не спасает, поэтому нужны типы. Я не буду счас касаться высокотехнологичных штук типа MMX,SSE,AVX векторизаций, скажу только что если вам парят стрим процессинг без вот этого всего хаскелевского задротства — шлите такие стримы нахуй. Например Go именно поэтому и соснет хуйцов. Что у нас остается?

С++, Rust, Haskell — это то где сразу тебе векторизация бесплатная
Scala/Java/JVM, F#/C#/CLR — по сути JIT интерпретаторы, но тоже векторизируют

В остальных либо нет типов, либо не векторизируют (если забыл кого пишите в каментах).

Дошли стримы и до эрланга и эликсира. Приезжал к нам в Киев Жозе Валим (он кстати обиделся на меня за упоминание фашистского марша в Бразилии в посте сравнении Феникса и N2O :) и рассказывал про GenStage, в Scala это Akka-stage. Придумали видно какие-то мега архитеткоры, которые решили а давайте запилим DSL, в котором будем как сантехники рисовать Flow и указывать размеры буферов с бекпрешуром и прчими настройками. Идея вроде здравая, пока не начинаешь читать код реализации.

Анатомия стрим процессинга:

— Код (стрим комбинаторы, FSM или ваша lazy программа)
— Данные (буфер или виртуальная сущность в памяти которая хранит стрим, может быть например BTree дерево)
— Топология системы очередей (которая связывает реальные хранилища, штука где невозможен Zero-Copy и нужно распаковать один стрим чтобы запаковать в другой в другой области памяти), собственно эту задачу и решают stages комбинатооры.

Как работает стейджинг

Обычно во всех имплементациях лепят просто мемори буфер между физическими очередями ну и со своим async протоколом, потому что если sync то нахуй этот стейджинг тогда бы сдался. Но это все мне напоминает какой-то ад. Очередя это и так буфера. Зачем на каждое сопряжение Out-In выделять дополнительный буфер, если и так можно все разрулить? Или у математиков есть возражения по этому поводу? Протокол бекпрешура можно делать глобальный для всех Акторов вашего Flow, и забивать клиенские буфера при любых отказал на любом из стейджей.

Кроме того незнаю нахуя ввообще тюнить эти буфера, тщательно подбирая их размеры под каждый поток данных. Ведь есть теория, которую расписал еще Краруп, которая позволяет посчитать емкость системы для любой системы очередей и расставив счетчики, можно сразу определять пытаться форсить по глобальному протоколу эти сообщения или сразу начать забивать клиентские буфера (у нас в ПТУ-бурсе КПИ даже это рассказывали на курсе Теория Массового Обслуживания, я не говорю уже об университетах типа EPFL).

Кароче мне кажется тут ад и пиздец именно от того, что еще ни один чувак не сделал систему которая тебе при твоей схеме данных и частоты процессора и битрейта сети сразу показывает емкость системы для вашей картинки из GraphDSL? Сразу говорит где боттлнеки и где можно стримы сплитить, чтобы сделать их паралельную обработку (как это делает например Rayon в Rust).

Но нет блядь, распаралеливание стримов на ядра не под силу ни одной базовой библиотеке ни одного языка. Даже в Rust — это отдельный crate, но там идеология такая, что ВСЕ должно быть отдельным крейтом, так что это вроде как простительно. Есть либы которые распаралеливают это на ноды (машины), но вы себе можете представить их качество и количество заюзаных буферов там!

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

Вот я тут набросал топологию для системы очередей паралельной и последовательной (символы-трейдеры) сборки буков шардированой по символам:



Какие могут быть вообще буфера в real-time системах? Никаких! Система сама должна сказать где будет ботлнек и просчитать теоретическую емкость которая не может отличается от фактической больше чем на эпсилон. Если она этого не делает — она мне не конкурент.

08 февраля 2017, 23:58

06 февраля 2017

nponeccop

Делаем ставки, господа

Я как-то говорил, что у меня ломается всё. Поломал тайпскрипт и он сгенерировал ill-scoped code который крешится:

https://github.com/Microsoft/TypeScript/issues/13893

06 февраля 2017, 03:52

Игры для программистов

http://dirk.rave.org/combinatris/ - а какие ещё есть? Core wars наверное считается.

06 февраля 2017, 02:12

05 февраля 2017

nponeccop

Декларативная геометрия

Надрачиваю тут уже третий день на аффинные пространства. Потому что в отличие от нахуй не нужных (мне) линейных, аффинные описывают over 80% всего что я вообще когда-либо делал с дробными числами.

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

Базисы из n+1 точек это вообще бомба - наконец внятный единообразный способ описания композиции "линейных" завивимостей ax + b. Например обнаружил, что пространство параллельных переносов и масштабирований как аффинное - одномерно независимо от количества координат у точек, поскольку является прямым произведений одномерных. Скажем, для описания параллельного переноса с масштабированием в моем проекте графиков надо 4 точки, а не 6. И в стомерном случае тоже 4.

05 февраля 2017, 03:27

04 февраля 2017

nponeccop

Сияние базисных симплексов

https://github.com/streamcode9/svg-time-series/blob/master/draw.ts

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

04 февраля 2017, 23:21

ru_declarative

абстрактный язык программирования процессора

Интересно, существуют ли учебники по языкам процессора вообще, то есть в которых описываются общие свойства языков процессора. Под языком процессора я подразумеваю ассемблер, машинный код. Конечно, в учебнике должны быть описаны и конкретные языки процессора в качестве примеров, но не полностью, чтобы не раздувать его ненужными деталями. Я полагаю, в качестве примеров можно взять Intel x86 и какой-нибудь RISC, например, ARM.

написал beroal 04 февраля 2017, 05:43

01 февраля 2017

nponeccop

Декларативная геометрия

люди, я тут решил стать алгебраическим композабельным геометром, отцом бескоординатных 2д-фронтэндов для векторного WebGL фидонета.

не подскажете какие-нибудь пейперы или книжки для школьников по мат. основам diagrams c hackage? У них референсов я не нашёл, но должно же быть

ну и вообще по теме отвязывания графики от координат и перехода к высокоуровневым представлениям, не обязательно в разрезе diagrams

Нашел тут пейпер.

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.220.4802

В-общем, от линейных пространств переходим к аффинным, а от них к геометрической алгебре (не путать с алгебраической геометрией).

01 февраля 2017, 00:04

31 января 2017

Anton Salikhmetov

Лямбды на веревочках в командной строке

https://www.npmjs.com/package/@alexo/lambda

$ npm install -g @alexo/lambda
└── @alexo/lambda@0.1.6 

$ lambda -e 'S hello bye world'
hello world (bye world)
$ lambda -de 'x: (x: x) v1 x'
\read_{[ ]}(\print) = \lambda(w1, \apply(\apply(\lambda(w2, w2), \atom_{v1}), w1));
\apply(\apply(\lambda(w2, w2), \atom_{v1}), \atom_{v2}) = \read_{v2: [ ]}(\print);
\apply(\lambda(w2, w2), \atom_{v1}) = \lambda(\atom_{v2}, \read_{v2: [ ]}(\print));
\lambda(w2, w2) = \lambda(\atom_{v1}, \lambda(\atom_{v2}, \read_{v2: [ ]}(\print)));
\lambda(\atom_{v2}, \read_{v2: [ ]}(\print)) = \atom_{v1};
\atom_{v2} = \read_{v1 [ ]}(\read_{v2: [ ]}(\print));
\read_{v2: [ ]}(\print) = \atom_{v1 v2};
\print = \atom_{v1};
$ npm explore -g @alexo/lambda -- sh test.sh
SAMPLE             NORMAL          CLOSED         OPTIMAL        ABSTRACT
counter             54(7)           58(6)          145(4)             N/A
w2eta             125(20)         137(16)          208(7)           38(7)
22210ii               N/A       1740(182)        7918(70)         732(70)
3222ii                N/A       5896(545)      164474(43)        1183(43)
1022ii                N/A     23026(2085)     2490504(59)        4299(59)
4222ii                N/A 1442259(131124)             N/A      262402(64)
222210ii              N/A 6685119(655415)             N/A    2359813(201)
cfact4         8605(1028)      18606(887)      96676(691)      13985(691)
yfact4        92395(4833)     53519(1741)     659727(760)      16611(760)
cfact5      170958(16917)   895848(16170)  5906411(13462)   287527(13462)
yfact5      783031(43651)  1371216(22267)             N/A   291418(13550)
$ 


comment count unavailable comments

31 января 2017, 23:33

30 января 2017

ru_declarative

абстрактные методы решения задач

Сразу оговорюсь, что это не вопрос, а тема для обсуждения. Метод «разделяй и властвуй» все мы знаем. Есть ещё что-то на таком же абстрактном уровне? Примеры от меня.

Нужно найти неподвижную точку функции f. Пусть x — такая последовательность, что x(succ(n)) = f(x(n)). Находим такое наименьшее n, что x(succ(n)) = x(n). Говоря неформально, вычисляем последовательность, пока она не стабилизируется.

Частный случай предыдущей задачи, где f определена на векторах. (Вектор — это функция, определённая на некотором множестве V.) Здесь тоже вычисляем последовательность «недорешений» x. Параллельно вычисляем такую последовательность с, что ∀n ∀v v∈c(n) ↔ x(n)(v) = f(x(n))(v). с показывает, в каких точках x(n) «решён». Комплемент к этому множеству называется «agenda». x(succ(n)) вычисляем следующим образом. Выбираем «нерешённый» (принадлежащий agenda) u. Для всех v, если v=u, то x(succ(n))(v) = f(x(n))(v), иначе x(succ(n))(v) = x(n)(v). Другими словами, на одном шаге «решаем» один элемент вектора. c(succ(n)) вычисляется хитро, потому что изменение элемента вектора может сделать другие элементы «нерешёнными». Полное и формальное описание алгоритма могу привести, если кому-то надо.

Прикладные варианты этой задачи — алгоритмы на графах (V — множество вершин графа) (reachability, наиболее короткий путь), дедукция «снизу» (chart parser).

написал beroal 30 января 2017, 08:20

27 января 2017

Ратибор

Я сотворил Ничто

Небрежный плод моих забав №2 прошу любить и жаловать здесь: http://hackage.haskell.org/package/empty-monad-0.1.0.0

Если кратко - то это структура данных, в которой нет данных. Этот контейнер сразу забывает значение, которое в него засовывают. Обладает свойствами аппликативного функтора и монады, Foldable, Traversable и др.

27 января 2017, 11:39

26 января 2017

nponeccop

Хаскель для мудаков

Подумалось тут, что поскольку на хаскеле никто не пишет или пишет исчезающе малая доля народу, надо сделать учебник Хаскеля нового типа.

Учебник должен не учить писать на хаскеле (это всё равно не пригодится), а учить интеллектуальному опусканию других таких же неумёх в интернет-спорах. Интеллектуальному = давить интеллектом, а не эмоциями. По эмоциям отдельная книга нужна. Том 2.

В идеале книга не должна содержать ни строчки матана и ни строчки собственно хаскеля. Кому он интересен!

Главы должны быть театром абсурда, но нести некую мораль, упомянутую в эпиграфе к главе. Что-то среднее между коанами и идиотскими упражнениями в фильмах про китайские боевые искусства. ("Цель коана — придать определённый психологический импульс ученику для возможности достижения просветления или понимания сути учения")

В качестве лингвы франки я предлагаю 4 языка:

- K&R С
- ES7
- брейнфак
- регулярные выражения

С это если надо про работу с ячейками, брейнфак как всем известный пример нестандартной семантики с большим количеством реализаций (оптимизирующие компиляторы и т п), и ES7 как эталон высокоуровневости, регулярки как математический аналог K&R C (внутренний язык конечных автоматов).

Три главы Аж восемь глав я уже придумал (не обязательно первые или идущие последовательно).

Глава 100501. Описывается процесс написания на ES7 компилятора из брейнфака в graph reduction system из Плазмеер-Экелена и обратно.

Глава 100502. Описывается процесс написания на ES7 тайпчекера для GRS, в духе Х-М расширенного ПМ и мономорфной рекурсией, но используя подход статьи где с целью улучшения сообщений об ошибках собираются все констрейнты и в случае ошибки среди всех возможных неконсистентностей ищется минимальная.

Глава 100503. Описывается процесс разработки инструмента для поиска осмысленной программы на брейнфаке, не типизируемой после трансляции в GRS.

Глава 100504. Имплементация GRS наитупейшим образом без ячеек/стековых машин. Реализация call by name Scheme наитупейшим образом на санках. Описывается процесс поиска программы с разной асимптотикой при переходе от call by name к эмуляции call by need на GRS.

Глава 100505. Коан по boxing/universal variable representation/polymorphic recursion. Ещё не придумал.

Глава 100506. Коан по виртуальным машинам для редукции графов и тонкостям вроде G-machine blackholing. Ещё не придумал.

Глава 105007. Компилятор из брейнфака в регулярки. Поиск некомпилируемой программы.

Глава 100508. HTTP-сервер на нерасширенном брейнфаке но с внешним декодером на JS как пример кодировки эффектов. Кодирование эффектов в GRS палочкой, коданными, продолжениями, абстрактными монадами как в Х-е и свободными монадами.

26 января 2017, 22:37

Новости одним постом

1. У нас ночью +15 а в горах типа заморозки https://youtu.be/jrNWo3edkZU
2. https://github.com/begriffs/haskell-vim-now - потуга собрать все vim-плагины х-я в одном месте
3. Typescript Typings теперь модно прописывать в package.json как "@types/d3-request"
4. П. 3 требует TypeScript 2.0+ и мы трахались чтобы в студии встроенный ТС обновить. У одного обновилось а у второго старый npm почему-то. В проекте TypeScriptTools 2.1 прописаны.
5. В линуксе внезапно починили vim-youcompleteme и он дал семантические комплишены TS из коробки. То есть у переменной точку ставишь - методы светит. Даже в конце цепочки foo.bar().baz() и типы сразу показывает там же.
6. В SVG-чартах я запилил сияющее демо в benchmarks/path-draw-transform-d3, но теперь всё остальное надо переписывать, поскольку я столько поменял. В-общем, 60 фпс на десктопе
и 30-40 в мобильном хроме (а webview тормозит 2 фпс, и фф тоже 30 на десктопе, но это значительная победа по сравнению с конкурентами)
7. http://groupoid.space/hnc/ новая хоумпейж HNC, написал там несколько статей описания кишок, но maxim будет постепенно публиковать. Попутно выяснил что чекер можно ещё компактнее сделать - пока не
начнёшь объяснять кому-то сам не поймешь.
8. Начал лепить слайды по HNC в гуглодоках, макс потом на кошерные перелопатит. Англоязычных фпшников надо зазывать.
9. Есть тред по веб-фреймворку на Эрлаче: https://erlach.co/fp/6h9

26 января 2017, 00:46

20 января 2017

nponeccop

Прикладная фаллометрия

300 строк из 1700 занимают импорты и прагмы :)
$ grep -RE "^import |^INCLUDE|^{-# LANGUAGE " AG HNC.hs Utils.hs Setup.hs Bar.ag \
  HN CPP FFI Tools Utils Unifier Parser | wc -l
265
70 - сигнатуры типов. Притом, что я их не люблю, то есть, стоят только в особо мерзких местах:
$ grep -RIE '^[^ ]+ ::' AG HNC.hs Utils.hs Setup.hs Bar.ag HN CPP FFI Tools Utils Unifier Parser | wc -l
17 файлов, в которых есть декларации типов и инстансов:
$ grep -RIEl '^instance|^data |^DATA' AG HNC.hs Utils.hs Setup.hs Bar.ag \
  HN CPP FFI Tools Utils Unifier Parser | wc -l
17
Как правило, в этих файлах ничего кроме этих деклараций нет, разве что смарт-конструкторы и иные бойлерплейт-хелперы, которые заведомо просты и безбажны.

В файликах 611 строк. За вычетом 83 импортов и прагм (которые вошли в 265) получаем 1712 - (611 - 83) - 265 - 70 = 849 строк собственно хардкорной логики компилятора HNC :)

Ровно половина строк чистая декларативность. Ну не мечта ли поэта? Не об этом ли говорили классики?

20 января 2017, 21:52

19 января 2017

nponeccop

SPL/HNC 10 лет

Первый коммит в репе от inv2004 - в августе 2006
Первый пост в ЖЖ (ещё с перлом) - в августе 2007
Первый коммит от меня - в ноябре 2008
Даже перенос kashnikov репы с гуглокода на гитхаб - аж 5 лет назад.

Впрочем, основные работы были в 2010 году в Нигерии, когда я жарился в "офисе" без кондиционера, подключённом ethernet на скрутках и изоленте к EDGE-модему с 40 кбитами и 10000 мс пинга (450 первая миля).

Разработка ведётся "непрерывно, но эпизодически" - я быстро набросал скрипт, который показал что если посчитать уникальные месяцы, в которых был хотя бы один коммит - то получается аж 60 месяцев, 5 лет из 10.

19 января 2017, 19:13

TU и TV

Несмотря на то, что унификацию я вырезал, проблема двух эквивалентных представлений типов и конвертации туда-сюда никуда не делась.

Помимо модуля HN.MilnerTools, занимающегося Хиндли-Милнером, вышеупомянутой конвертацией и пост-процессингом выведенных типов для нужд C++, обнаружился модуль HN.TypeTools, работающий исключительно со "старым" представлением типов.

В этом старом представлении типопеременные есть двух видов - TU String и TV String. И в модуле TypeTools есть функция removeTU, которая тупо заменяет все встретившиеся TU на TV, а остальное оставляет как есть.

Обнаружилось, что эта removeTU вызывается только один раз из Root.ag, а там код, который вызывается только в начале или только в конце обработки AST атрибутной грамматикой. То есть, разного рода инициализации, препроцессинги и постпроцессинги атрибутов.

Выяснилось, что removeTU постпроцессит выход парсера FFI. Из этого парсера типы библиотечных функций поступают в чекер, ну и парсер генерит TU, а чекеру требуются TV. Тупо? Тупо, надо чинить!

Но тут выясняется, что парсер FFI у меня используется ещё в тестах, причём не только в тестах парсера FFI :) То есть, чтобы убрать лишнюю конвертацию, надо много всего перелопатить.

Чем завтра и займусь.

Upd: не мог заснуть, а проблема оказалась не столь большой. Починил. 7 files changed, 13 insertions(+), 18 deletions(-)

19 января 2017, 05:35

Разобрался с унификацией

Есть либа unification-fd, она же Control.Unification. В кои-то веки выпилил из HNC отдельно
стоящий унификатор:

https://github.com/nponeccop/HNC/blob/master/Unifier/Unifier.hs

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

Либа предоставляет функцию unify и её несиметричный вариант subsumes (проверяющий, можно ли второй терм получить из первого подстановкой). К сожалению, out of the box ими пользоваться затруднительно т.к. всё настолько генерическое, что компилятор не знает, какой инстанс нам нужен. Дизайн не ахти, буду писать письмо автору и думать что можно сделать.

В связи с чем пришлось написать бойлерплейт:

https://github.com/nponeccop/HNC/blob/master/Unifier/Restricted.hs

Я там просто импортирую unify с обобщённым типом и экспортирую её же, но уже с нашим конкретным.

Вот примерчик унификации:

https://gist.github.com/nponeccop/739a720582c961ab05991d61fb5cb598

Можно скопировать эти три файлика - они больше ни от чего не зависят - и поэкспериментировать с унификацией в репле. Типа runStack uni1 и runStack uni2

19 января 2017, 01:20

18 января 2017

nponeccop

Решил описать унификацию типов в HNC

В результате обнаружил, что там столь же дремучий лигаси, как был в парсере. Надо чистить конюшни!

Затрудняется это всё тем, что во-первых, в дизайне используемой библиотеки unification-fd пейпер на пейпере сидит и трансформатором монад погоняет, надо снова напрячь мозги и вспомнить. А во-вторых, у меня после починки скорее всего будут другие, хотя и альфа-эквивалентные, выходные программы на С++. Столько тестов переделывать!

Суть проблемы в том, что надо было уникальные имена типовых переменных генерить. Я раньше использовал наколенный глючный унификатор, и через атрибутную грамматику протаскивал счётчик.

А потом унификацию заменил на покупную из unification-fd, но счётчик оставил, и похоже построил целую инфраструктуру для перевода имен, выдаваемых моим счётчиком, в имена, выдаваемые unification-fd и обратно.

В-общем, если предположение выше верно - можно будет отрезать этот слой конверсии и сократить количество строк :)

Upd: гипотеза частично подтвердилась трассами:

Unifier.map = fromList [("a",0),("b",1),("num",2),("s",3),("t0",4),("t1",5),("t10",15),("t11",14),("t12",16),("t13",17),("t14",18),("t15",20),("t16",19),("t17",21),("t18",22),("t19",23),("t2",6),("t20",24),("t21",25),("t22",26),("t23",27),("t24",28),("t3",7),("t4",8),("t5",10),("t6",9),("t7",11),("t8",12),("t9",13)]

("t9",13) означает что атрибутная грамматика выдала 9, а унификатор - 13.

18 января 2017, 06:18

17 января 2017

nponeccop

Замыкания на Rust

#include <valarray>

std::valarray<int> foo(std::valarray<int> x, int y)
{
        auto mul2 = [=](std::valarray<int> x) { return x * y; };
        return mul2(x);
}
Rust:
fn foo(x: Vec<i32>, y: i32) -> Vec<i32>
{
    let mul2 = |x: Vec<i32>| x.iter().map(|x| x * y).collect();
    mul2(x)
}

fn main() {
     println!("{:?}", foo(vec![1, 2, 3], 6))
}

17 января 2017, 18:45

Scala@livejournal.com

Как реализовать fallback ?

Возвращаясь к ранее приведённому примеру: Допустим у нас есть функция для чтения файла
type Content = String
def readFile(fileName: String): Try[Content] = ???
Нам нужно написать функцию readFile(fileNames: List[String]), которая бы читала все файлы по очереди и возвращала содержимое первого успешно считанного файла. Тогда эта функция будет выглядеть так:
def readFile(fileNames: List[String]): Either[Content, List[Throwable]]
А что, если нам нужно вместе с содержимым получить список ошибок, которые случились до того ? Тогда функция будет:
def readFile(fileNames: List[String]): Either[(Content, List[Throwable]), List[Throwable]]
Как написать такую функцию ?

написал Michael 17 января 2017, 16:46

16 января 2017

nponeccop

Подпилил HNC

В-основном выпилил из парсера лигаси и налепил везде fmap. HN/Parser2.hs сократился в 2 раза до 90 строк со 180. Или до 60, если считать c помощью cloc без комментов и пустых строк.

Если считать консервативно (не считать тесты и SPL) - то на весь проект 1700 строк

cloc AG HNC.hs Utils.hs Setup.hs Bar.ag HN CPP FFI Tools Utils --force-lang=haskell,ag

Делим 60 на 1700 - получаем 3.5% занимает парсер. Это для тупых, считающих, что компилятор состоит из парсера, или предлагающих экономию на спичках в виде использования готового парсера S-выражений. Я люблю экономию на спичках, но красивый лексический синтаксис комментариев я люблю больше!

16 января 2017, 17:00

15 января 2017

Scala@livejournal.com

Как решить предыдущий пример без моноида ?

Допустим, нужно прочитать обязательно все файлы и вернуть либо содержимое всех этих файлов, либо список ошибок чтения.
def readFiles(fileNames: List[String]): Either[List[Throwable], List[String]] = ???
Предположим у нас есть уже функция для чтения одного файла:
def readFile(fileName: String): Try[String] = ???
Как написать функцию readFiles без использования моноидов как в предыдущем посте ?

Было предложено сначала построить val tries: List[Try[String]] = fileNames map readFile, а дальше из этого списка получить Either[List[Throwable], List[String]].
Будет ли это проще чем решение в предыдущем посте ?

написал Michael 15 января 2017, 15:27

14 января 2017

Scala@livejournal.com

Пример использования моноида. Накопление ошибок

Допустим, нам нужно прочитать несколько файлов. Функция readFiles принимает список имён файлов, которые нужно прочитать, и возвращает либо список содержимого файлов (пусть это будут строки для простоты), либо список ошибок, из-за которых нам не удалось эти файлы прочитать.
def readFiles(fileNames: List[String]): Either[NonEmptyList[Throwable], List[String]] = ???
Предположим у нас уже есть функция, которая читает один файл:
def readFile(fileName: String): Try[String] = ???
Наша задача написать функцию readFiles.
def readFiles(fileNames: List[String]): Either[NonEmptyList[Throwable], List[String]] = {
  val read = {fn: String => readFile(fn).toEither.map(_ :: Nil).toValidatedNel}
  val validated = fileNames foldMap read
  validated.toEither
}
Что тут можно улучшить или упростить ?
Я хочу использовать этот пример для демонстрации полезности моноида: List это моноид. Validated[A, B], где А и B моноиды -- тоже моноид. А для работы с моноидами у нас есть удобная функция foldMap.

Ещё примеры использования моноида:

   1) написать readFiles2 (partial results), чтобы та возвращала и список содержимого, и список ошибок чтения
   2) написать readFiles3 (fallback), чтобы та возвращала содержимое первого файла, который удалось прочитать, и список ошибок, случившихся до того.

Можно ли для (2) использовать моноид ?

написал Michael 14 января 2017, 21:21

Максим Сохацкий

Дефорестизационные Интерпретаторы O2

Тут nponeccop говорит, что наши JIT интерпретаторы говно, вручную мы аллоцируем регистры или через LLVM калейдоскоп, и что надо делать интерпретаторы с реврайт рулами которые делают фьюжин на стадии прекомпиляции. Такие интерпретаторы надо выделить в отдельный класс О2, например, а О класс пускай включает в себя все нормальные интерпретаторы, включая CPS и JIT.

Примеры элиминаторов или правила дефостеризации для стримов и листов:

stream (unstream s) = s
foldr k z (build g) = g k z

where

foldr f z [] = z
foldr f z (x:xs) = f x (foldr f z xs)
build g (:) []
stream :: List -> Stream
unstream :: Stream -> List

Приложения в промышленности: векторизация, SIMD конвеерация

__________________
[1]. https://github.com/flypy/flypy/blob/master/docs/source/fusion.rst#id19
[2]. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.36.5748&rep=rep1&type=pdf
[3]. http://citeseer.ist.psu.edu/viewdoc/download;jsessionid=CF2161C30B69C13CB86B4CAB32E6F607?doi=10.1.1.421.8551&rep=rep1&type=pdf

14 января 2017, 01:12

12 января 2017

nponeccop

Quote of the day

We suspect that many C programmers are in the same state of ignorance - SPJ

Имелось ввиду, что сишник, которому SPJ дал задание написать скалярное произведение длинных векторов на SIMD-интринсиках, не осилил префетчи и написал код на уровне автовекторизатора GCC, отстав от state of the art BLAS в 2 раза на некоторых участках.

12 января 2017, 22:32

Scala@livejournal.com

К предыдущему

По предложению lomeo заменил возвращаемое значение testFetch на Option
case class Foo(name: String)
def fetch(name: String):Foo = ???

import cats.implicits._

class FetchFooSpec extends SpecificationWithJUnit {

  def testFetch(name: String): Option[String] = 
    if (fetchFoo(name).name == name) none else s"$name error".some

  def testFetch2(names: List[String]): Option[String] = names foldMap testFetch map (_.mkString(", "))

  "fetchFoo should handle all names" {
     val names = List("abc", "a/b/c", "a.b.c", "אבג")
     testFetch2(names) must beNone
  }
}
Как правильно заметил juan_gandhi заменять names на генератор случайных данных в этом тесте не нужно. Но можно, наверное, применить такой генератор для других тестов.

написал Michael 12 января 2017, 11:39

nponeccop

Кметтификация словами Кметта

Из опубликованного вчера интервью с Кметтом:

For the most part I look for something that should exist for some deep underlying mathematical reason that doesn’t yet exist in code in a reusable form and try to figure out how to bring it about.

Но он на этом не останавливается - всё интервью так или иначе посвящено тому, как выглядит кметтификация изнутри головы.

12 января 2017, 03:18

Максим Сохацкий

Дейкстра об APL-бомжах :-)

APL is a mistake, carried through to perfection. It is the language of the future for the programming techniques of the past: it creates a new generation of coding bums.

http://www.cs.virginia.edu/~evans/cs655/readings/ewd498.html

12 января 2017, 01:18

11 января 2017

Dee Mon journal

эта самое

Haskell on JVM, made in Bangalore: http://eta-lang.org/

(not to be confused with http://www.elalang.net/ which is for .NET, dynamically typed and made in Moscow)

11 января 2017, 20:17