Russian Lambda Planet

20 августа 2017

Anton Salikhmetov

Депрессия

У меня тут экзист... в общем, кризис среднего возраста. Были поводы. Пока было солнце, море и пиво две недели, думал, что пройдет. Не прошло. Вокруг какая-то сплошная хуита творится. Нашел какие-то online social support groups. Открыл, посмотрел и закрыл. Только хуже стало. Одни уроды и дебилы. Те же самые, что и в жизни. А где взять глобус с неуродами и недебилами, неизвестно. Уроды и дебилы - депрессия - еще больше уроды и дебилы - еще больше депрессия... Это замкнутый круг какой-то!

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

Короче, надо просто всех убить, и все.

comment count unavailable comments

20 августа 2017, 06:50

16 августа 2017

nponeccop

Объясните грабли

bug.ts:
export const foo = (bar: number) => {
    console.log(arguments)
}
Компиляция без ключей, "tsc bug.ts", ожидаемо падает c сообщением о том, что arguments нету в случае arrow function.

А если собирать как "tsc -t es6 bug.ts" - то собирается без ошибок, а в рантайме понятно что жопа.

Так и должно быть? Да-нет и почему.

16 августа 2017, 19:28

David Sorokins WebLog

Трансляция модели из Python в Haskell

Вспомнив известные слова про гору и Магомета, решил сделать свои наработки более доступными. Создал для языка программирования Python пакет aivika-modeler, который позволяет создавать дискретно-событийные модели. а затем запускать основанные на них имитационные эксперименты по методу Монте-Карло с тысячами запусков в серии и более.

Пакет больше предназначен быть неким клеем, с помощью которого на языке Python можно соединять и объединять готовые компоненты в единую модель, причем сами компоненты предполагается создавать уже на языке Haskell. Однако, во многих случаях должно хватить существующего набора компонент, и поэтому часто можно ограничиться одним языком Python. В планах добавить поддержку GPSS-подобного DSL.

Есть довольно большая категория людей из целевой аудитории, которые не знают, не хотят и не любят программирование, но Python вполне могут знать на некотором простом уровне. Однако, они могут быть очень хорошими специалистами в своей предметной области. Мой пакет может показаться удобным для них.

Итак, модель описывается на языке Python. По ней автоматически создается соответствующий код на языке Haskell. Более того, создается готовый проект на основе системы сборки Stack. Собственно, это главное техническое требование - на системе пользователя должен быть установлен Stack. Здесь предвижу некоторые возможные трудности с пакетом old-time на некоторых системах Windows, но надеюсь, что со временем они благополучно разрешатся.

Так вот, автоматически созданный проект на Stack собирается, а потом запускается на исполнение. В случае успеха в самом конце открывается веб-браузер с результатами имитационного эксперимента. Там могут быть графики, гистограммы, ссылки на таблицы в формате CSV, сводная статистика и прочая информация. Вид и формат желаемых итоговых результатов задается также на языке Python.

Мне был довольно интересен такой эксперимент по использованию Haskell из Python. Может быть, кто-нибудь возьмет идею на вооружение

написал dsorokin (noreply@blogger.com) 16 августа 2017, 07:31

09 августа 2017

nponeccop

Внезапно работы по GHC+libuv

https://ghc.haskell.org/trac/ghc/ticket/8400

там правда не RTS, а товарищ свою NIH base пишет, с libuv и IOCP.

09 августа 2017, 22:36

04 августа 2017

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

Swift Model Generator from Erlang Types

-module(roster_swift).
-export([parse_transform/2]).
-compile(export_all).
-define(SRC, "apps/roster/priv/macbert/").

parse_transform(Forms, _Options) -> switch(directives(Forms)), Forms.
directives(Forms) -> lists:flatten([ form(F) || F <- Forms ]).

switch(List) ->
    file:write_file(?SRC++"Source/Decoder.swift",
    iolist_to_binary(lists:concat([
       "func parseObject(name: String, body:[Model], tuple: BertTuple) -> AnyObject?\n"
       "{\n    switch name {\n",
       [case_rec(X) || X <- List],
       "    default: return nil\n"
       "    }\n}"
    ]))).

act(List,union,Args,Field,I) -> act(List,union,Args,Field,I,simple);
act(List,Name,Args,Field,I) -> act(List,Name,Args,Field,I,keyword).

act(List,Name,Args,Field,I,Fun) ->
%    io:format("Keyword: ~p~n",[{Name,Args}]),
    lists:concat([tab(1),List,".",Field,
    " = body[",I,"].parse(bert: tuple.elements[",I+1,"]) as? ",
    ?MODULE:Fun(Name,Args,{Field,Args}),"\n"]).

case_rec({Atom,T}) ->
    List = atom_to_list(Atom),
    Lower = string:to_lower(List),
    Var = "a" ++ List,
    lists:concat([ "    case \"", List, "\":\n"
    "        if body.count != ", integer_to_list(length(T)), " { return nil }\n",
    io_lib:format("        let ~s = ~s()\n",[Var,List]),
    [ tab(2) ++ act(Var,Type,Args,Field,I-1) ||
         {{_,{_,_,{atom,_,Field},Value},{type,_,Type,Args}},I} <- lists:zip(T,lists:seq(1,length(T))) ],
    "        return " ++ Var ++ "\n" ]).

form({attribute,_,record,{List,T}})  ->
   [X|Rest]=atom_to_list(List),
   case X >= $A andalso X =< $Z andalso List /= 'Client'
                                orelse List == io
                                orelse List == error
                                orelse List == ok2
                                orelse List == error2
                                orelse List == ok of true
      -> spec(List,T),
         class(List,T),
         {List,T};
    _ -> [] end;
form(Form) ->  [].

class(List,T) ->
   file:write_file(?SRC++"/Model/"++atom_to_list(List)++".swift",
   iolist_to_binary(case lists:concat([ io_lib:format("\n    var ~s",
                [ infer(Name,Args,atom_to_list(Field))])
               || {_,{_,_,{atom,_,Field},Value},{type,_,Name,Args}} <- T ]) of
               [] -> [];
               Fields -> lists:concat(["\nclass ",List," {", Fields, "\n}"]) end)).

spec(List,T) ->
    file:write_file(?SRC++"/Spec/"++atom_to_list(List)++"_Spec.swift",
    iolist_to_binary("func get_"++atom_to_list(List) ++ "() -> Model {\n  return " ++ premodel(List,T) ++ "}\n")).

premodel(List,T) ->
    D = 1,
    Model = tab(D) ++ string:join([ model({type,X,Type,Args},D+1) || {_,_,{type,X,Type,Args}} <- T ],",\n"++tab(D)),
    erlang:put(List,Model),
    io_lib:format("Model(value:Tuple(name:\"~s\",body:[\n~s]))",[atom_to_list(List), Model]).

tab(N) -> lists:duplicate(4*N,$ ).

model({type,_,nil,Args},D)     -> "Model(value:List(constant:\"\"))";
model({type,_,binary,Args},D)  -> "Model(value:Binary())";
model({type,_,atom,Args},D)    -> "Model(value:Atom())";
model({type,_,list,[{type,_,atom,[]}]},D)    -> "Model(value:List(constant:nil, model:Model(value:Atom())))";
model({type,_,list,[{type,_,binary,[]}]},D)  -> "Model(value:List(constant:nil, model:Model(value:Binary())))";
model({type,_,list,[{type,_,integer,[]}]},D) -> "Model(value:List(constant:nil, model:Model(value:Number())))";
model({_,_,list,[{_,_,record,[{_,_,Name}]}]},D) -> lists:concat(["Model(value:List(constant:nil,model:get_",Name,"()))"]);
model({type,_,list,[Union]},D)    -> "Model(value:List(constant:nil, model:"++ model(Union,D) ++ "))";
model({type,_,record,[{atom,_,Name}]},D)        -> lists:concat(["get_",Name,"()"]);
model({type,_,list,Args},D)    -> "Model(value:List(constant:nil))";
model({type,_,boolean,Args},D) -> "Model(value:Boolean())";
model({atom,_,Name},D)         -> lists:concat(["Model(value:Atom(constant:\"",Name,"\"))"]);
model({type,_,term,Args},D)    -> "Model(value:nil)";
model({type,_,integer,Args},D) -> "Model(value:Number())";
model({type,_,tuple,any},D)    -> "Model(value:Tuple())";

