sea

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".
sea

Свисс Эмоушинс

Когда у меня еще не было паспорта, из всей Европы мне не хотелось побывать нигде. Я вырос в европейском городишке, по сути ебаное село 100 тыс населения в 400 км от Киева на юг, но очень красивое. Когда старшие друзья мне показывали свои фотки Саграды де Фамилия упоротого Гауди и шотландские замки у меня хуй не ставал ни на что, потому что в Каменце-Подольском, где я родился, была и есть своя крепость, и свой архитектурный фьюжин 7 народов (евреев, поляков, армян, турков, литовцев, украинцев, русских), и желания ездить в Еропу, чтобы повтыкать на очередной замок, собор, костёл или маленькие улочки с ресторанчиками, не было никакого — все это я и так видел.

Но Швейцария другое дело, я туда всегда хотел попасть, прямо таки незакрытый гештальт. Просто я был нищебродом и просить делать визу у друзей не было никакого желания, даже если вы и считаете, что это не унижение.  Но как вы знаете, нам дали БЕЗВИЗ и первым делом я решил закрыть детские травмы, побывав в самой дорогом городе Европы и самой дорогой стране и определить — наконец нищеброд я или нет.

Приблизительно я набросал такой план на 4 дня:

Tickets: 1000, Hotel: 2000, Per Day: 500 x 4 = 2000, Airport Gifts: 500

Пятерочку должен осилить каждый Java-синьор, поэтому если у вас тоже не закрыт гештальт можете ориентироваться на меня. Написав эту СМС своей жене с предварительным планом, она забукала такие отели:

1. ZenCity (Geneva), 2. Eden (Montreux), 3. Mirador (Vevey), 4. AirBnB

Collapse )
sea

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
sea

N2O over MQTT + KVS



Пришла пора завернуть весь стек протоколов N2O в какой транспорт, который поддерживает, что-то более сложное чем ACK, такой транспорт — MQTT, он легковеснее AMQP, который, давайте без обид, порос кольцами уже, как и riak. Вообщем, пока emqtt.io еще позволяет, нужно быстро форкануться и повыбрасывать оттуда половину либ.

Из чего состоит EMQ — компания производитель EMQ Enterprise, Inc, автор Feng Lee. В основе лежит esockd — очередной неблокирующий сервер (типа ranch), в качестве веб сервера используется mochiweb, его же и вебсокеты.

emqtt.io — это пример как нужно писать приложения, минимальная документация, отпидерашеный код, приятно работать. Только там все на lager завязали и в итоге, чтобы залогировать нужно lager, lager_syslog, gen_logger, goldrush, syslog. Поэтому пришлось форкануть это все. Или просто выброосить, но lager в продакшине любят, так как проверен. Ладно не буду пока удалять.

Теперь о рекомендациях по общей архитектуре. Стек протоколов N2O я вижу как федерацию, аналогичную CORBA/OASIS/XMPP поверх различных транспортов. До этого — это был BERT/JSON кодировка over WS/WSS транспорт, теперь качество и количество транспортов расширилось до MQTT over WS/WSS, TCP/TLS. Т.е. появился базовый посредник, с ack+pubsub+presence+ping протоколом, соответственно N2O HEART ["PING","N2O,"] протокол уже не нужен. Такая версия N2O расширит области применения. С другой стороны дополнительное кодирование MQTT и его заголовки будут потреблять больше ресурсов.

Официальный MQTT JavaScript клиент от IBM: https://github.com/voxoz/mq/blob/master/apps/emq_dashboard/priv/www/assets/js/mqttws31.js Будем его резать и интегрировать в N2O. Есть альтернативный mqtt.js — но там как-то слишком адово как по нашим меркам. Для джаваскриптеров такое в порядке вещей считается.

MQTT как сервер приложений. Ну какие могут быть приложения у MQTT — коннектить устройства IoT. Чтобы реализовать перситенс — нужно имплементировать публичные хуки MQTT протокола:

load(Env) ->
    emqttd:hook('client.connected', fun ?MODULE:on_connected/3, [Env]),
    emqttd:hook('client.disconnected', fun ?MODULE:on_disconnected/3, [Env]),
    emqttd:hook('client.subscribe', fun ?MODULE:on_subscribe/3, [Env]),
    emqttd:hook('client.subscribe.after', fun ?MODULE:on_subscribe_after/3, [Env]),
    emqttd:hook('client.unsubscribe', fun ?MODULE:on_unsubscribe/3, [Env]),
    emqttd:hook('message.publish', fun ?MODULE:on_publish/2, [Env]),
    emqttd:hook('message.delivered', fun ?MODULE:on_delivered/3, [Env]),
    emqttd:hook('message.acked', fun ?MODULE:on_acked/3, [Env]).


Вообщем-то это все, что нужно знать людям, которые принимают решения. Инструкция для mad хипстеров не признающих rebar, mix и hex:

$ brew install erlang
$ curl -fsSL https://raw.github.com/synrc/mad/master/mad > mad \
              && chmod +x mad \
              && sudo cp /usr/local/bin
$ git clone git://github.com/voxoz/mq && cd mq
$ mad dep com rep
Configuration: [{emq_dashboard,
                    [{listeners_dash,
                         [{http,18083,[{acceptors,4},{max_clients,512}]}]}]},
                {emqttd,
                    [{listeners,
                         [{http,8083,[{acceptors,4},{max_clients,512}]}]},
                     {sysmon,
                         [{long_gc,false},
                          {long_schedule,240},
                          {large_heap,8000000},
                          {busy_port,false},
                          {busy_dist_port,true}]},
                     {session,
                         [{upgrade_qos,off},
                          {max_inflight,32},
                          {retry_interval,20},
                          {max_awaiting_rel,100},
                          {await_rel_timeout,20},
                          {enable_stats,off}]},
                     {queue,[]},
                     {allow_anonymous,true},
                     {protocol,
                         [{max_clientid_len,1024},{max_packet_size,64000}]},
                     {acl_file,"etc/acl.conf"},
                     {plugins_etc_dir,"etc/plugins/"},
                     {plugins_loaded_file,"etc/loaded_plugins"},
                     {pubsub,
                         [{pool_size,8},{by_clientid,true},{async,true}]}]},
                {emq_modules,
                    [{modules,
                         [{emq_mod_presence,[{qos,1}]},
                          {emq_mod_subscription,[{<<"%u/%c/#">>,2}]},
                          {emq_mod_rewrite,
                              [{rewrite,"x/#","^x/y/(.+)$","z/y/$1"},
                               {rewrite,"y/+/z/#","^y/(.+)/z/(.+)$",
                                   "y/z/$2"}]}]}]},
                {kvs,
                    [{dba,store_mnesia},
                     {schema,[kvs_user,kvs_acl,kvs_feed,kvs_subscription]}]},
                {n2o,[]}]
Applications:  [kernel,stdlib,gproc,lager_syslog,pbkdf2,asn1,gen_logger,
                mnesia,compiler,inets,crypto,syntax_tools,xmerl,kvs,esockd,
                goldrush,public_key,lager,ssl,mochiweb,emqttd,mad,sh,syslog]
Erlang/OTP 19 [erts-8.2] [source] [64-bit] [smp:4:4] [async-threads:10] [hipe] [kernel-poll:false] [dtrace]

Eshell V8.2  (abort with ^G)
1> 19:17:23.670 [info] Application lager started on node nonode@nohost
19:17:23.746 [info] Application ssl started on node nonode@nohost
19:17:23.749 [info] Application mochiweb started on node nonode@nohost
starting emqttd on node 'nonode@nohost'
Nonexistent: []
emqttd ctl is starting...[ok]
emqttd hook is starting...[ok]
emqttd router is starting...[ok]
emqttd pubsub is starting...[ok]
emqttd stats is starting...[ok]
emqttd metrics is starting...[ok]
emqttd pooler is starting...[ok]
emqttd trace is starting...[ok]
emqttd client manager is starting...[ok]
emqttd session manager is starting...[ok]
emqttd session supervisor is starting...[ok]
emqttd wsclient supervisor is starting...[ok]
emqttd broker is starting...[ok]
emqttd alarm is starting...[ok]
emqttd mod supervisor is starting...[ok]
emqttd bridge supervisor is starting...[ok]
emqttd access control is starting...[ok]
emqttd system monitor is starting...[ok]
Plugins: [{mqtt_plugin,emq_auth_username,"2.1.1",
                       "Authentication with Username/Password",false},
          {mqtt_plugin,emq_dashboard,"2.1.1","EMQ Web Dashboard",false},
          {mqtt_plugin,emq_modules,"2.1.1","EMQ Modules",false},
          {mqtt_plugin,emq_persistence,"1.1.2","Synrc KVS for MQTT",false}]