model({type,_,union,Args},D)   -> io_lib:format("Model(value:Chain(types:[\n~s]))",
                                  [tab(D) ++ string:join([ model(I,D+1) || I <- Args ],",\n"++tab(D))]);

model({type,_,tuple,Args},D)   -> io_lib:format("Model(value:Tuple(name:\"\",body:[\n~s]))",
                                  [tab(D) ++ string:join([ model(I,D+1) || I <- Args ],",\n"++tab(D))]);

model({type,_,Name,Args},D)    -> io_lib:format("Model(~p): Args: ~p~n",[Name,Args]).

keyword(X,Y,_Context) -> keyword(X,Y).
keyword(record, [{atom,_,Name}]) -> lists:concat([Name]);
keyword(list, [{type,_,record,[{atom,_,Name}]}]) -> lists:concat(["[",Name,"]"]);
keyword(list, [{type,_,atom,[]}]) -> lists:concat(["[","String","]"]);
keyword(list, Args)   -> "[AnyObject]";
keyword(tuple,any)    -> "[AnyObject]";
keyword(term,Args)    -> "AnyObject";
keyword(integer,Args) -> "Int";
keyword(boolean,Args) -> "Bool";
keyword(atom,Args)    -> "StringAtom";
keyword(binary,Args)  -> "String";
keyword(union,Args)   -> "AnyObject";
keyword(nil,Args)     -> "AnyObject".

infer(union,Args,Field) -> Field ++ ": " ++ simple(union,Args,{Field,Args}) ++ "?";
infer(Name,Args,Field)  -> Field ++ ": " ++ keyword(Name,Args,{Field,Args}) ++ "?".

simple(A,[{type,_,nil,_},{type,_,Name,Args}],Context) -> keyword(Name,Args,Context);
simple(A,[{type,_,Name,Args},{type,_,nil,_}],Context) -> keyword(Name,Args,Context);
simple(_,_,_) -> "AnyObject".

04 августа 2017, 19:23

28 июля 2017

nponeccop

Implementing Algebraic Effects in C “Monads for Free in C”

Тут проскочила ссылка на пейпер. Не радуйтесь, там это лапша из setjmp/long jump, а не rust-style zero cost.

28 июля 2017, 16:22

10 июля 2017

nponeccop

Опять починили Hyper-V

Теперь правда не креши, а поддержку high dpi displays. Теперь гостевые low dpi displays на low dpi хостах снова отображаются корректно (но только после того как загрузится модуль hyperv_fb)

С крешами ситуация старая по веткам:

4.11.9 работает
4.9.36 падает
4.4.76 вешается
4.1.42 падает
3.18.60 работает
3.16.43 работает
3.14.2 работает

10 июля 2017, 23:18

25 июня 2017

Nikita Prokopov

Зачем вам нужна Clojure?

Слайды доклада на Codefest: https://speakerdeck.com/tonsky/clojure-at-codefest-2013 (там же и pdf)

Картинки для привлечения внимания:





Спасибо lionet и моей жене Юле за помощь в подготовке доклада.

25 июня 2017, 22:48

21 июня 2017

beroal

сумма как моноидальное произведение

Правильно ли я думаю, что любой функтор F является моноидальным между категориями, в которых моноидальная структура задана категорной суммой? Конкретно, (F, [F(ι0), F(ι1)]) есть моноидальный функтор? (ι… — инъекции суммы.)

21 июня 2017, 12:33

map, filter, catMaybes

∃a. ∃b. ∃m:a->Maybe b. ∀f:a->b. ∀p:a->Bool. ¬(catMaybes . map m == map f . filter p)

Другими словами, не всякий catMaybes можно выразить через map и filter. Ситуация такая же, как с инъекциями и сюръекциями. Для каждой инъекции s:A->B, кроме случая, когда A пустое и B населённое, существует сюръекция r такая, что r∘s=id. Это «кроме» портит всё удовольствие.

Значит, придётся отказаться от filter в пользу функции zyu

zyu m = catMaybes . map m
zyu (m1 <=< m0) == zyu m1 . zyu m0

где <=< — композиция в категории Клейсли над Maybe.

21 июня 2017, 12:33

the list type constructor and its analogs

Besides singly linked (inductive) lists, there are other entities similar to lists. They may be more or less convinient than lists depending on a problem.

Inductive lists first. The most concise interface for lists is the isomorphism list e ≅ list_step e (list e), where list_step e rc := 1 + e×rc. The right-to-left component of this isomorphism is list construction, left-to-right is destruction. The glaring property of such lists is asymmetry. A head of a list is accessible by 1 destruction, other elements require more. An inductive list is a stack, construction is “push”, destruction is “pop”, a head of a list is a top of a stack.

But we can provide 2 isomorphisms for every side of a list, where side is “left” or “right”. The S-side isomorphism tinkers with the S-most element of the list.

I will describe 2 kinds of symmetric lists: free monoids and arrays.

Viewing a list as a free monoid stresses the fact that a list may be folded/accumulated by a monoid. In detail, there are the category of sets, the category of monoids, and the adjunction F⊣U between them. F e is a monoid, the free monoid of e. It is the standard list monoid, i.e. its operations are concatenation and the empty list. Its carrier is the set of lists with elements from the set e. ε (the counit) of the adjunction is a folding function. ε m, where m is a monoid, folds a given list with m. List elements must come from the carrier of m, of course. η e (the unit of the adjunction) converts a value into a singleton list containing this value. (A singleton list is a list of length 1.)

Folding provides a limited way of reading. Some definitions first. I will use “assop” is another name for associative (2-ary) operation. For every side S, S-assop is the operation which returns its argument at S. Using a free functor from the category of assops to the category of monoids, we obtain the S-monoid, its created neutral element will be denoted as NONE and an assop element a as SOME a. For every list bs, folding map SOME bs by S-monoid gives SOME a, where a is the S-most element of the list, if it exists, and NONE otherwise. But we cannot read, for example, the element after the head in this way. This can be proved. Suppose that there is a function f and a monoid m, m = ⟨+', 0'⟩, such that fold m (map f bs) returns the element of bs after the head. Let g bs := fold m (map f bs). Then ∀a, ∀b, g [a, b] = SOME b and g [a, b] = f a +' g [b] = f a +' NONE. This means that SOME 0 = SOME 1, but SOME is injective like every data constructor.

Suppose that a function is constructing an abstract list, i.e. using an interface of lists. A monoid is not enough: we need to build finite lists somehow. So the interface must at least contain a method which construct a singleton list. Then we can get a finite list by concatenating singleton lists. This interface has 2 type parameters: a monoid carrier m (presumably the standard list monoid) and a type of list elements e. Using category theory, an implementation of this interface can be described concisely as an object in the category (comma category) of morphisms from the object e to the functor U. I call such an interface “a monoid with import”, where the function “import” is singleton list construction, so an element is may be imported into a monoid. Observe that this interface does not depend on a type constructor.

Instead of relying on types m and e, we can provide a type constructor list, a monoid structure on list e for every e, and a monad structure on list. Then import becames η of the monad list.

Random-access lists aka arrays. A simple formal description of an array is a function from list indices (locations) to list elements. Indices may be natural numbers starting from 0, but we do not need such details. A set of indices may be any finite total order. Concatenation of arrays requires a notion of a sum of total orders. Let L0 and L1 be total orders. Then the set carrier(L0)+carrier(L1) (“+” on sets is disjoint union) with lexicografic order is the total order L0+L1. Let a0:carrier(L0)→e and a1:carrier(L1)→e be arrays. carrier(L0+L1) = carrier(L0)+carrier(L1), carrier(L0+L1)→e = carrier(L0)+carrier(L1)→e ≅ (carrier(L0)→e) × (carrier(L1)→e) by properties of categorical sum. The right-to-left component of this isomorphism is concatenation, the left-to-right component is splitting.