Names: [emq_dashboard,emq_modules,emq_persistence,emq_auth_username]
dashboard:http listen on 0.0.0.0:18083 with 4 acceptors.
19:17:25.705 [info] started Apps: [emq_dashboard]
19:17:25.705 [info] load plugin emq_dashboard successfully
19:17:25.705 [info] Application emq_dashboard started on node nonode@nohost
Load emq_mod_presence module successfully.
Load emq_mod_subscription module successfully.
Load emq_mod_rewrite module successfully.
19:17:25.802 [info] started Apps: [emq_modules]
19:17:25.802 [info] load plugin emq_modules successfully
19:17:25.802 [info] Application emq_modules started on node nonode@nohost
19:17:25.848 [info] started Apps: [emq_persistence]
19:17:25.848 [info] load plugin emq_persistence successfully
19:17:25.849 [info] Application emq_persistence started on node nonode@nohost
19:17:25.895 [warning] CLI: users is overidden by {emq_auth_username,cli}
19:17:25.895 [info] started Apps: [emq_auth_username]
19:17:25.895 [info] load plugin emq_auth_username successfully
19:17:25.895 [info] Application emq_auth_username started on node nonode@nohost
mqtt:ws listen on 0.0.0.0:8083 with 4 acceptors.
emqttd 2.1.1 is running now
19:17:25.897 [info] Application emqttd started on node nonode@nohost
19:17:25.904 [info] Application mad started on node nonode@nohost
19:17:25.957 [info] Application sh started on node nonode@nohost
19:17:26.043 [info] Application syslog started on node nonode@nohost


Open http://127.0.0.1:18083/#/websocket with admin:public credentials, Press Connect, Subscribe, Send and observe statistics http://127.0.0.1:18083/#/overview.





sea

Compiling to Categories

Ok, here's my equation for the solver, written in plain Haskell:

equation :: (Num a, Ord a) => a -> a -> Bool
equation x y =
    x < y &&
    y < 100 &&
    0 <= x - 3 + 7 * y &&
    (x == y || y + 20 == x + 30)


Here's how I run the solver:

    res <- evalZ3With Nothing opts $ do
        x <- mkFreshIntVar "x"
        y <- mkFreshIntVar "y"
        PrimE ast <-
            runKleisli (runZ3Cat (ccc @Z3Cat (uncurry (equation @Int))))
                       (PairE (PrimE x) (PrimE y))
        assertShow ast
        -- check and get solution
        fmap snd $ withModel $ \m ->
            catMaybes <$> mapM (evalInt m) [x, y]
    case res of
        Nothing  -> error "No solution found."
        Just sol -> do
            putStrLn $ "Solution: " ++ show sol


And here's the result, which also show you the equation we submitted to Z3:

(let ((a!1 (ite (<= 0 (+ (- x!0 3) (* 7 y!1)))
                (ite (= x!0 y!1) true (= (+ y!1 20) (+ x!0 30)))
                false)))
  (ite (< x!0 y!1) (ite (< y!1 100) a!1 false) false))

Solution: [-8,2]


Now with one function, I have either a predicate that I can use in Haskell code, or an input to Z3 for finding possible arguments for which it is true!
</pre>

______________
[1]. https://github.com/conal/concat/issues/4
[2]. http://conal.net/papers/compiling-to-categories/compiling-to-categories.pdf
sea

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

Конгруэнтная функция 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
sea

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

Ужасный звук + украинский язык = Категорная Семантика Индуктивных типов