21 июня 2017, 12:32

путь к теории категорий



есть очевидный путь к теории категорий: формальная логика, алгебраические структуры, порядки, теория категорий
вы ищете «царский» путь, читаете философию, научпопные сказки, лишь бы не изучать математику
зачем вы так?

настенькины комиксы, не надо так, рисовач.ру

21 июня 2017, 12:32

придумайте какую-нибудь теорию

Задача из учебника по физике: «Запишите уравнение Менделеева—Клапейрона. Придумайте задачу на его применение и решите её». По мотивам я придумал свою: «Изучите теорию категорий. Научите теории категорий других. Придумайте ещё какую-нибудь теорию».

21 июня 2017, 12:31

24 мая 2017

Nikita Prokopov

Читабельная Кложа

Обнаглел настолько, что код вставляю скриншотами

http://tonsky.me/blog/readable-clojure/

24 мая 2017, 14:09

05 мая 2017

Yan Tayga

Курс по Хаскелю на русском, часть 2

Почти закончил курс -- еще есть что решать и можно решать, конечно, но на праздники возможности уже не будет.

По итогам - по глупости завалено 1 peer review, не решена 1 задачка на строгость, не решены 2 задачи на continuation и еще одна задачка на разобраться с типами применяя расширения ghc. Все остальное вроде нормально более менее и понятно.

Курс сам по себе просто отличный. Был бы еще лучше, если бы:
- подробнее бы рассмотрели continuation -- темы вроде на целую неделю вполне хватит, с нормальными постепенно возрастающей сложности задачами. Все таки интересная штука.
- изредка тщательнее формулировались задачи. Впрочем, по отзывам они часто тут же исправлялись командой курса.
- больше задачек не якобы «творческих» и с подвохом, а более рутинных, закрепить понятый материал. Ucucuga в обучении, имхо, не самый лучший выбор.

Но, повторюсь -- курс самый лучший из виденных мною по ФП вообще.

05 мая 2017, 09:29

28 апреля 2017

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

Le Coq` Art

Печатнул обе версии, Французскую и Английскую!



Издательство sagarasousuke

28 апреля 2017, 16:37

24 апреля 2017

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

Quelea — a declarative programming model for eventually consistent data stores

The store is a collection of replicas, each storing a set of objects (x, y, . . .) of a replicated data type. For the sake of an example, let x and y represent objects of an increment-only counter replicated data type (RDT) that admits inc and read operations.

We say that the effects inc1x and inc2x are visible to the effect (inc4x) of x.inc, written logically as vis(inc1x, inc4x) ∧ vis(inc2x, inc4x).

To capture happens-before, we define an irreflexive transitive session order relation that relates the effects of operations arising from the same session. For example, in Fig. 1, inc4x and inc5x are in session order (written logically as so(inc4x, inc5x)).

same object session order (soo = so ∩ sameobj)
same object happens-before order (hbo = (soo ∪ vis)+)
happens-before order (hb = (so ∪ vis)+)

Causal Visibility (CV) ::= ∀a, b, c. hbo(a, b) ∧ vis(b, c) ⇒ vis(a, c) 
Causal Consistency (CC) ::= ∀a, b, c. hbo(a, b) ⇒ vis(a, b)
Strong Consistency (SC) ::= ∀a, b. sameobj(a, b) ⇒ vis(a, b) ∨ vis(b, c)

Read Your Writes (RYW) ::= ∀a,b. soo(a, b) ⇒ vis(a, b)
Monotonic Reads (MR) ::= ∀a,b,c. vis(a, b) ∧ soo(b, c) ⇒ vis(a, c)
Monotonic Writes (MW) ::= ∀a,b,c. soo(a, b) ∧ vis(b, c) ⇒ vis(a, c)
Writes Follow Reads (WFR) ::= ∀a,b,c,d. vis(a,b)∧vis(c,d)∧(soo ∪ =)(b,c) ⇒ vis(a,d)

∀a,b,c.txn{a,b}{c} ∧ sameobj(a,b) ∧ vis(a,c)⇒vis(b,c)
∀a,b,c.txn{a}{b,c} ∧ sameobj(b,c) ∧ vis(b,a)⇒vis(c,a)

∀(a, b : getBalance),
 (c : withdraw ∨ deposit),
 (d : withdraw ∨ deposit). txn{a,b}{c,d} ∧ vis(c,a) ∧ sameobj(d,b)⇒vis(d,b)
∀a,b,c,d.txn{a,b}{c,d} ∧ so(a,b) ∧ vis(c,a) ∧ sameobj(d,b)⇒vis(d,b)
∀a,b,c,d.txn{a,b}{c,d} ∧ vis(c,a) ∧ sameobj(d,b)⇒vis(d,b)


ШИВА-РАМА-КРИШНА-Н!
______________
[1]. http://kcsrk.info/papers/quelea_ieee16.pdf
KC Sivaramakrishnan, Gowtham Kaki, Suresh Jagannathan
IEEE Data Engineering Bulletin, 39(1): 52 64, March 2016

24 апреля 2017, 17:06

22 апреля 2017

nponeccop

Avoiding success is..

Вместо эпиграфа:
---
Every 2nd grader knows that the C++ template system is Turing complete. So what? Compile time Brainfuck evaluator that’s what!
---

Надо выпустить какой-нибудь сойлент с вкладышами "Avoiding success is.."

22 апреля 2017, 17:30

21 апреля 2017

Dee Mon journal

Streams

Вот Идрис синтаксически очень похож на хаскель, однако не ленивый. В хаскеле ленивость-по-умолчанию сопровождается строгостью-по-запросу, добавшяешь перед полем значок ! и оно строгое. Оказывается, в Идрисе нынче есть симметричная штука: добавляешь перед типом поля волшебное слово Inf, и поле оказывается "ленивым": когда данные конструируются, выражение для вычисления этого поля не вычисляется сразу, а автоматически оборачивается в Delay (если явно поленился это сделать), а при паттерн-матчинге оно когда надо автоматически форсится через Force (т.е. механика практически как в окамле с ленивыми значениями, но вручную необязательно оборачивать и форсить, компилятор сам вставляет).
Например, через этот механизм сделан тип бесконечных последовательностей:
data Stream : Type -> Type where
(::) : (value : elem) -> Inf (Stream elem) -> Stream elem

Благодаря автоматическому расставлению делеев и форсов, код с такими коданными выглядит так же просто и чисто, как в хаскеле:
countFrom : Integer -> Stream Integer
countFrom x = x :: countFrom (x+1)

first : Nat -> Stream a -> List a
first Z xs = []
first (S k) (x :: xs) = x :: first k xs

prepend : List a -> Stream a -> Stream a
prepend [] ys = ys
prepend (x :: xs) ys = x :: prepend xs ys

Обратите внимание, что в функциях выше :: используется в паттерн-матчинге и в конструировании сразу и для списков и для стримов, компилятор сам по типу понимает где что, и для стримов вставляет delay/force.
Подобно Основной Теореме Арифметики и Основной Теореме Алгебры, есть Основная Теорема Функционального Программирования (это, по Карри-Говарду, конечно же тоже функция), ее можно записать так:
fibs : Stream Integer
fibs = 1 :: 1 :: zipWith (+) fibs (drop 1 fibs)

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

— Не пугайтесь, Екатерина Петровна, и не волнуйтесь. Только нет в мире никакого равновесия. И ошибка-то всего на какие-нибудь полтора килограмма на всю вселенную, а все же удивительно, Екатерина Петровна, совершенно удивительно!

21 апреля 2017, 18:17

верифай, но проверяй

This paper thoroughly analyzes three state-of-the-art, formally verified implementations of distributed systems: IronFleet (Dafny/C#), Verdi (Coq/OCaml), and Chapar (Coq/OCaml). Through code review and testing, we found a total of 16 bugs, many of which produce serious consequences, including crashing servers, returning incorrect results to clients, and invalidating verification guarantees.
https://homes.cs.washington.edu/~pfonseca/papers/eurosys2017-dsbugs.pdf
В протоколах и их доказанных реализациях багов не нашли, все баги были на границе взаимодействия верифицированного кода с жестоким внешним миром - неверифицированным окружением. Сложно описать формально все возможные косяки низкоуровневых библиотек и сторонних процессов. Смешной момент - Dafny для верификации использует Z3 солвер, если солвер невовремя прервать, Дафни считает, что все ок и считает недопроверенную программу годной.

А тут мужики нагенерили много тестовых программок для компиляторов:
In less than six months, our approach has led to 217 confirmed GCC/Clang bug reports, 119 of which have already been fixed ... In about three weeks, we have also found 29 CompCert crashing bugs, and 42 bugs in the production Scala compiler and the Dotty research compiler.
https://arxiv.org/pdf/1610.03148.pdf
GCC и Clang могут падать, а могут неправильный код генерить. CompCert (который на Coq'e верифицирован), как я понял, неправильный код не генерит, но вот сам падать может - ассерты срабатывают внутри, т.е. некоторая неконсистентность логическая там была.

21 апреля 2017, 06:50

17 апреля 2017

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

Пронумеруем типы и их значения

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

encode (X: Type) -> Nat
decode (X: Nat) -> (Sig: Type, Values: Stream Sig)


Еще это можно назвать — глобальное управление контекстами. Функция decode — может состоять из генератора Values: Nat -> Sig, который аллоцирует в виртуальной машине уникальный инстанс типа Sig по заданному Nat. Таким образом каждая возможная переменная в пространстве типов и термов на всех уровнях может индексироваться тройков Nat значений (Nat,Nat,Nat) — индекс вселенной, индекс типа, и индекс инстанса.

Конструирование термов в зависимом тайпчекере:

0 — UNIT      =
1 — NORM      = Nat      // normalisation
2 — SUBST     = Nat      // substitution 
3 — STAR      = Nat      // universe        
4 — REC       = Nat      // Cons: A -> List A -> List A
5 — VAR       = Nat Nat  // Nat, Bool, List A, Vec Nat A
6 — OR        = Nat Nat  // data
7 — AND       = Nat Nat  // record
8 — EQ        = Nat Nat  // definition 
9 — PI        = Nat Nat Nat
A — FUN       = Nat Nat Nat
B — TYPECHECK = Nat        


Пример:

encode "List A = Nil: List A | Cons: A -> List A -> List A"

0 — UNIT        // "A"
1 — UNIT        // "Nil"
2 — UNIT        // "Cons"
3 — UNIT        // "List"
4 — VAR 0 _     // A
5 — VAR 3 4     // List A
6 — REC 5       // Rec List A
7 — AND 4 6     // (A, Rec List A)
8 — VAR 2 7     // Cons: A -> List A
9 — VAR 1 _     // Nil:
A — OR 9 8      // Nil: | Cons:
B — EQ 5 A      // List A = Nil: List A | Cons: A -> List A -> List A


— основные конструкторы, которые индексируют (кроме Unit), некоторую переменную в таблице имен (индексы де Брейна), значение которой составляет тройка, таким образом словарь контекстов — List (Nat, (Nat, Nat, Nat)) — закодирован списком пар.

Для сравнения, List A в формате Lean:

1 — NS 0 u
2 — NS 0 list
3 — NS 0 α
1 — UP 1
0 — ES 1
1 — EP BD 3 0 0
4 — NS 2 nil
2 — EC 2 1
3 — EV 0
4 — EA 2 3
5 — EP BD 3 0 4
5 — NS 2 cons
6 — NS 0 a
6 — EV 1
7 — EA 2 6
8 — EV 2
9 — EA 2 8
A — EP BD 6 7 9
B — EP BD 6 3 10
C — EP BI 3 0 11
D — IND 1 2 1 2 4 5 5 12 1

17 апреля 2017, 16:36

13 апреля 2017

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

Семинары в НАН

Мне кажется мой доклад на прошлом семинаре про категорную семантику индуктивных типов прошел хорошо. Видео записали, скоро выложу.

Приходите на следующий семинар:

20.04.2017, Четвер
Семінар: Похiднi категорiї та їх застосування
Керівники: В.В. Любашенко
Місце: Інститут математики НАН України, вул. Терещенківська, 3, 219/305
Час: 15:30
Доповідач Ю.М. Беспалов
Доповідь: Кубічні групоїди
Резюме: За мотивами книги Ronald Brown, Philip J. Higgins, Rafael Sivera, Nonabelian Algebraic Topology: Filtered Spaces, Crossed Complexes, Cubical Homotopy Groupoids

Трейс семинаров:

Модератор: В.В. Любашенко. Провідний співробітник відділу топологій інституту математики НАН України

1. 30.03.2017 С.І.Максименко: Враження від гомотопічної теорії типів. Голова відділу топології інституту математики НАН України
2. 06.04.2017 М.Е.Сохацький: Категорна семантика індуктивних типів. Групоїд Інфініті
3. 20.03.2017 Ю.М. Беспалов: Кубічні групоїди. Існтитут теоретичної фізики НАН України

13 апреля 2017, 00:28

12 апреля 2017

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

Рекомендации от Mad Advisors Corp



Куда ИНВЕСТИРОВАТЬ, что НАСЛЕДОВАТЬ или ВОРОВАТЬ, на что ориентироваться:

Binary Protocols and Protocol Stacks (CORBA and SOAP Replacement)

— WebSocket
— SVG
— MQTT
— N2O
— ASN.1

Storage Systems (CODASYL and MUMPS Replacement)

— Aerospike (SSD)
— BlazingDB (GPU)
— PumpkinDB (FORTH, AVX) — лучший хакатон стартап на расте, авансом

Array Processing Languages (Fortran replacement)

— Futhark (GPU)
— Julia (AVX)
— AutumnAI (ML)

Concurrency Runtime and Languages (Ada Replacement):

— Pony (Runtime+Language, Erlang replacement, Zero Copy, CAS)
— Erlang, LING (Runtime+Language, Poor man)
— Rust (Language, Zero Copy)

R&D Languages (AUTOMATH replacement):

— Coq
— Z3
— Lean
— F*

Target Languages / Platforms for Runtime (Pascal Replacement):

— OCaml
— LLVM/MIR
— Rust
— D
— GHC

New Markets (Inexistant satisfaction) — озеро, где живут Синие Птицы и Черные Лебеди:

— VHDL FPGA toolchain replacement
— SIP/VoIP/RTP replacement
— Xen, Hyper-V, EXSI replacement
— Wolfram Mathematica replacement
— Lisp Machine replacement
— seL4 replacement

Куда НЕ ИНВЕСТИРОВАТЬ, от чего УБЕГАТЬ или что СОЗЕРЦАТЬ:

— JSON, XML, MessagePack, Text Protocols, ...
— HTML, Virtual DOM, React, Angular, Literally Any JavaScript Framework ...
— HTTP 1, 2, 3, 4, ...
C-Style Languages: Go, C, C++, JavaScript, TypeScript, ES6, ASM.JS, ...
Any LISP: Clojure, Common Lisp, Smalltalk, Self, Io, ...
Big VMs: JVM, CLR, ...
Просто унылое говно: Go, C#, Java, PHP, Scala, Python, PHP, Ruby, Elixir, Perl, node.js ...
Any RDBMS: SQL, MySQL, PostgreSQL, Oracle, ...
British Languages: Haskell, Agda, Idris, ...
APL Languages: K, J, Q, APL, ...
Almost any DHT: Riak, Cassandra, Spark, Hadoop, RethinkDB, CouchDB, Memcache, BDB, Tokio, MongoDB, Redis, ArangoDB, Neo4j, AllegroGraph, OrientDB, OrientDB
Almost any serializers: gRPC, Protobuf, Thrift, ...
Modern way of devops: Kubernetes, Docker, ...
Any product built by Google: Go, TensorFlow, Android, Blockly, Dart, Polymer,
Big Operaing Systems: UNIX, BSD, Linux, Windows, Mac

Список Обновляется. Коментарии Пендинг. Дискас.

Ты выше ЖЖ и не хочешь оставлять контент? Будь Анонимным!
Есть альтернативный канал комментирования https://erlach.co/pr/77c

Follow Back:

http://nponeccop.livejournal.com/556778.html

12 апреля 2017, 07:58

nponeccop

От чего бежать (языки)

Тут наш фашист-консультант сделал наброс типа по тру и не тру технологиям, прошлому и будущему.

Я придумал альтернативную мудаческую схему реальности. Есть академия - пишут "в стол". Есть хипсторы - пишут свистопердящую никому не нужные но красивые игрульки. И промышленные зрелые практики - пишут мейнстрим.

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

- Академия Хипсторы Мейнстрим Ретрограды
Прошлое ML, Coq, ACL2 CL, Ruby, R Сobol, Perl, Ada, C, C++ Scheme, VB6/.Net, PHP, Java, ObjC, D
Настоящее GHC Node, Scala, Erlang C++, Python, JS, Java, PHP С99, Go, Rust, Swift, Dart
Будущее F*, Z3, Lean Purs, Jupyter, Polly C++/OpenCL/OpenAcc, C#, Python, JS, TS


Тут надо комментировать каждую клетку

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

Хипсторы прошлого - CL это совсем далёкое прошлое, Ruby полупрошлое а R вот недавно. Имхо всё же R уступит своё место Питону. А там, где у питона кишка тонка - R уступит место всяким Julia under Jupyter. Джулии нет нигде в табличке, поскольку я вижу её, как чуть более прогрессивную и менее убогую сестру R, Питона и Матлаба.

Мейнстрим прошлого - тут только заведомый мейнстрим не столь далёкого прошлого. Языки упорядочены по моему пониманию степени ужаса программиста, столкнувшегося с соответствующим лигаси.

Ретрограды прошлого - ретрограды, с которыми всё ясно. PHP и Java успешно выполнили ретроградскую миссию и попали в мейнстрим, VB6 умер но VB.Net поддерживается в коме, ObjC если б не монополия/диктаторство Эппл тоже бы умер.

Академия настоящего - тут академия у которой есть шанс попасть на место Инрии в будущем. Я к сожалению мало знаком с академией, которая с одной стороны достаточно прогрессивна, а с другой стороны - работоспособна. Но GHC этому условию удовлетворяет. В отличие от всяких говноидрисов и прочих попыток избежать написания ленивого редуктора. Думаю GHC к 12 версии превратится в унылое но уже совершенно рабочее и зрелое говно.

Хипсторы настоящего - со Скалой проще всего. Если унылые энтерпрайзники жабошарпопитоновые собрались и решили писать стартап во имя блага всех существ - будут писать на Скале пить дать. Эрланг это для лиспорубепохапепитонистов решивших выпендриться. Нода достаточно забавна поскольку по сути лингва франка и не пишет на ней только ленивый лжавист или сишарпник. Для тех же плюсовиков скажем libuv подарок судьбы. Как в конце 1990-х на С++ разве что сайты не писали. Имхо всё из этой клетки просто со временем перекочует в "хипсторы прошлого". СL вот тоже достаточно хорош и хипстотен, но у него нет яркого будущего. Как и у ноды.

Мейнстрим настоящего - тут всё понятно, только нет Рубей, Р и С#. C# в мейнстриме по всем параметрам, но юные веб-падаваны не в курсе того что винда нужна и считают C# маргинальным, хоть он в первых строчках как не считай. Но МС продавливает его на линукс как Сан продавливала джаву куда только можно, и я считаю продавит.

Ретрограды настоящего - все на слуху (кроме может Dart и Swift). C99 отдельная категория. Это мейнстрим, но с ретроградским уклоном, и его адептов можно разделить на 3 категории: рокет саентисты, показывающие зиллионы попугаев там где конкуренты гордятся что у них овер 8000 или на самодельной гармонике играющие лучше чем иные на покупной, жертвы (например эмбедщики у которых просто вендор не написал кроме С ничего другого) и ебанаты (там как GNU-сексуалисты, так и школота жизни не видевшая, олд скул юникс вейщики, и просто упоротые - в общем в сортах специалистом не являюсь). Раст, свифт - можно сказать продолжатели своих соседей этажом выше (D и ObjC). Dart, Go - унылые высеры а ля PHP/нода но got traction.

Будущее лучше в обратном порядке описывать. Я вот не знаю что будет логическим продолжением ретроградской колонки. Ждём пока текущие начнут обсираться и будут предложены новые на их место. Я болею за C99 (может станет гошечкой), Go (может станет си для дебилохипсторов) и Rust (может присоединится к С++ в упоротых конторах, неупоротые говорят что в принципе юзабельно уже сейчас или через год будет).

Джава останется мейнстримом, но превратится в глазах общественности в унылый мейнстрим типа похапе сейчас. Т.е. станет "мейнстримом прошлого". Её место займет C#, в который будут вливать не рандомно-базарные фичи JSR а всякие няшки из ресёрча типа монад компрехеншонов Linq. Ну и под линухом МС запилит с JVM оракловской вряд ли победу - но уверенную ничью. А то и JetBrains купит - на такие кинжалы в спину МС горазда.

Python таки заборет R и Ruby, особенно в свете истерии machine learning. JS станет подобием чистых сей для ебанатов, а TS подобием C++ для промышленных зрелых видавших жизнь практиков с детьми которые будут юзать дремучее и уебищное админподмножество (заметьте и тут длинная рука MS).

Академия - вы не поверите, снова проклятые авторы ОС которой никто 10 лет в глаза не видел по мнению школоты и юниксофагоы, если не задали общее направление - то имеют достаточно типичных представителей направлений в своем портфолио.

Lean - в целом направление MLTT-пруверов с уклоном в HoTT

Z3 - направление ультрафинитных слабых логик и арифметик, типа битовых векторов SMT-LIB, я вижу очень перспективным. Долой мракобесие натуральных чисел и Тьюринг-полноты!

F* - направление gradual semi-automatic verification, гибрид модел-чекера, refinement typing, наколенного стат. анализатора и предыдущих двух направлений в рассчёте на экспорт в Бангалор.

12 апреля 2017, 06:53

09 апреля 2017

08 апреля 2017

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

Ватные Зав Типы

Зашел на канал, который гордо именуется зависимые типы: https://t.me/joinchat/AAAAAD9SWO-kmHf9o6Cn-Q, где сидят люди, которые нихуя не знают ни про пи калкулус, ни про лямбда исчисление, по великодушному приглашению моего антагониста 4da. Ни одной статьи полезной, репосты Вадлера (как он то к зависимым типам относится?) и Хаскелей. Ни одной новой темы, ничего. Болото, как и в ебантом ИТ, как и везде. Групоид Инфинити очевидно планку поднял высоко, не думаю что кто-то в Русском Мире до нее допрыгнет. Рома Михайлов вроде высоко парит, но практического применеия его FR языку, кроме как кодировать слова Хуй и Пизда я не вижу.

В конце чата мне предолжили стать оппонентом на защите (чувак с SLC на канале с зависимыми типами), я сказал, что после капитуляции России я сразу же приеду. На что мне сказали, что политека запрещена и я съебался (после того как меня забанили, еще смеялся ехидно, одминчег)! Хорошо, что видосы Вадлера и Хаскель System D разрешены.

В совете админов nivanych, который пизданулся и говорил мне что с Бандерой не так все очевидно как кажеться, сидя у себя в российских ебенях, а второй админ clayrat и глазом не моргнул, хотя живет не в России. Все-таки телеграм ужасно неудобный для чата. Хорошо, что все наши чаты в гиттере.

Кто говорит, что я нихуя не делаю и Групоид Инфинити хуйня, зайдите на канал и охуейте от контента, там 60 человек, саммый большой чат в России по зависимым типам. Нищета. Зайдите почитайте, кто любит срачи. Последнее слово будет Гаага и сказано будет в Гааге!

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

https://www.youtube.com/watch?v=RQjhqD0fHeo

https://www.youtube.com/watch?v=hqfzOxnx7yI

Ставлю тег Компьютер Сайнс, чо.

Все групповые чаты, которые создают русские обречены на забвение, так было с erlang-russian, так было с ЖЖ, так было с Juick, так стало с FPROG, так будет и с Зав Типами! Ноль контента — одна вата.

08 апреля 2017, 16:54

07 апреля 2017

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

Феномен постоянного повышения ставок

http://www.cs.virginia.edu/~robins/YouAndYourResearch.html

When you are famous it is hard to work on small problems. This is what did Shannon in. After information theory, what do you do for an encore? The great scientists often make this error. They fail to continue to plant the little acorns from which the mighty oak trees grow. They try to get the big thing right off. And that isn't the way things go. So that is another reason why you find that when you get early recognition it seems to sterilize you. In fact I will give you my favorite quotation of many years. The Institute for Advanced Study in Princeton, in my opinion, has ruined more good scientists than any institution has created, judged by what they did before they came and judged by what they did after. Not that they weren't good afterwards, but they were superb before they got there and were only good afterwards.

07 апреля 2017, 13:45

06 апреля 2017

ruhaskell.org

react-flux: React-powered Web GUI на Haskell

Доклад призван продемонстрировать возможность построения Web GUI с использованием GHCJS и библиотеки react-flux - "обертки" над ReactJS, отличающейся использованием подхода "Flux" для работы с состоянием приложения.

написал Денис Шевченко 06 апреля 2017, 00:00

Haskell вместо СУБД

Опыт отказа от реляционной СУБД в веб-проекте в пользу in-memory структуры данных и CAS (Content-addressable storage). Зачем это было сделано и что получилось в итоге.

написал Денис Шевченко 06 апреля 2017, 00:00

Если нельзя писать на Haskell, но очень хочется

Мы рассмотрим задачу построение OSC-контроллеров с графическим интерфейсом (в духе TouchOSC) и как писать таким образом UI на Haskell. На примере этой задачи мы рассмотрим альтернативный способ написание программ на Haskell. Мы можем написать небольшой интерпретатор на языке, который лучше справляется с данной задачей и можем генерировать код для интерпретатора из Haskell.

написал Денис Шевченко 06 апреля 2017, 00:00

Интеграция с API внешних сервисов

Опыт использования Haskell для для генерации HTTP клиентов для внешнего API. О проблемах, с которыми приходится сталкиваться во время разработки, возможных способах их минимизировать, а также о том, как Haskell помогает нам генерировать адекватную и всегда актуальную документацию для нашего API.

написал Денис Шевченко 06 апреля 2017, 00:00

Видео докладов 4 митапа

Видео со второй встречи нашего сообщества 6 апреля 2017 года.

написал Денис Шевченко 06 апреля 2017, 00:00

04 апреля 2017

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

Cutting Edge: New Basis for HITs

Andrej Bauer, Niels van der Weide

Theorem: if we have the coequalizers, path coequalizers, and colimits, then we have all HITs. Uses function extensionality.

_______________
[1]. http://5ht.co/three.pdf
[2]. https://github.com/verimath/hit

04 апреля 2017, 21:00

Anton Salikhmetov

Еще одно введение в веревочковедение

После конференции TERMGRAPH в Эйндховене понял, что хорошо было бы иметь под рукой готовое быстрое введение одновременно в сети взаимодействия и исчисление взаимодействия. Вот что получилось из этой идеи.

Сети взаимодействия (interaction nets) - это структуры, подобные графам, состоящие из агентов (agents) и дуг. Агент типа α

имеет арность ar(α) ≥ 0. Если ar(α) = n, то агент α имеет n дополнительных портов (auxiliary ports) x1,..., xn в дополнение к его главному порту (principle port) x0. Все типы агентов принадлежат множеству Σ, называемому сигнатурой (signature). К любому порту можно присоединить не более одной дуги. Порты, которые не соединены ни одной дугой, называются свободными (free ports). Совокупность всех свободных портов в сети называется ее интерфейсом. Разводка (wiring) ω

состоит исключительно из дуг. Индуктивно определяемые деревья (trees)

соответствуют термам t ::= α(t1,..., tn) | x в исчислении взаимодействия (interaction calculus), где x называется именем (name).

С помощью разводок и деревьев любая сеть может быть представлена следующим образом:

что в исчислении взаимодействия будет соответствовать конфигурации (configuration)
<t1,..., tm | v1 = w1,..., vn = wn>,
где ti, vi, wi - некоторые термы. Последовательность t1,..., tm называется интерфейсом (interface), остальное же представляет собой мультимножество уравнений (equations). Разводка ω транслируется в выбор имен, и каждое имя обязано иметь ровно два вхождения в конфигурации.

Как и в λ-исчислении, в исчислении взаимодействия естественным образом определяются понятия α-конверсии и подстановки (substitution). Оба вхождения любого имени могут быть заменены на новое имя, если оно не участвует в данной конфигурации. Если терм t имеет ровно одно вхождение имени x, то подстановка t[x := u] определяется как результат замены имени x в терме t некоторым термом u.

Когда два агента соединены своими главными портами, они формируют активную пару (active pair). Для активных пар можно ввести правила взаимодействия (interaction rules), которые описывают, как активная пара будет заменена во время редукции сети взаимодействия. Графически любое правило взаимодействия можно преставить следующим образом:

где α, β ∈ Σ, а сеть N представлена с помощью разводок и деревьев в виде, пригодном для исчисления взаимодействия: в нотации Lafont это соответствует
a[v1,..., vm] >< β[w1,..., wn].
Говорят, что сеть без активных пар находится в нормальной форме (normal form). Сигнатура и множество правил взаимодействия вместе задают систему взаимодействия (interaction system).

Теперь рассмотрим пример для введенных конструкций, в котором участвуют часто использующиеся агенты ε и δ. В нотации Lafont правила взаимодействия для удаляющего (erasing) агента ε

записываются как ε >< α[ε,..., ε], а правила для дублирующего (duplicating) агента δ

выглядят следующим образом:
δ[α(x1,..., xn), α(y1,..., yn)] >< α[δ(x1, y1),..., δ(xn, yn)].
В качестве примера сети, в которой участвуют правила удаления и дублирования, возьмем простую сеть которая не имеет нормальной формы и редуцируется к самой себе:

В исчислении взаимодействия такая сеть соответствует конфигурации
<∅ | δ(ε, x) = γ(x, ε)> без интерфейса.

Редукция для конфигураций определяется более подробно, чем для сетей. Если
a[v1,..., vm] >< β[w1,..., wn], то следующая редукция:
<... | α(t1,..., tm) = β(u1,..., un), Δ> → <... | t1 = v1,..., tm = vm, u1 = w1,..., un = wn, Δ>
называется взаимодействием (interaction). Когда одно из уравнений имеет форму x = u, к конфигурации применимо разыменование (indirection), в результате которого другое вхождение имени x в некотором терме t будет заменено на терм u:
<...t... | x = u, Δ> → <...t[x := u]... | Δ> или <... | x = u, t = w, Δ> → <... | t[x := u] = w, Δ>.
Уравнение t = x называется тупиком (deadlock), если x имеет вхождение в t. Обычно рассматривают только сети, свободные от тупиков (deadlock-free). Вместе взаимодействие и разыменование задают отношение редукции на конфигурациях. Тот факт, что некоторая конфигурация c редуцируется к своей нормальной форме c', где мультимножество уравнений пусто, обозначают через c ↓ c'.

Если вернуться к примеру незавершающейся редукции сети, то бесконечная редукционная цепочка, начинающаяся с соответствующей конфигурации выглядит следующим образом:
<∅ | δ(ε, x) = γ(x, ε)> →
<∅ | ε = γ(x1, x2), x = γ(y1, y2), x = δ(x1, y1), ε = δ(x2, y2)> →*
<∅ | x1 = ε, x2 = ε, x = γ(y1, y2), x = δ(x1, y1), x2 = ε, y2 = ε> →*
<∅ | δ(ε, x) = γ(x, ε)> → ...

На нашем языке программирования, который подобен yacc(1)/lex(1) по структуре и лексически близок к LaTeX-нотации для исчисления взаимодействия, тот же самый пример можно записать следующим образом:
\epsilon {
        console.log("epsilon >< delta");
} \delta[\epsilon, \epsilon];

\epsilon {
        console.log("epsilon >< gamma");
} \gamma[\epsilon, \epsilon];

\delta[\gamma(x, y), \gamma(v, w)] {
        console.log("delta >< gamma");
} \gamma[\delta(x, v), \delta(y, w)];

$$

\delta(\epsilon, x) = \gamma(x, \epsilon);
Отметим, что наш язык программирования позволяет записывать побочные действия в императивном стиле, таким образом давая возможность исполнять произвольный код, включая ввод-вывод, а также условные множественные правила для пар вида αi >< βj в зависимости от значений i и j, которые могут быть произвольными данными, привязанными к агентам.

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

Сигнатура и арности агентов соответствующей системы взаимодействия автоматически выводятся при компиляции исходного кода программы на основе правил взаимодействия и начальной конфигурации. Правила взаимодействия вместе с их побочными действиями компилируются заранее, до начала редукции сети, при этом компилятор формирует таблицу для быстрого O(1)-поиска правил, соответствующих активным парам, во время последующего исполнения программы. После этого начальная конфигурация добавляется в FIFO-очередь уравнений, которая затем обрабатывается, пока она не станет пуста.

P. S. Недавно адаптировал этот текст и дополнил им статью на Википедии.

comment count unavailable comments

04 апреля 2017, 20:17

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

Idris 1.0

Make yourself unemployable (like I did) in 6 months with the book that recruiters don’t want you to know about

04 апреля 2017, 19:15

Российская Интеллигенция

Когда началась война ни один глубокоуважаемый господин из российского компьютер сайнс или математик не написал четкой позиции по этому вопросу. А как TOC в ЖЖ поменяли, так сразу Путин должен уйти в отставку. В отставку блядь! Не Гаага, нет, отставка!

04 апреля 2017, 07:52

01 апреля 2017

Scala@livejournal.com

Event Sourcing и Моноид

Вот говорят, что есть т.н. event sourcing, когда в базу записываются только event-ы, например
"изменить значения таких-то полей у такой-то instance-a такой-то entity", "удалить такой-то instance" и т.д. А потом по последовательности этих event-ов можно восстановить весь state.

Выглядит это восстановление так: каждый event превращается в функцию: State => State, которые потом "композируются". Поскольку A => A с операцией andThen образуют моноид, то процесс восстановения можно записать:
def createTransform(e: Event): State => State = ...
val transform = events foldMap createTransform
transform(state)
Логично ?
Даёт ли нам что-то использование абстракции моноида ?
Есть ли какие-нибудь примера использования моноида для event sourcing ?

написал Michael 01 апреля 2017, 15:53

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

Лучший отпуск в моей жизни

Как все-таки офигенно ничего не делать, а крутить лямбды и категории. Благодаря Владу я бросил работу и мы ходим с ним на лекции по Гомотопической Теории в НАН Украины. Инстайты продолжают струиться, нейронная сеть дышит полным своим дыханием. Как говорится, лучше с умным потерять, чем с дураком найти.

Влад не только трансформировал kievfprog, значительно повысив планку, отфильтровав примитивные доклады джаваскриптеров и кложуристов, но и делает, то, что называется фьюжин фундаментальной науки и инженерного искусства. Что интерсно, тусовка функциональных программистов Киева понравилась академикам, и теперь мы проводим регулярные семинары по четвергам. Например вот такие:



Я был приятно удивлен, увидев на семинаре бывших сотрудников doxtop с Плейтека, которые пишут там на scalaz и purescript с подачи доктора. Сам доктор, как и мы с Владом, не выдержал гнета гильд-энергии бабла и тоже решил дауншифнуться почитывая геометрические доклады про сигма слоения и их пи сечения.

Поэтому я решил написать этот пост. Я хочу, чтобы все кому интересно, то чем мы занимемся в Групоид Инфинити, нашли в себе силы потратить 2 часа ваших четвергов на семинары, которые проводит Вова совместно с НАН Украины :-) Для меня это площадка и возможность не придать забвению Пашину работу, а продолжить ее на академическом уровне привлекая лучших специалистов в этой области. Можете считать это моим извинением за обещанный доклад в прошлом году http://synrc.com/news/2016/groupoid.htm

В следующий четверг будет мой доклад про категорную семантику индуктивных типов, по материалам Вармо Вене, Николя Гамбино и Майкла Шульмана. На предыдущем семинаре был мой обзор Pure Type Systems и их конфигураций, по материалам Хенка Барендрехта.


Retracting Thursdays — Сергій Іванович Максименко показує відмінність ректрактів і домінації, голова відділу топології НАН України

АНОНС

Семінар
Похідні категорії та їх застосування
Гомотопічна теорія типів
15.30, Четвер, 06.04.17
Інститут математики
кім. 208 або конференц-зал 305
Максим Сохацький
Категорна семантика індуктивних типів

Бажано знайомство з теорією категорій — категорії, функтори, природні перетворення, монади — наприклад, з http://5ht.co/cat.pdf
і лямбда-численням – наприклад, з http://5ht.co/pts.pdf
Модератор: Володимир Васьльович Любашенко

Слайди з перед-семінарського обговорення:
https://groupoid.space/tex/cub/Cubical%20Type%20Theory.pdf

01 апреля 2017, 03:14

31 марта 2017

ruhaskell.org

Haskell: цель или всё-таки средство?

Я вижу большую проблему в Haskell-сообществе. Вот мои сумбурные мысли на сей счёт.

написал Денис Шевченко 31 марта 2017, 00:00

29 марта 2017

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

Групоид Инфинити открывает свой репозиторий Coq пакетов

С коком такая тема, что не все пакеты обновляются часто, никому не нужны FTC, Category Theory, CoInduction свойтва на последних коках. Последний — 8.6 — вышел в декабре 2016, а у всех пакетов в OPAM стоит жестко меньше 8.6. Они там язык тактик поменяли, и улучшлили тайпчек вселенных.

Демонстрировать кому-то всю силу кока приходится на своем компе, и простых инструкций взять и склонировать что-то для известных теорем нет. Более того, не все теоремы есть в OPAM, много просто валяются на ftp серверах унивеситетов.

Поэтому в соответствии с парадигмой "Грабь и Воруй" я принял решение сделать свой репозиторий пакетов под игидой Групоид Инфинити. Делаю я это для того, чтобы крамсать код пакетов в (само)-образовательных целях и публикации статей по основаниями математики с примерами кок-термов. Следите за сайтом Групоид Инфинити, а также языком Infinity Language.

Итак, встречайте, кодовое название проекта "Вери Мас Сач Вау" https://github.com/verimath Логотип тупо ноль — обозначает начальный уровень Кунг-фу в Зависимой теории :-)



Хочу сделать максимальный smooth экспириенс для математиков и академии, чтобы студенты могли очень просто начать разрабатывать на коке. Смешно, но даже матерые коко-писатели из НАН не знают как накатить HoTT патчи и чекнуть гомотопические теоремы.

Хочу, чтобы простая последовательность действий всегда позволяла запустить любой наш репо на последнем коке. У чуваков культуры оформления вообще никакой, какие-то перл скрипты, беш скрипты — представьте, что вы говорите математику на виндовсе поставить перл и беш, чтобы у вас работали теоремы. Вообщем, я это все повыбрасывал и оставил только coq_makefile. В репозиториях ничего кроме коковских файлов нет и все собирается простой последовательностью команд:

$ brew install opam
$ opam install coq
$ git clone http://github.com/verimath/topology && cd topology
$ coq_makefile -f Make -o Makefile
$ make

Начал я с таких тем-репозиториев — все рабочие (только ftc wip):

1. topology — общая топология + лемма Цорна
2. co — первый коиндуктивный репл-шелл на коке
3. real — действительные числа, как коиндуктивные стримы цифр
4. termination — терминальная категорная семантика коиндуктивных стримов
5. set — теория множеств Тарского-Гротендика
6. interpreter — интерпретатор гомотопической теории
7. ftc — основная теорема анализа по предложению риалити хакера
8. lambda — нетипизированное лямбда исчисление как инициальный объект категории экспоненциальных монад

Пакеты можно будет добавлять так:

$ opam repo add coq-released https://groupoid.space/opam

Делаем зависимые лямбда термы ближе к народу!

29 марта 2017, 02:20

nponeccop

Хачим oczor

31 files changed, 356 insertions(+), 462 deletions(-)

29 марта 2017, 00:12

28 марта 2017

ruhaskell.org

CoLaboratory.RuHaskell.2017.Весна

Анонс митапа 6 апреля сообщества RuHaskell и Лаборатории Касперского.

написал Денис Шевченко 28 марта 2017, 00:00

26 марта 2017

nponeccop

Экстракшен

https://hal.archives-ouvertes.fr/file/index/docid/338973/filename/letouzey_extr_cie08.pdf

Долго длившийся односторонний "спор" с maxim по поводу правомерности использования термина "extraction" закрыт в его пользу.

Отец кок-экстрактора Pierre "какой-то студент" Letouzey употребляет этот термин вольно через предложение в статье по ссылке. Также на эту работу ссылаются пейперы по F* и так же вольно употребляют extraction.

В-общем, на то что extraction это превращение прувов в программы - можно забить. Все всё равно превращают только программы в программы, а CHI-экстракция остаётся не более чем любопытным курьёзом.

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

26 марта 2017, 03:05

25 марта 2017

nponeccop

Новости хакатона

Создал тучу тасок по окзору: https://github.com/ptol/oczor/issues/10

В-основном это что-то типа линта, можно все скопом одним коммитом/PR лепить. Ну и делать аналогичное в других файлах, благо там конь не валялся. Главное не переусердствовать. Линейный композиционный стиль - ок, но как начинаются выкрутасы лучше остановиться.

По HNC посрывали низковисящие фрукты, но осталось ещё немного.

25 марта 2017, 03:27

24 марта 2017

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

Cubical Type Theory in a Topos

Axioms:

ax1 : [∀(φ:I Ω).(∀(i:I).φi∨¬φi)⇒(∀(i:I).φi)∨(∀(i:I).¬φi)]
ax2 : [¬(0 = 1)]
ax3 : [∀(i:I).0⊓x=0=x⊓0 ∧ 1⊓x=x=x⊓1] 
ax4 : [∀(i:I).0⊔x=x=x⊔0 ∧ 1⊔x=1=x⊔1].
ax5 : [∀(i:I). cof(i=0) ∧ cof(i=1)]
ax6 : [∀(φψ:Ω). cofφ⇒cofψ⇒cof(φ∨ψ)]
ax7 : [∀(φψ:Ω). cofφ⇒(φ⇒cofψ)⇒cof(φ∧ψ)].


____________________________
[1] https://www.cl.cam.ac.uk/~rio22/pdf/Fields-talk.pdf
[2] http://drops.dagstuhl.de/opus/volltexte/2016/6564/pdf/LIPIcs-CSL-2016-24.pdf
[3] http://www.cl.cam.ac.uk/~rio22/agda/cubical-topos/root.html

24 марта 2017, 00:59

22 марта 2017

nponeccop

N2O.hs погнил

- в зависимости HJavascript почему-то перестали работать констрейнты на суперклассы. Т.е. class Show a => IsClass a, и в функции с IsClass a => a -> Foo требуетcя теперь констрейнт Show a.
- перестал работать фейковый инстанс Data для Connection из WebSocket (который абстрактный тип, не экспортирующий конструкоры). Задам ща вопрос на SO.

22 марта 2017, 19:10

21 марта 2017

nponeccop

Прогресс по хакатону-2

У нас уже 15 коммитов, в-основном однострочные рефакторинги, от 3 участников: xgromxx, yury-panchin и ingvar-lynn. И 6 служебных коммитов от меня.

Задания-однострочники описаны в двух тасках:

https://github.com/nponeccop/HNC/issues/97
https://github.com/nponeccop/HNC/issues/82

Помимо этого можно делать всё что хочется :)

21 марта 2017, 20:50

20 марта 2017

David Sorokins WebLog

GPSS на Haskell

Если кто еще не знает, GPSS - это один из самых известных специализированных языков дискретно-событийного моделирования. Так вот, я добавил в AivikaSim [http://www.aivikasoft.com/ru/products/aivikasim.html] поддержку GPSS-подобного предметного-ориентированного языка. Это пакет aivikasim-gpss [https://github.com/dsorokin/aivikasim-gpss]. Вот здесь находится работающий тестовый пример [https://github.com/dsorokin/aivikasim-gpss-test].

Постарался охватить основные моделирующие блоки, такие как SEIZE, PREEMPT, GATHER, ASSEMBLE, MATCH. Другие либо имеют явные аналоги у меня, либо требуют небольшого программирования как в случае блоков LINK и UNLINK. Не гарантируется точного совпадения результатов с GPSS World, так как логика работы с транзактами у меня совершенно иная, но в некоторых случаях результаты получаются очень близкими.

Вот, здесь примеры моделей [https://github.com/dsorokin/aivikasim-gpss/tree/master/examples] из красной книги Шрайбера по GPSS. Там в начале каждого примера приводится соответствующий код модели на языке GPSS World. Можно сличить результаты.

Example2A.hs означает, что это пример 2A из книги, а вот Example7-26.hs означает, что это соответствует модели на рисунке 7.26. Модели с окончанием Trans, такие как Example2BTrans.hs, означают, что там используется обобщенная версия AivikaSim. Фактически это означает, что приведенный код готов для использования в распределенной имитации.

Более того, пример Example7-26Distributed.hs непосредственно запускается через модуль распределенного моделирования. В данном случае это формально последовательная модель, но запускается она фактически в виде распределенной, т.е. она готова для кластера компьютеров. Используется оптимистичный алгоритм деформации времени.

Сразу напишу, что хотя для приведенных моделей удалось добиться очень хорошего соответствия с GPSS, то вот для примера 5D из книги Шрайбера такого близкого соответствия, скорее всего, не получится. Сейчас совпадение идет в 9 случаях против одного, где модель будет уже другой. Причем, совпадает даже на очень нетривиальных моделях, где важен порядок обработки транзактов.

Касательно скорости моделирования. Модуль GPSS-подобного языка последовательной версии AivikaSim моделирует примерно в 5-7 раз медленнее, чем GPSS World, но зато позволяет использовать разные методы в рамках одной модели, например, агенты и события. Для сравнения, распределенный модуль AivikaSim на последовательных задачах медленнее в раз 6-9, чем последовательная версия AivikaSim, но зато распределенную версию можно запустить много раз на разных узлах в рамках одной модели. Например, можно запустить 7 параллельно работающих локальных процессов на одной системе с 8-ядерным процессором.

Если кто захочет проверить результаты, то вот руководство по установке AivikaSim [https://github.com/dsorokin/aivikasim-installer].

написал dsorokin (noreply@blogger.com) 20 марта 2017, 20:56

19 марта 2017

Anton Salikhmetov

Лямбды на веревочках с рюшечками

Большие новости!

Я доделал needed reduction на веревочках, почистил лямбду от уродской waiting construct, сделал closed reduction дефолтным алгоритмом и обновил браузерную демку. Там теперь есть бесконечная прокрутка для дебага. Зацените рюшечки:

https://codedot.github.io/lambda/

Приятно иметь калькулятор в браузере, который одновременно печатает полную βη-нормальную форму для любого бестипового λK-терма и при этом считает 10 2 2 1 в цифрах Черча за долю секунды на моем Хромбуке.

Напомню, что 21024 примерно в (1017)4 раз больше, чем гиперобъем пространства-времени всей наблюдаемой вселенной с момента большого взрыва в планковских единицах измерения, в наши дни имеющий порядок (1060)4 планковских единиц.

Вот.

comment count unavailable comments

19 марта 2017, 17:43