Russian Lambda Planet

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

Scala@livejournal.com

property-based testing для бедных

Допустим, нам нужно протестировать функцию fetch, которая возвращает Foo
case class Foo(name: String)
def fetch(name: String):Foo = ???
Тест должен проверить, что функция работает для разных name: ASCII alphanumeric, ASCII non-alphanumeric, non-ASCII и так далее.

Для этого у нас есть тест на specs2 :
class FetchFooSpec extends SpecificationWithJUnit {

  def matchFoo(name: String): Matcher[Foo] = {foo: Foo => (foo.name == name, s"$foo.name != $name"}

  "fetchFoo should handle ASCII alphanumeric names" {
     fetchFoo("abc") must matchFoo("abc")
   }
   "fetchFoo should handle names with slashes" {
     fetchFoo("a/b/c") must matchFoo("a/b/c")
   }
   "fetchFoo should handle names with dots" {
     fetchFoo("a.b.c") must matchFoo("a.b.c")
   }
   "fetchFoo should handle non-ASCII names" {
     fetchFoo("אבג") must matchFoo("אבג")
   }
}
Чтобы избавиться от бойлерплейта можно сделать так:
def testFetch(name: String):Either[String, Unit] = {
  val foo = fetchFoo(name)
  if (foo.name == name) Left(s"$foo.name != $name") else Right(())
}

import cats.implicits._
def testFetch2(names: List[String]): Either[String, Unit] = 
  (names map testFetch)
    .foldMap(_.toValidatedNel)
    .toEither
    .leftMap(_.toList.mkString(", "))

"fetchFoo should handle all names" {
   val names = List("abc", "a/b/c", "a.b.c", "אבג")
   testFetch2(names) must beRight
}
Можно ли это упростить и улучшить ? Как добавить сюда генератор для names ?

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

10 января 2017

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

Safe and Static Methods for Memory Management

https://github.com/critiqjo/seminar-report/files/280495/report.pdf

Dirty Notes: MIR has Linear Type System, as drop is exposed explicitly. While Rust has Affine Type System, while must_use is not enforcing to consume values. Linear type systems are the internal language of closed symmetric monoidal categories

Addition: http://pauillac.inria.fr/~fpottier/slides/fpottier-2007-05-linear-bestiary.pdf
Categorical Semantic of Linear Type Systems: https://www.irif.fr/~mellies/papers/panorama.pdf

10 января 2017, 13:22

09 января 2017

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

Последний гвоздь в гроб Хаскеля/C++ в этом году!

TL;DR Больше микробенчмарков богу микробенчмарков!

Дошли руки до микробенчмарков, где известные фокусники всея Руси -- Лев Валкин и Сергей Зефиров тролят байтойобов и показывают, что если разложить Data Flow в свободные монады то получится что стрим можно выгребать пачками (генерируются MMX инструкции). Сегодня мы покажем, что в нашем цирке (Rust) иллюзионисты не хуже, а может быть даже и лучше.

Итак, как говорят хранители интернета, мы можем это написать двумя способами:

1. Циклы
2. Итераторы

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

#![feature(step_by)]

pub fn lpa(sz: usize, iter_num: usize, ) -> usize {
    let mut sum = 0_usize;
    for e in 0..sz {
        sum = 0;
        let mut x: Vec = Vec::with_capacity(iter_num);
        for i in 0..iter_num {
            x.push(i);
        }
        let mut y: Vec = Vec::with_capacity(iter_num - 1);
        for i in 0..iter_num - 1 {
            y.push(x[i] + x[i + 1]);
        }
        for i in (0..iter_num).step_by(100) {
            sum += y[i];
        }
    }
    sum
}

pub fn lpv(iter_num: usize, sz: usize) -> usize {
    let sums: Vec_> = (0..iter_num)
        .map(|_| {
            let x: Vec_> = (0..sz).map(|i| i).collect();
            let y: Vec_> = x.iter().zip(x.iter().skip(1)).map(|(x, y)| x + y).collect();
            (0..sz).step_by(100).map(|i| y[i]).sum()
        })
        .collect();
    *sums.last().unwrap()
}

fn main() {
    println!("{:?}", lpa(20, 1000000));
}

$ rustc -O main-lpv.rs

$ time ./main-lpv
9999010000

real	0m0.055s
user	0m0.044s
sys	0m0.008s

$ time ./main-lpa
9999010000

real	0m0.107s
user	0m0.096s
sys	0m0.012s


Теперь сишечка:

#include <stdint.h>
#include <vector>
#include <iostream>

int main() {
    int64_t sum = 0;

    for(int e = 0; e < 20; e++) {
        sum = 0;

        std::vector<int64_t> x;
        x.reserve(1000000);
        for(int i = 0; i < 1000000; i++) {

            x.push_back(i);
        }

        std::vector<int64_t> y;
        y.reserve(1000000-1);
        for(int i = 0; i < 1000000-1; i++) {
            y.push_back(x[i] + x[i+1]);
        }

        for (int i = 0; i < 1000000; i += 100) {
            sum += y[i];
        }
    }

    std::cout << sum << std::endl;
}

g++ main-c.cc -Ofast -march=native -funroll-loops  -o main-c
$ time ./main-c
9999010000

real	0m0.129s
user	0m0.100s
sys	0m0.028s


Теперь божественная "неоптимизированная" ГеАшЦешечка


{-# LANGUAGE ParallelListComp #-}
import Control.Monad

main = times 20 (compute 1000000) >>= print
    where
        times n m = do
            results <- replicateM n m
            return ((sum results) `seq` (head results))

compute n = do
    let xs = [0 .. (n-1)]
        ys = [x+k | x <- xs | k <- drop 1 xs]
    return $ sum $ map snd $ filter fst [((i`mod`100)==0,y) | y <- ys | i <- [0,1..]]


$ ghc -O3 -o main-hs ./main-hs.hs
$ time ./main-hs
9999010000

real	0m0.115s
user	0m0.108s
sys	0m0.004s


По требованию трудящихся на арену выходит божественный ЛуаДЖИТик:

ffi=require('ffi')                                                                                                                              
jit.opt.start("hotloop=5", "loopunroll=100", "instunroll=100")                                                                                  
jit.flush()                                                                                                                                     
                                                                                                                                                
local ct=ffi.typeof('int64_t[?]')                                                                                                               
                                                                                                                                                
function lpa(size, iter_num)                                                                                                                    
    local sum                                                                                                                                   
    for e=0,size-1 do                                                                                                                           
        sum=0LL                                                                                                                                 
        local x=ffi.new(ct, iter_num)                                                                                                           
        for i=0,iter_num-1 do                                                                                                                   
            x[i]=i                                                                                                                              
        end                                                                                                                                     
        local y=ffi.new(ct, iter_num-1)                                                                                                         
        for i=0,iter_num-2 do                                                                                                                   
            y[i]=x[i]+x[i+1]                                                                                                                    
        end                                                                                                                                     
        for i=0,iter_num-1,100 do                                                                                                               
            sum = sum + y[i]                                                                                                                    
        end                                                                                                                                     
    end                                                                                                                                         
    return sum                                                                                                                                  
end                                                                                                                                             
                                                                                                                                                
print(lpa(20, 1000000))                                                                                                                         
os.exit(1)  

$ time luajit lpa.lua
9999010000LL

real	0m0.099s
user	0m0.032s
sys	0m0.064s


Swift и Go -- ниже дна (С++). Поэтому эту хуйню даже ставить на машину не буду. Свифт лично мне нравится и желаю ему взросления, но его не будет так как Apple не технологичная компания уже (хотя за LLVM низкий поклон). С Go чуда не будет -- язык откровенно делался плохим (как и С++), поэтому его любят гидроцефалы с лоботомией пишущих лапшу вида if err != nil. Если видете чувака, который рекламиурет Go -- знайте, ебанат, инфа 100%. До существования Go эти люди называли себя системными администраторами (POSIX, KISS, UNIX, Керниган и Ритчи головного мозга), теперь гугл их пересадила из беша в гошечку. А мы вернемся из благодатного оазиса рассовой ненависти в лоно микробенчмарков.

Раздача шампанского:

Lang             ms
--------------- ---
Rust Iterators   55
LuaJIT 2.1       99
Rust Arrays     107
GHC             115
C++             119


С Новым Годом, Сережа и Лев!
Всем желаю успешного байтойобства и глубокого аппликативного фьюжена в 2017!

09 января 2017, 13:26

07 января 2017

nponeccop

Ложь, наглая ложь и TIOBE

Нашел тут пост полугодичной давности: http://nponeccop.livejournal.com/490132.html

В мае около-фя распределялись так:

R, Matlab, Scheme, Lisp, Scala, Prolog, F#, Haskell, Erlang, Q

В декабре:

R, Matlab, Haskell, F#, Scala, Lisp, Q, Prolog, Scheme, Erlang

Всплыли Haskell, F# и Q за счёт Пролога, Схемы, Лиспа и.. Эрланга.

Вовремя же наш расстреливающий неугодных фашист Максим перестал на нём писать! А может как раз наоборот - Макс и Лев перестали, и поэтому он просел!

07 января 2017, 00:18

05 января 2017

03 января 2017

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

O-CPS SPEC

Если бы O-CPS был PhD :-)

1. Синтаксис. Модифицированный lalrpop (убраны типы-аттрибуты и несущественные элементы, отсутствуют терминалы, можно найти в предыдущих постах).

E: V | A | C
NC: ";" = [] | ";" m:NL = m
FC: ";" = [] | ";" m:FL = m
EC: ";" = [] | ";" m:EL = m
NL: NAME | o:NAME m:NC = Cons o m
FL: E | o:E | m:FC = Cons o m
EL: E | EC  | o:E m:EC = Cons o m
V: v:V = Verb v [] [] | v:V r:E = Verb v [] r
A: a:A = Adverb a [] [] | v:A r:E = Adverb v [] r
C: N | c:N a:C = Call c a | l:N a:A = Adverb a l [] | l:N v:V = Verb v l []
     | l:N a:A r:E = Adverb a l r | l:N v:V r:E = Verb v l r
N: NAME | S | HEX | L | D | F
D: "[" "]" = [] | "["  l:EL "]" = Dict l
L: "(" ")" = [] | "([" c:NL "]" m:FL ")" = Table c m | "(" l:EL ")" = List l
F: "{" "}" = Lambda [] [] [] | "{[" c:NL "]" m:EL "}" = Lambda [] c m
                             | "{" m:EL "}" = Lambda [] [] m

2. Порт Rust в System F (убраны лайфтаймы).
lazy n (Assign n b)               e k = D n b (ContAssign n k)
     n (Cond v a l)               e k = D n v (ContCond l r k)
     n (List l)                   e k = eve n l e k
     n (Call c a)                 e k = D n a (ContCall c k)
     n (Verb v (Number _) r)      e k = D n r (ContVerb v l 0 k)
     n (Verb v _ (Number _))      e k = D n v (ContVerb v r 1 k)
     n (Verb v x y)               e k = D n x (ContVerb v y 0 k)
     n (Name s)                   e k = cont (lookup n s e) k
     n (Lambda _ x y)             e k = cont ((Lambda n x y) n) k

evf  n (Lambda c x y) a e k = cont (y (if (= c []) n c)) (ContFunc x a k)
     n       (Name s) a e k = lookup n s e
eve  n       (Cons a d) e k = D n a (ContExpr d k)
     n              Nil e k = cont n Nil e k
     n                a e k = D n a k
emr            (Dict x) e k = R Dict (rev x)
             (Cons x y) e k = R Dict (Cons (rev x) (rev x))
                      a e k = R a
run  D              n a e k = lazy n a e k
     R                a     = a

cont n (Dict v) e (ContCall c k)          = evf n c v e k
     n x        e (ContCall c k)          = evf n c x e k
     n x        e (ContFunc s a k)        = eve (e.define_args s (rev a)) v k
     n False    e (ContCond l r k)        = D n r k
     n True     e (ContCond l r k)        = D n l k
     n x        e (ContCond l r k)        = D n x (ContCond l r k)
     n x        e (ContAssign (Name s) k) = eve n (e.define s x) k
     n x        e (ContExpr (Cons a d) k) = eve n (Cons a d) k
     n x        e (ContExpr r k)          = cont n x k
     n x        e  ContRet                = emr x e k

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

rssh

The Exp=Log normal form of types. Danko Ilik.

Написано давно, но я вот только сейчас в POPL17 ее прочитал (см. препринт https://arxiv.org/abs/1502.04634 )
Широкоизвестно что в typed lambda-calculus типы образуют экспотенциальное кольцо и могут быть представлены как арифметические выражения, где +, *, exp обозначают соответственно (a|b), (a,b), a->b

Danko предлагает использовать формальные алгебраические преобразования exp и log для нормализации lambda-термов что-бы получить какое-то приближение конструктивной процедуры для Tarski High School Identities Problem. Нормализация, правда получилась неполная: bn редукция порождает расхождения, но типа лучше чем ничего

03 января 2017, 23:16

02 января 2017

ru_declarative

предикаты высшего порядка и унификация

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

Я знаю один яп (Oz), включающий Пролог, в котором предикаты унифицируются iff их адреса равны, и такая унификация не считается ошибкой. (Например, в Прологе выполнение арифметической операции на несвязанных (not instantiated) переменных является ошибкой.) Как эта проблема решена в других Прологах?

написал beroal 02 января 2017, 12:16

29 декабря 2016

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

Lambda Term Exponential Explosion

nponeccop поставил вопрос и был получен прекрасный ответ который хочется процитировать.

q:(nat->nat->nat)->nat->nat->nat = \f:(nat->nat->nat).(\a b:nat.f (f a b) (f a b))

q p => \a b.p (p a b) (p a b)

q (q p) => \c d.q p (q p c d) (q p c d) 
  => \c d.q p (p (p c d) (p c d)) (p (p c d) (p c d))
  => \c d.p (p [p (p (p c d) (p c d))] [p (p (p c d) (p c d))]) (p [p (p (p c d) (p c d))] [p (p (p c d) (p c d))])



Section Expand.

Variable nat:Type.

Variable p:nat->nat->nat.

Definition q:(nat->nat->nat)->nat->nat->nat :=
  fun f:(nat->nat->nat) => fun a b:nat => f (f a b) (f a b).

Eval compute in (q p).
(*
  = fun a b : nat => p (p a b) (p a b)
     : nat -> nat -> nat
*)

Eval compute in (q (q p)).
(*
  = fun a b : nat =>
       p (p (p (p a b) (p a b)) (p (p a b) (p a b)))
         (p (p (p a b) (p a b)) (p (p a b) (p a b)))
     : nat -> nat -> nat
*)

Eval compute in (q (q (q p))).
(*
     = fun a b : nat =>
       p
         (p
            (p
               (p
                  (p (p (p (p a b) (p a b)) (p (p a b) (p a b)))
                     (p (p (p a b) (p a b)) (p (p a b) (p a b))))
                  (p (p (p (p a b) (p a b)) (p (p a b) (p a b)))
                 =============SKIPPED LOTS OF LINES==========
                  (p (p (p (p a b) (p a b)) (p (p a b) (p a b)))
                     (p (p (p a b) (p a b)) (p (p a b) (p a b)))))))
     : nat -> nat -> nat
*)


Prelude> q f a b = f (f a b) (f a b)
Prelude> (q $ q $ q (+)) 1 1
256
Prelude> (q $ q $ q $ q (+)) 1 1
65536
Prelude> (q $ q $ q $ q $ q (+)) 1 1
4294967296
Prelude> (q $ q $ q $ q $ q $ q (+)) 1 1
18446744073709551616
Prelude> (q $q $ q $ q $ q $ q $ q (+)) 1 1
340282366920938463463374607431768211456
Prelude> (q $ q $ q $ q $ q $ q $ q $ q (+)) 1 1
115792089237316195423570985008687907853269984665640564039457584007913129639936
Prelude> (q $ q $ q $ q $ q $ q $ q $ q $ q (+)) 1 1
13407807929942597099574024998205846127479365820592393377723561443721764030073546976801874298166903427690031858186486050853753882811946569946433649006084096


Это пример терма, который растет экспоненциально при аппликативном порядке бета редукции (аксиома subst операционной семантики).

29 декабря 2016, 01:54

28 декабря 2016

Dee Mon journal

raytracing

Неожиданно отрендерил себе обои на рабочий стол рейтрейсером на хаскелле.

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

Свежий GHC и программы им сделанные забавно выгдядят в top'е: сразу съедают терабайт виртуальной памяти.

28 декабря 2016, 22:23

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-очередь уравнений, которая затем обрабатывается, пока она не станет пуста.

comment count unavailable comments

28 декабря 2016, 06:56

24 декабря 2016

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

Language Tiers

Tier 1. Динамические языки программирования. JavaScript, Python, Erlang, Ruby, Elixir, К. Часто включают в себя макросы. Родоначальник семейства — LISP. Не-типизированное лямбда исчисление. Особенности устройства современной вычислительной техники со всем этими кешами, конвейерами и т.п. создали благоприятные условия для того, чтобы интерпретаторы иногда делали вид, что обходят компилируемые языки. Существуют два основных способа повышения производительности — это векторизация (K, Julia*) (или параллельная обработка) и трассирующая JIT компиляция (Lua, JVM*, V8). До сих пор бытует миф что эти языки молотят данные не хуже С++ кода. Ничем не примечательный Erlang берет в Tier 1 категории не бенчмарками но уровнем и культурой инфрастктуры, не смотря на возраст эквивалентный возрасту говна мамонта. Если вы сцыте от LISP машин то прибежище вы найдете только в Erlang. Smalltalk как лиспойобская ВМ судя по признакам подходит, но продакшин это не переживет.

Эта ниша удобна для создания референсных трастед виртуальных машин. Есть такая область их применения, причем даже не обязательно чтобы они работали супер-быстро, главное чтобы их верификация (третьими лицами или теорем пруверами) проходила максимально безболезненно. Представьте себе верифицировать средний LISP с 4-5 индуктивными конструкторами и верифицировать типизированные JVM или Julia. Хотят пейперы по интернету, что Java вообще не поддается верификации также как и С++.

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

Верифицировать Erlang нет никакого желания и возможности, поэтому нужно было найти какой-то интерпретирующее ядро, которое А) можно полностью самому надизайнить создав предусловия для безболезненной верификации Б) сделать это на языке максимально близкому к MLTT с индуктивными и коиндуктивными типами. Семантика Rust вполне подходит в качестве более продвинутый ML конфигурации, фактически когда мы говорим Rust мы имеем ввиду современный LLVM уровня ML в который еще и обогатили MLton-новским region-based memory allocation статическим анализом. Такой себе OCaml только без gc.

Tier 2. System F языки. Минимальный индустриальный базис. Все современные языки так или иначе сравнялись с этой системой. Morte/OM примеры современных тайпчекеров-компиляторов-экстракторов чистых рекурсивных и корекурсивных программ. Эта система достаточно мощная чтобы на ней составить трамплин для вычисления функторов локальных ДЗК. Этому исследовательскому проекту была посвящена суть категорных кодировок. Выражая эту идею простыми словами — создать вычислитель лимитов (обычный интерпретатор на свободных монадах), с помощью которого можно построить индуктивные и коиндуктивные типы по сигнатурам их алгебр. Достаточно мощная и новая идея к сожалению не была воспринята общественностью. Верифицированный System F компилятор не думаю что возможен, хотя ходили слухи о метациркулярности в Fw. Программы доказываются по другому, просто экспортируются в Coq/Agda и там для проимпорченых термов строятся общие высказывания. Так делались все прувед стеки: seL4, VST; и это пример того как делать не нужно.

Поэтому, чтобы минимизировать этот импорт к нулю нужно просто совместить Tier 2 и Tier 3 в один язык. Базовая библиотека таким образом распадается на части экстракт-имплементация (System F) и теоремы-спецификации (MLTT). Так произошло разделение OM и EXE. OM -- это программы ядра которые прошивается в трастед окружение: FPGA (Tier 0), или Tier 1. А EXE это язык на котором эти программы были сформулированы вместе с их спецификациями.

OM поддерживает сейчас Erlang бекенд, но Erlang -- это трастед интепретатор, нужен какой-то интерпретатор, который можно было поместить в узкие рамки (как спецификацию так и имплментацию), которые потом портировав на Coq можно было бы превратить в доказанную вычислительную среду уровня Tier 1. Такой кандидат — новая платформа на языке О. Ближайшие пол года год я буду посвящен исключительно языку О и его интерпретатору.

Tier 3. Теорем пруверы способные схавать HoTT, т.е. с бесконечной предикативной иерархией универсумов. Основное предназначение этого высшего Tier 3 — это доказательство свойств программ написанных на Tier 2. Процесс экстракта начинается с этого уровня и здесь тоже хочется чтобы в стеке небыло никаких импортов. Irdis, Agda, Coq, Lean, есть куча всего создать конкурентно-способный прувер это дело техники. Наработки Groupoid Infinity хоть и скромные но убедительные.

Таким образом в непрерывном стеке я выделяю только три языка: 1) виртуальная машина и нетипизированное лямбда исчисление; 2) System F промышленная базовая библиотека 3) язык доказывающий базовую библиотеку в продолжении синтаксиса языка уровня 2.

_______________
* Julia и JVM типизированные

24 декабря 2016, 02:16

21 декабря 2016

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

О-CPS Интерпретатор

Немного о том, как я написал парсер языка О. Хотя netch80 и ругает у себя в посте язык К справедливо, хочу попытаться зафиксировать основные правила синтаксиса и привнести некоторый порядок в язык, предоставив формальную нотацию для LR парсеров. Имплементация прототипа делалась на lalrpop — это нетабличный однопроходной LR парсер который поставляется с голимым регэксп токенайзером. Токенайзер вместо регекспов хочется кастомный на NOM, но руки не доходят.

Существует три вида скобочек: [], (), {} — множества, списки и лямбды. Другими словами это M-expressions, S-expressions и Лямбда-калкулус соответственно (который в К можно представить как Pi-calculus, так как K-Cell содержит вектор, а значит все параметры — это стримы, и если трактовать срабатывание функции на появление нового элемента в любом стриме-параметре, то это уже будет Пи-калкулус и CHR, штука которая полезна не только для моделирования самобалансирующего скедулера но для потокового бизнес роутинга).

> ()
> []
> {}

Ok(Nil)
Ok(Nil)
Ok(Lambda(Nil, Nil))


Эти Nil могут либо схлопываться, либо рости при встраиваниях. Например [[]] и (()) не изменяются при встраиваниях, а {{}} растет:

> (())
> [[]]
> {{}}

Ok(Nil)
Ok(Nil)
Ok(Lambda(Nil, Lambda(Nil, Nil)))


Изменяя способ расстановки скобочек можно догадаться какие основные правила создания выражений:

> ((()))
> ()()()
> [][]()
> {}{}{}

Ok(Nil)
Ok(Call(Nil, Call(Nil, Nil)))
Ok(Call(Nil, Call(Nil, Nil)))
Ok(Call(Lambda(Nil, Nil), Call(Lambda(Nil, Nil), Lambda(Nil, Nil))))


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

>  1 2 3
> (1 2 3)
> [1 2 3]
> {1 2 3}
> (1(2(3(4))))
> [1[2[3[4]]]]
> [[[[1]2]3]4]
> {1{2{3{4}}}}

Ok(Call(Number(1), Call(Number(2), Number(3))))
Ok(Call(Number(1), Call(Number(2), Number(3))))
Ok(Call(Number(1), Call(Number(2), Number(3))))
Ok(Lambda(Nil, Call(Number(1), Call(Number(2), Number(3)))))
Ok(Call(Number(1), Call(Number(2), Call(Number(3), Number(4)))))
Ok(Call(Number(1), Call(Number(2), Call(Number(3), Number(4)))))
Ok(Call(Call(Call(Number(1), Number(2)), Number(3)), Number(4)))
Ok(Lambda(Nil, Call(Number(1), Lambda(Nil, Call(Number(2), Lambda(Nil, Call(Number(3), Lambda(Nil, Number(4)))))))))


Если множество в своем списке-носителе содержит присваивания к именам то такой множество трактуется как словарь, если список множества — это просто имена — то это бинд параметр функции {[x;y;z]...}, если параметр множества если функция без параметров бинда, то x,y,z трактуются как имена контекста по умолчанию. Если члены списка словаря просто выражения, то это множество носитель параметров. Множества называются M-expressions.

> [1;2]
> function[1;2]
> [a:1;b:2]
> {[x;y]x*y+x}

Ok(Dict(Cons(Number(1), Number(2))))
Ok(Call(Name("function"), Dict(Cons(Number(1), Number(2)))))
Ok(Dict(Cons(Adverb(Assign, Name("a"), Number(1)), Adverb(Assign, Name("b"), Number(2)))))
Ok(Lambda(Cons(Name("x"), Name("y")), Verb(Times, Name("x"), Verb(Plus, Name("y"), Name("x")))))


Списки тоже можно конкатенейтить через Semicolon, вообще у Semicolon максимальный приоритет и она разделяет все экспрешины. Это в сущности одни и те же списки, только данные обрамленные конструкторами, а колл-чейн более абстрактный, и он тоже конвертируется с список но в общем случае может состоять из любых K-Cell.

> (1;2;3;4)
> [1;2;3;4]
>  1 2 3 4
> `a`b`c`d

Ok(List(Cons(Number(1), Cons(Number(2), Cons(Number(3), Number(4))))))
Ok(Dict(Cons(Number(1), Cons(Number(2), Cons(Number(3), Number(4))))))
     Ok(Call(Number(1), Call(Number(2), Call(Number(3), Number(4)))))
     Ok(Call(Symbol("a"), Call(Symbol("b"), Call(Symbol("c"), Symbol("d")))))


У меня получилась BNF нотация на 13 правил. Что скажете? Можно короче, красивее?

List:      AST = { "(" ")" => AST::Nil, "(" <l:exprlist> ")" => list(l), };
Dict:      AST = { "[" "]" => AST::Nil, "[" <l:exprlist> "]" => dict(l), };

Lambda:    AST = { "{" <m:exprlist> "}"                      => fun(AST::Nil,m),
                   "{[" <c:namelist> "]" <m:exprlist> "}"    => fun(c,m),
                   "{" "}"                                   => fun(AST::Nil,AST::Nil)};

Call:      AST = { <c:noun> <a:callcont>                     => call(c,a), };
NameList:  AST = { Name, <o:name> <m:namecont>               => cons(o,m), };
ExprList:  AST = { ExprCont, Expr, <o:expr> <m:exprcont>     => cons(o,m), };

CallCont:  AST = { Noun, <m:call>                            => m };
NameCont:  AST = { ";" => AST::Nil, ";" <m:namelist>         => m };
ExprCont:  AST = { ";" => AST::Nil, ";" <m:exprlist>         => m };

Noun:      AST = { Name, Number, Hexlit, Bool, Symbol, List, Dict, Sequence, Lambda, Ioverb };
Expr:      AST = { Noun, Call, Verbs, Adverbs, };

Verbs:     AST = {           <v:verb>               => verb(v,AST::Nil,AST::Nil),
                             <v:verb>     <r:expr>  => verb(v,AST::Nil,r),
                   <l:call>  <v:verb>     <r:expr>  => verb(v,l,r),
                   <l:noun>  <v:verb>     <r:expr>  => verb(v,l,r), };

Adverbs:   AST = {           <a:adverb>             => adverb(a,AST::Nil,AST::Nil),
                             <a:adverb>   <e:expr>  => adverb(a,AST::Nil,e),
                   <l:call>  <a:adverb>   <r:expr>  => adverb(a,l,r),
                   <l:noun>  <a:adverb>   <r:expr>  => adverb(a,l,r), };

Терминалы думаю написать на NOM попробовать, чтобы быстрее парсалось.
Number:    AST = { <n:r"\d+"> => AST::Number(u64::from_str(n).unwrap()), };
Hexlit:    AST = { <h:r"0x[a-zA-Z\d]+"> => AST::Number(u64::from_str_radix(&h[2..], 16).unwrap()), };
Bool:      AST = { <b:r"[01]+b"> => AST::Number(u64::from_str_radix(&b[0..b.len()-1], 2).unwrap()), };
Name:      AST = { <n:r"[a-zA-Z][-a-zA-Z\d]*"> => AST::Name(String::from(n)), };
Symbol:    AST = { <s:r"`([a-z][a-z0-9]*)?"> => AST::Symbol(String::from(&s[1..s.len()])), };
Adverb: Adverb = { <a:r"[\x27:\x5C\x2F]:?"> => Adverb::from_str(a).unwrap(), };
Verb:     Verb = { <v:r"[+\x2D*$%!&|<>=~,^#_?@.]"> => Verb::from_str(v).unwrap(), };
Ioverb:    AST = { <i:r"\d+:"> => AST::Ioverb(String::from(i),Box::new(AST::Nil)), };
Sequence:  AST = { <s:r"\x22(\\.|[^\x5C\x22])*\x22"> => AST::Sequence(String::from(&s[1..s.len()-1])), };



Этот парсер парсает все исходники К и Q которые мне попадались на глаза, включая диалекты типа Kona (K4) и oK.js (K5). Это около 128КБ, включая саму имплементацию Q, каталоги примеров других диалектов и корпоративный продакшиновский К код. Принципиальной и абсолютной совестимости я не хочу, но максимальное покрытие диалектов и высокая портируемость не помешает.

21 декабря 2016, 11:54

beroal

ассоциативное мышление вредит при верификации

Недавно я писал о ассоциативном мышлении. Всё это выглядело как философия. Философы любят высасывать проблемы из пальца. Но ассоциативное мышление — это реальная проблема. Следующий пример демонстрирует это.

В одном курсе по программированию есть следующая задача. «Вычислить, пусто ли A∪B. Известно, пусто ли A и пусто ли B». (Рассматриваются подмножества , но это не существенно здесь.) Решаем с помощью теоремы A∪B⊆∅ ↔ A⊆∅∧B⊆∅ (теорема 0). Другая похожая задача. «Вычислить, пусто ли A∩B. Известно, пусто ли A и пусто ли B». Вот как решил её один студент, используя ассоциативное мышление. (Конечно, я предполагаю, что происходило в его голове. Я не телепат.) « двойственно . Следовательно, надо использовать двойственную логическую связку. Получается A∩B⊆∅ ↔ A⊆∅∨B⊆∅». Кратко, элегантно, интуитивно понятно. К сожалению, ложно.

Чего не хватает? Разумеется, доказательства. Попробуем доказать. Допустим, A∩B⊆∅. Раскрыли определения, ∀a a∈A∧a∈B → ⊥. Надо доказать, что A пусто или B пусто. Мы могли бы использовать a∈A∧a∈B → ⊥, если бы каждый элемент B также принадлежал A. Тогда бы мы доказали, что B пусто. Это наводит на контрпример. Найдём населённое B такое, что каждый его элемент не принадлежит A. Например, A={1}, B={2}. A∩B⊆∅ и не A⊆∅∨B⊆∅.

Кстати, интуиция помогает найти теорему, двойственную теореме 0. Теорема 0 соответствует (ассоциирована) сложению морфизмов. Теорема C⊆A∩B ↔ C⊆A∧C⊆B соответствует умножению морфизмов. Двойственность требует повернуть в противоположную сторону. Конечно, это «рассуждение» не заменяет логического доказательства.

21 декабря 2016, 06:09

18 декабря 2016

beroal

Пролог и фанатизм в информатике

Присказка. Однажды я захотел создать файл в формате Low Level Virtual Machine Intermediate Representation (LLVM IR). В ходе работы выяснилось, что официальная документация неясна, неполна и некорректна. Не то, чтобы совсем бесполезна, но многие вещи пришлось выяснять с помощью экспериментов и чтения исходного кода парсера на C++, который я не люблю. Родилась идея описать этот формат формально, чтобы потом уже обращаться к формальному описанию, а не блуждать каждый раз в плохой официальной документации. Я думал, что это не займёт много времени. I had no idea. ☺

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

Быстро стало ясно, что класс контекстно-свободных грамматик слишком маломощный, чтобы описать LLVM IR. Поэтому я закопался в более мощные. Многие такие грамматики строятся на базе контекстно-свободных, то есть это контекстно-свободная грамматика с добавлением текста на некотором япе. Из них я выбрал definite clause grammars. В них в качестве япа взят Пролог. Мне понравилось то, что контекстно-свободная грамматика может быть транслирована в тот же Пролог, то есть мы имеем как бы общую платформу. Причём результат трансляции (отношение, предикат) будет работать как парсер и как принтер. (Попутно я узнал о идее parsing as deduction. Это значит, что приёмы парсинга можно обобщать в Пролог. Например, дедукция Эрли.) (Кстати, в вузе мы учили Пролог. Конечно, это мне мало помогло. Можете представить, какое это было изучение, учитывая, что мы не учили формальную логику. Общее впечатление, которое осталось, выразил один студент фразой «кумарной язык».)

По ходу изучения мне стала ясна и теоретическая польза от Пролога. В Прологе отношения заменяют функции. (Здесь я не говорю о функциях в смысле теории множеств. В теории множеств функция есть функциональное (двойственно-биективное) 2-местное отношение, то есть функции есть частный случай отношений. Здесь я говорю о функциях в смысле теории типов. В теории типов функция есть алгоритм.) Отношения соответствуют спецификациям, функции соответствуют алгоритмам. Отношение описывает, ну, отношение между результатом и аргументом и обычно не описывает, как вычислить результат. (Иногда отношение описывает, как вычислить аргумент, зная результат. Например, отношение «возвести в квадрат» двойственно отношению «извлечь квадратный корень». Отношение «извлечь квадратный корень» описывает, как вычислить аргумент: возвести в квадрат, разумеется. Это очень просто, но это мало помогает, ведь нужен всё-таки квадратный корень.) Реализация Пролога — это попытка автоматически вывести алгоритм из спецификации. Поэтому программы на Прологе частенько не останавливаются, то есть алгоритм как бы выведен, но он не годный. Чудес не бывает.

Мораль. «Я знаю, что я ничего не знаю». Раньше я считал Пролог маргинальным направлением информатики. Я игнорировал его, потому что был увлечён теорией типов. Пролог оказался полезным с практической и теоретической сторон. Более того, мне нужен не просто стандартный Пролог, но и надстройки к нему, и более совершенная реализация. То есть фанатичное следование некоторой идее закрывает пути развития. Я вижу такую фанатичность у других людей. В отношении теории типов. В отношении теории категорий. Везде ищут категории. Вплоть до того, что моноиды и предпорядки надо преподавать как частные случаи категорий. Не абсурд ли? В результате наивные люди учат теорию категорий, не выучив структуры в смысле Бурбаки, учат на примерах из программирования. То есть учат частный случай. Значит, потом придётся переучиваться, учить теорию категорий заново. Я считаю, что лучше выучить 1 раз хорошо, чем 10 раз плохо.

18 декабря 2016, 07:03

16 декабря 2016

nponeccop

Фейсбучик пилит GHC

http://simonmar.github.io/posts/2016-12-08-Haskell-in-the-datacentre.html

Похоже, что появился второй серьёзный проект, использующий GHC :) Первый - это сам GHC.

Xmonad, Darcs, Pandoc и Leksah не считаются, потому что им насрать на перфоманс.

16 декабря 2016, 04:23

13 декабря 2016

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

Замена Heap на преалоцированный Vec + Lifetime переменные

TL;DR: Такой рефакторинг привел всех в состояние Х. С 7мкс до 200нс (буст в 35 раз). В вопросе скорости создания контекстов мы выебали Kx Systems, Erlang и Python. На этом можно поставить пока точку.

Lang    avg ns of 1M calls
------- ------------------
Rust    0
Java    3
O-CPS   217
Erlang  10699/1806/436/9
Python  537
K       899
LuaJIT  33856


Мы поменяли в нашем интерпретаторе все Box Heap аллокации на преалоцированный ручной хип с вектором указателей + лайфтайм по всему коду. Т.е. даже Box остались исключительно как бинды. Получился Zero-Copy Interpreter работающий исключительно с указателями на ячейки байт-кода виртуальной машины, которые в сущности сериализированные элементы AST дерева. Опуская детали реализации приведу только типы деревьев:

Старое дерево с Heap указателями
pub enum Cont {
    Expressions(AST, Tape),
    Lambda(Code, AST, AST, Tape),
    Assign(AST, Tape),
    Cond(AST, AST, Tape),
    Func(AST, AST, Tape),
    Call(AST, Tape),
    Verb(Verb, AST, u8, Tape),
    Adverb(Adverb, AST, Tape),
    Return,
}

pub struct Tape {
    env: Rc<RefCell<Environment>>,
    cont: Box<cont>,
}


Новое дерево только с абстрактными ссылками и переменными времени жизни
pub enum Cont<'a> {
    Expressions(&'a AST<'ast>, &'a Cont<'a>),
    Lambda(Code, &'a AST<'a>, &'a AST<'a>, &'a Cont<'a>),
    Assign(&'a AST<'ast>, &'ast Cont<'ast>),
    Cond(&'a AST<'a>, &'a AST<'a>, &'a Cont<'a>),
    Func(&'a AST<'a>, &'a AST<'a>, &'a Cont<'a>),
    Call(&'a AST<'a>, &'a Cont<'a>),
    Verb(Verb, &'a AST<'a>, u8, &'a Cont<'a>),
    Adverb(Adverb, &'a AST<'a>, &'a Cont<'a>),
    Return,
}

pub struct Interpreter<'a> {
    arena: Arena<'a>,
    env: Environment<'a>,
}


Environment в наивном прототипе представлен в виде HashMap, который как известно неподходит там где нужна скорость, зато понятно — у каждой кложи своя хеш-таблица контекст. Другое дело что для этого всего хватит и стека фреймов. Вообще говоря контексты функций — это и есть стек, а перенесен он в Heap для того, чтобы можно было писать не валящиеся бесконечные циклы, что называется tailcall или CPS интерпретаторами.

Написать прототип на расте оказалось очень просто. Бездумный ленивый CPS интерпретатор, который в хипе держит свой стек в виде HashMap изначально является не хуже чем LuaJIT в вопросе создания контекстов, а переписанный нормально в zero-copy версию с лайфтаймами с стек-фреймами в преалоцированном векторе обгоняет даже лидеров индустрии.

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

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

13 декабря 2016, 23:44

Lispnik

Тряхнём стариной Мандельбротом

Решил я вспомнить молодость — нарисовать множество Мандельброта, тем более что с тех пор мощность компьютеров значительно выросла. Самую первую программу для рассчёта множества Мандельброта я написал ещё в 11 классе, используя Borland C++ (для Windows 3.11, стоявшей в компьютерном классе).

Чтобы было веселей, я решил написать параллельную программу на C с использованием MPI. Нужно же использовать многоядерные процессоры...

Одновременно я сделал версию, которая использует тип complex, она оказалось в два раза медленнее варианта с использованием double. После микрооптимизаций стала отставать лишь где-то на четверть, а то и меньше (замеров не сохранилось, к сожалению).

Первая версия использовала примитивную раскраску, основанную на скорости убегания. Картинка 5120x10240 40960x20480 считалась в 8 потоков 6 часов на 8-ядерном Intel® Core i7 920 (2.67GHz).

Потом я решил сделать улучшенную раскраску, и стал использовать вариант с complex. Новый вариант (34Мб, не пытайтесь открывать в браузере!) считался в тех условиях 10 часов.

И тут я решил сделать вариант на Common Lisp... И сделал вариант на C без MPI. И оказывается, вариант на Common Lisp (SBCL 1.0.55) работает на четверть быстрее, чем вариант на C (gcc 4.4.5)! Запускал на AMD Phenom 9650 Quad-Core (2.3MHz), картинка 1024x512. (Исходники).

> (time (calculate))                                                     
Evaluation took:
  33.333 seconds of real time
  33.317935 seconds of total run time (32.625041 user, 0.692894 system)
  99.96% CPU
  76,832,689,149 processor cycles                                               
  1 page fault
  393,232 bytes consed

$ time ./mmb
real    0m43.621s
user    0m42.694s
sys     0m0.896s

Однако справедливости ради нужно упомянуть, что оба варианта дают немного разные картинки — в 13 пикселях на картинке 1024x512 разница значений равна 1. Ошибки округления?

Upd 13 декабря 2016: в комментариях указывают, что для справедливого результата надо сраавнивать с -O3 -ffast-math. На С c -O3 считается на текущем железе за 16.7 секунд, с -O3 -ffast-math за 10 секунд, на SBCL — 14 секунд. Однако разнятся теперь 87 пикселей, а не 13, как раньше.

13 декабря 2016, 09:57

09 декабря 2016

08 декабря 2016

Scala@livejournal.com

ru_scala @ 2016-12-08T10:11:00

Допустим, у нас есть матрица представленная в виде Vector[Vector[Int] и функция def foo(i: Int, j: Int, cell: Int): Int, у которой первые два аргумента это индексы, а третий -- элемент матрицы.

Я хочу применить foo ко всем элементам:
type Board = Vector[Vector[Int]]
def foo(i: Int, j: Int, cell: Int): Int = ???
val board = Vector(Vector(0, 0, 0), Vector(0, 1, 0), Vector(0, 0, 0))
board.zipWithIndex map { case (row, i) => row.zipWithIndex map { case (cell, j) => foo(i, j, cell) } }

А можно это написать попроще и без этих вложенных zipWithIndex map ?

написал Michael 08 декабря 2016, 08:11

06 декабря 2016

Scala@livejournal.com

Игра Жизнь для разреженных матриц

Возник вопрос, как написать решение для случая, когда живых клеток намного меньше неживых. Тогда игровое поле логично представить в виде множества координат живых клеток -- Set[(Int, Int)]. Как бы вы решили эту задачу ? У меня пока есть только одна идея: для каждой из живых клеток сгенерить её соседей и дальше фильтровать выживших.

написал Michael 06 декабря 2016, 13:26

02 декабря 2016

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

CPS Interpreter in Rust Language

Итак, в прошлых постах мы построили парсер диалектов K, а именно: K3, K4, K5 и Q. Теперь пришла пора написать CPS интерпретатор, такой который смог бы крутить бесконечные циклы лямбдочки быстрее эрланга.

Интерпретатор мы будем строить используя следующий базис понятий функционального программирования: Вложенные контексты, Отложенные вычисления и Лямбда исчисление.

Вложенные контексты — это наш Environment или Dictionary, когда мы создаем дочерний контекст, например при аппликации лямбды, мы линкуем дочерний контекст с родителькому, поэтому в имплментациях акссесоров у нас будет рекурсивный Find — он не только должен вернуть значение по ключу, но и вернуть контекст в котором он это нашел в цепочке контекстов. Значения — это AST (чтобы не плодить много типов, мы просто некоторые конструкторы AST объявляем боксами Integer, String, Boolean, Float, поэтому в процессе работы интерпретатора он вычислит и положит результат в тот же тип AST, в байткоде виртуальной машины — это может выглядеть как просто состояние регистров и инструкции для загрузки или выгрузки констант), а Контексты — это счетчики ссылок на ячейки (AST, Rc<RefCell<Environment>>). Если сказать о контекстах высоко — то вложенные контексты соответствуют Сигма типу и являются свидетелями контекстуальной полноты.
pub struct Environment {
    parent: Option<Rc<RefCell<Environment>>>,
    values: HashMap<String, AST>,
}

impl Environment {
    pub fn new_root() -> Result<Rc<RefCell<Environment>>, Error> {
        let mut env = Environment {
            parent: None,
            values: HashMap::new(),
        };
        Ok(Rc::new(RefCell::new(env)))
    }
    pub fn new_child(parent: Rc<RefCell<Environment>>) -> Rc<RefCell<Environment>> {
        let env = Environment {
            parent: Some(parent),
            values: HashMap::new(),
        };
        Rc::new(RefCell::new(env))
    }
    pub fn find(&self, key: &String) -> Option<(AST, Rc<RefCell<Environment>>)> {
        match self.values.get(key) {
            Some(val) => Some((val.clone(), Rc::new(RefCell::new(self.clone())))),
            None => {
                match self.parent {
                    Some(ref parent) => parent.borrow().find(key),
                    None => None,
                }
            }
        }
    }

Интерпретатор хранит рутовый контекст.
pub struct Interpreter {
    root: Rc<RefCell<Environment>>,
}

Отложенные вычисления — используются нами для проскакивания цепочки AST, и форсинг когда достигли определенного события. Обычно во всех базовых функциональных библиотеках (типа PureScript и Elm) называется Lazy Type. У нас Lazy параметризирован контекстами и протоколом выполнения — Environment и Continuation. Вообще тут мистики никакой нет. Если посмотреть на любое выражение — то половина времени тратится на Defer и приблизительно половина на Force, причем все дефер обычно заканчиваются сразу парными форсами. Это сделано для того, чтобы вечные циклы крутились в нулевом стеке. Что еще можно сказать про этот интерпретатор? Я лично хотел добиться от этого интерпретатора идиоматичности, чтобы его понимал и прокурор и милиция. Я намеренно в посте исключил имплементации обычных выражений + и * чтобы показать суть интерпретатора. Так как многие знают что этого уже достаточно для моделирование вычислительных вселенных. По крайней мере такты интерпретатора уже можно считать. Если бы этот интерпретатор был клаудом, он бы чарджил и билил только форсы.
pub enum Trampoline {
    Defer(AST, Rc<RefCell<Environment>>, Continuation),
    Force(AST, Continuation),
    Return(AST),
}

Протокол исполнения: Лямбда исчисление + синтаксические расширения — ядро интерпретатора (Assign, Cond, Lambda, Call) которое создает контексты, делает по ним лукапы и биндит переменные при аппликациях. У нас не аппликативно-божественный (на subst, как в OM/EXE), а нормально-колхозный порядок бета редукции (ALGOL68, LUA, K), зато если поместиться в 32К L1 то можно сорвать большой куш, как это делают K и LuaJIT, остальные сосут с call-by-name причмокивая. Тут хочется быть максимально расширяемым, чтобы новые конструкторы AST ложились на этот протокол отложенных вычислений. Особой мистики тут не нужно, можно считать — это управляющим протоколом, вся магия будет происходить в векторном DSL, там целые блоки будут транслироваться в Lazy структуры итераторы Rust и выполняться в интерпретаторе как единые инструкции, для которых определен AST конструктор. Лямбда исчисление является свидетелем функциоальной полноты нашей системы. Если добавить сюда Пи тип, мы сможем превратить интерпретатор в теорем прувер? :-)
pub enum Continuation {
    EvaluateExpressions(AST, Rc<RefCell<Environment>>, Box<Continuation>),
    EvaluateAssign(AST, Rc<RefCell<Environment>>, Box<Continuation>),
    EvaluateCond(AST, AST, Rc<RefCell<Environment>>, Box<Continuation>),
    EvaluateFunc(AST, AST, Rc<RefCell<Environment>>, Box<Continuation>),
    EvaluateVerb(AST, AST, Rc<RefCell<Environment>>, Box<Continuation>),
    EvaluateAdverb(AST, AST, Rc<RefCell<Environment>>, Box<Continuation>),
    Return,
}

В CPS интерпретаторе самое главное — это цикл, который крутит AST дерево и создает отложенные вычисление, периодически форся вычисления. Обычно это проистодит в стиле Defer-Force, но все зависит от программ.
fn process(exprs: AST, env: Rc<RefCell<Environment>>) -> Result<AST,Error> {
    if exprs.len() == 0 {
        return Ok(AST::Nil);
    }
    let mut b = try!(evaluate_expressions(exprs, env, Box::new(Continuation::Return)));
    loop {
        match b {
            Trampoline::Defer(a, e, k) => b = try!(handle_defer(a, e, k)),
            Trampoline::Force(x, k) => b = try!(k.run(x)),
            Trampoline::Return(a) => return Ok(a),
        }
    }
}

handle_defer выглядит примерно так:
fn handle_defer(a: AST,
                env: Rc<RefCell<Environment>>,
                k: Continuation)
                -> Result<Trampoline,Error> {
    match a {
        AST::Assign(box name, box body) => {
            Ok(Trampoline::Force(body,
                                 Continuation::Assign(name, env, Box::new(k))))
        }
        AST::Call(box callee, box args) => evaluate_function(callee, env, args, k),
        AST::Name(name) => {
            match lookup(name, env) {
                Ok(v) => k.run(v),
                Err(x) => Err(x),
            }
        }
        x => k.run(x),
    }
}

evaluate_function разворачивает Name и деферит лямбду.
fn evaluate_function(fun: AST,
                     env: Rc<RefCell<Environment>>,
                     args: AST,
                     k: Continuation)
                     -> Result<Trampoline, Error> {
    match fun {
        AST::Lambda(box names, box body) => {
            Ok(Trampoline::Force(body, Continuation::Func(names, args, env, Box::new(k))))
        }
        AST::Name(s) => {
            match env.borrow().find(&s) {
                Some((v, x)) => evaluate_function(v, x, args, k),
                None => {
                    Err(Error::EvalError {
                        desc: "Function Name in all Contexts".to_string(),
                        ast: AST::Name(s),
                    })
                }
            }
        }
        x => {
            Err(Error::EvalError {
                desc: "Call Error".to_string(),
                ast: x,
            })
        }
    }
}

evaluate_expressions создает один отложеный такт интерпретатора, типа R(1).
fn evaluate_expressions(exprs: AST,
                        env: Rc<RefCell<Environment>>,
                        k: Box<Continuation>)
                        -> Result<Trampoline,Error> {
    match exprs.shift() {
        Some((car, cdr)) => {
            Ok(Trampoline::Defer(car,
                                 env.clone(),
                                 Continuation::EvaluateExpressions(cdr, env, k)))
        }
        None => {
            Err(Error::EvalError {
                desc: "Empty list".to_string(),
                ast: AST::Nil,
            })
        }
    }
}

Обработчики Лямбда исчисления простые, эвалуатор ложит и кладет в контексты, сравниватель сранивает, биндинг переменной биндит переменную.
impl Continuation {
    pub fn run(self, val: AST) -> Result<Trampoline,Error> {
        match self {
            Continuation::EvaluateExpressions(rest, env, k) => {
                if rest.is_cons() || !rest.is_empty() {
                    evaluate_expressions(rest, env, k)
                } else {
                    Ok(Trampoline::Force(val, *k))
                }
            }
            Continuation::EvaluateFunc(names, args, env, k) => {
                let local_env = Environment::new_child(env);
                for (name, value) in names.into_iter().zip(args.into_iter()) {
                    try!(local_env.borrow_mut().define(name.to_string(), value));
                }
                evaluate_expressions(val, local_env, k)
            }
            Continuation::EvaluateCond(if_expr, else_expr, env, k) => {
                match val {
                    AST::Bool(false) => Ok(Trampoline::Defer(else_expr, env, *k)),
                    _ => Ok(Trampoline::Defer(if_expr, env, *k)),
                }
            }
            Continuation::EvaluateAssign(name, env, k) => {
                match name {
                    AST::Name(ref s) => {
                        try!(env.borrow_mut().define(s.to_string(), val));
                        Ok(Trampoline::Force(AST::Nil, *k))
                    }
                    x => {
                        Err(Error::EvalError {
                            desc: "Can assign only to var".to_string(),
                            ast: x,
                        })
                    }

                }
            }
            _ => Ok(Trampoline::Return(val)),
        }
    }
}

Вот и весь интерпретатор (кроме правил для Verb и Adverb, там умножение и вычитание необходимые для факториала и Cond вообще говоря тоже, который в K языке повешен на Cast). Традиционно бенчмарки против Erlang написанном на С.
1> Fac = fun Factorial(X) -> case X of 1 -> 1; _ -> X * Factorial(X-1) end end.
#fun<1131414>
2> Fac(5).
120
3> timer:tc(fun() -> Fac(5) end).
{91,120}

Интерпретатор написанном на Rust:
"fac:{[x]$[x=1;1;x*fac[x-1]]};fac[5]"
test tests::fac ... bench:      16,850 ns/iter (+/- 1,169)

91 микросекунд (Erlang) против 17 микросекунд (O-CPS INTERPRETER)

02 декабря 2016, 23:49

29 ноября 2016

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

Угадайте язык по BNF :-)

Я сейчас пишу один язычок, у нас на самом деле в компании где я сейчас работаю, трое человек пишет этот язык. Еще один сотрудник недавно критиковал этот язык в ЖЖ, по делу конечно.

29 ноября 2016, 21:44

Векторный DSL

Надо как-то назвать язык. Назову его О. Задачи языка:

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

— Выстувать в роли векторного DSL для K Cell. Каждая K Cell — это по сути вектор или растовский итератор, поддерживающий все его интерфейсы и поддающийся векторизации. Есть также библиотеки распаралеливания этих итераторов.

Сейчас язык парсает основные диалекты K, Q, oK.js, а также Kona. В К мире не приянято писать декларативные парсеры, так как строятся ручные интерпетаторы с встроеным токенайзером. Но поскольку мы воспринимам К программу как DSL к итераторам, нам нужно все AST сразу для ленивого выполнения, поэтому так или иначе строить его нужно. Ну и еще листы в векторы сворачивать, все это тоже можно эффективно делать на этапе парсинга.

Покажу на примере, например нам нужно вычислить скалярное произведение двух векторов:
+/{x*y}[(1;3;4;5;6);(2;6;2;1;3)]

А теперь представим вместо очередей Ioverb устройства, индексы кольцевых буферов в стиле как мы идектируем потоки ввода выводы (0: и 1:) — "1212:" или "3600:".
+/{x*y}[1212:;3600:]

Это транформируется в растовский:
vec1.iter()
    .zip(vec2.iter())
    .map(|(i, j)| i * j)
    .sum()

И в итоге векторизируется LLVM в:
.LBB0_7:
	testq	%r8, %r8
	je	.LBB0_9
	movdqu	16(%rdx,%rax,4), %xmm2
	movdqu	16(%rdi,%rax,4), %xmm3
	pshufd	$245, %xmm2, %xmm4
	pmuludq	%xmm3, %xmm2
	pshufd	$232, %xmm2, %xmm2
	pshufd	$245, %xmm3, %xmm3
	pmuludq	%xmm4, %xmm3
	pshufd	$232, %xmm3, %xmm3
	punpckldq	%xmm3, %xmm2
	paddd	%xmm2, %xmm1
	movdqu	(%rdx,%rax,4), %xmm2
	movdqu	(%rdi,%rax,4), %xmm3
	pshufd	$245, %xmm2, %xmm4
	pmuludq	%xmm3, %xmm2
	pshufd	$232, %xmm2, %xmm2
	pshufd	$245, %xmm3, %xmm3
	pmuludq	%xmm4, %xmm3
	pshufd	$232, %xmm3, %xmm3
	punpckldq	%xmm3, %xmm2
	paddd	%xmm2, %xmm0

29 ноября 2016, 21:43

David Sorokins WebLog

Сетевое моделирование с Айвикой

Давно присматриваюсь к сетевому моделированию (англ. network simulation). Нахожу, что многое можно моделировать с помощью моей Айвики уже сейчас, в том числе, моделировать распределенно на кластере или параллельно на суперкомпьютере.

Основная идея такая. Обычно говорят о портах - источниках данных. В Айвике источники могут быть как активными, так и пассивными. Активный источник сам проталкивает данные дальше для обработки. Это у меня тип Signal a (или Signal m a в обобщенной версии). Тогда каналом будет просто преобразование одного сигнала в другой. Модуль будет функцией, отображающей входные сигналы на выходные.

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

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

Пассивные источники данных у меня в Айвике представлены потоками Stream a (или Stream m a в обобщенной версии). Их нужно запрашивать, чтобы вытянуть из них данные. Их можно распараллеливать для обработки, а потом снова сливать в один поток.

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

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

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

p.p1 {margin: 0.0px 0.0px 0.0px 0.0px; font: 12.0px Helvetica} p.p2 {margin: 0.0px 0.0px 0.0px 0.0px; font: 12.0px Helvetica; min-height: 14.0px}
В общем, у меня есть достаточно общий аппарат, который может быть применен к широкому классу задач на мой взгляд. Более того, используя модуль aivika-distributed, такие задачи можно обсчитывать распределенно на кластере или параллельно в случае необходимости. Как раз на днях значительно улучшил этот модуль.

написал dsorokin (noreply@blogger.com) 29 ноября 2016, 20:25

Распределенное моделирование c Айвикой

Обновил версию aivika-distributed, которую можно использовать для распределенного и параллельного моделирования. Реализована оптимистичная стратегия по методу Time Warp. В этой версии значительно улучшена синхронизация глобального времени. Используется алгоритм Самади. В общем, если соединения между узлами достаточно надежные, то распределенная имитация должна вполне хорошо работать.

Чтобы использовать эту версию, достаточно вооружиться документацией PDF по базовой версии Айвики. Здесь все то же самое, т.е. события, процессы, ресурсы, сигналы, потоки транзактов, все это применимо и к распределенной версии. Только типы будут выглядеть по другому. Там, где был Event a, станет Event DIO a и т.д.  Последний Event - это фактически монадный трансформер, но я решил не добавлять к его названию букву T, как это обычно делают, а сохранить все названия из базовой версии. Тому были причины.

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

Собственно, все! В следующем сообщении напишу, как это можно применить к сетевому моделированию (англ. network simulation)
p.p1 {margin: 0.0px 0.0px 0.0px 0.0px; font: 12.0px Helvetica} p.p2 {margin: 0.0px 0.0px 0.0px 0.0px; font: 12.0px Helvetica; min-height: 14.0px}

написал dsorokin (noreply@blogger.com) 29 ноября 2016, 20:23

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

Неизвестная Миру Лямбда Кодировка с CPS Континуатором

НАМО ЛЯМБДАГАРБХА

Итак, как вы все знаете, в PTS системах для кодирования индуктивных типов данных принято использовать лямбда исчисление. Все вы знаете про Church, Parigot, Scott кодировки. Если кто забыл, я быстро напомню! Но есть одна особая кодировка, которая круче чем все эти кодировки, но которая почему-то совершенно не описана в литературе. Кто найдет ее упоминание в интернете -- пишите сюда.

Будем использовать инфиксную скобочную форму записи лямбды: "(a b -> c)" означает "λ a b . c", чтобы λ не мусолила глаза и легче было распознавать узор последовательности.

1. Church кодировка. Самая простая. Она представляет структуры в виде своих правых фолдов. Будем рассматривать простейшие структуры данных натуральные числа. Они же используются дя чистого моделирования вселенных.

0 = (f x -> x)
1 = (f x -> (f x))
2 = (f x -> (f (f x)))
3 = (f x -> (f (f (f x))))

pred    = (n (g h -> (h (g succ))) (const zero) id) -- O(n), хуйня.
foldNat = (s z nat -> (nat s z))                    -- Нерекурсивный, заебись.

С ней есть "маленькая" проблемка: pred такого числа или tail списка занимает O(n).

2. Scott кодировка. Дана Скотт предложил кодирвать структуры не в виде их фолдов а в виде их паттерн мачинг элиминаторов.

0 = (f x -> x)
1 = (f x -> (f (f x -> x)))
2 = (f x -> (f (f x -> (f (f x -> x)))))
3 = (f x -> (f (f x -> (f (f x -> (f (f x -> x)))))))

pred    = (nat -> (nat (pred -> pred) _))                       -- O(1). Заебись.
foldNat = (s z nat -> (nat (pred -> (s (foldNat s z pred))) z)) -- Рекурсия, Хуйня.

Для такой кодировки у нас pred натурального числа занимает константу, но для выражения нужна рекурсия. А мы на это в Групоид Инфинити никак не можем пойти.

3. Кодировка Parigot. Является смесью Скотт и Черч кодировок. Паригот убирает рекурсию из фолдов.

0 = (f x -> x)
1 = (f x -> (f (f x -> (f x)) (f x -> x)))
2 = (f x -> (f (f x -> (f (f x))) (f x -> (f (f x -> (f x)) (f x -> x)))))
3 = (f x -> (f (f x -> (f (f (f x)))) (f x -> (f (f x -> (f (f x))) (f x -> (f (f x -> (f x)) (f x -> x)))))))

pred    = (nat -> (nat (_ pred -> pred) _)) -- O(1). Заебись.
foldNat = (nat -> (nat (fold _ -> fold) _)) -- Нерекурсивный, Заебись.

Как вы видите Паригот вроде как заебись, но термы ростут как на дрожжах. Т.е. экспоненциально. Но мы можем избавиться от этого!

4. Кодировка CPS. Вместо нумералов черча мы храним континуаторы (c -> (c f x)). Описание этой кодировки вы не найдете в интернете ни в одном пейпере.

0 = (f x -> x)
1 = (f x -> (f (c -> (c f x)) (f x -> x)))
2 = (f x -> (f (c -> (c f x)) (f x -> (f (c -> (c f x)) (f x -> x)))))
3 = (f x -> (f (c -> (c f x)) (f x -> (f (c -> (c f x)) (f x -> (f (c -> (c f x)) (f x -> x)))))))

pred    = (nat -> (nat (_ pred -> pred) _))                   -- O(1). Заебись!
foldNat = (s z nat -> (nat (cont pred -> (s (cont pred))) z)) -- Нерекурсивная Заебись!

И термы все растут так как при черче просто умножаются на константу -- размер континуатора. Одна хуйня что для этой кодировки нужны Self-типы Пенг-Фу и Ко, слабая форма рекурсивных типов. Но зато индукция и все остальное получается бесплатно для этой кодировки.

Бенчмарк CPS кодирвки против Church кодировки:
Pack/Unpack 1 000 000 Inductive Nat Church:  {410682,#Fun}
Pack/Unpack 1 000 000 Inductive Nat CPS:     {712684,1000000}
Pack/Unpack 1 000 000 Inductive Church List: {717695,'_'}


Типа в два раз медленнее.

%  data nat: * :=
%       (zero: () → nat)
%       (succ: nat → nat)

% Church
nat    () -> [fun (Succ) -> 1 + Succ end, 0 ].
zero   () -> fun (Succ) -> fun (Zero) -> Zero end end.
succ   () -> fun (Nat) -> fun (Succ) -> fun (Zero) -> Succ((Nat(Succ))(Zero)) end end end.

% CPS
nat1() -> [fun (F) -> fun (X) -> F(X) + 1 end end, 0 ].
zero1() -> fun (F) -> fun (X) -> X end end.
succ1() -> fun (Z) -> fun (F) -> fun (X) -> (F(fun(C) -> (C(F))(X) end))(Z) end end end.


https://github.com/groupoid/om/blob/master/src/cc.erl

ОМ ЛЯМБДА ГАРБХА ХУМ

29 ноября 2016, 19:12

28 ноября 2016

beroal

достаточно одной функции

Из свойства суммы морфизмов (например, для 3-местной суммы: A_0+A_1+A_2→B ≅ (A_0→B)×(A_1→B)×(A_2→B)) следует, что несколько функций можно заменить на одну. Говоря языком простых программистов, семейство функций можно заменить на одну глобальную функцию, которая принимает имя функции из этого семейства и аргумент и вычисляет функцию, имя которой приняла.

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

28 ноября 2016, 08:26

24 ноября 2016

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

Лямбда Калкулус на Стримах

Кто кушал вкус свободных монад, тот знает, что все синтаксические деревья имеют свои интерпретаторы. Деревьями мы кодируем FSM выразимые тем, что мы называем "данными", а CPS-интерпретаторы мы называем "кодом". Выполнение кода каждого хендлера такой синтаксической единицы мы называем 1 тактом выполнения в интерпретаторе. В процессе интерпретации программы мы вызываем poll у текущего элемента в дереве и он вызывает poll у детей вниз по синтаксическому дереву, попутно выполняя редукции и создавая матрешки контекстов, которые и есть env.

Плюсы такой системы: интеграция интерпретатора и паралелизатора стримов с интерпретатором лямбда калкулуса в единую библиотеку комбинаторов. Наряду с векторизирующими Fold, Map, Over, Scan, Filter комбинаторами мы имеем Lambda, Call, Cond, Assign. Дальше синтаксические конструкции дерева могут расширятся — мы просто ложим файл хендлер единой функции poll соотв. комбинатора.

Посмотрел бегло интернет но такого чтобы имплементации такого интерпретатора — то нет, не найти. Може я гоню или идея ок? Простой и элегантный векторизирующий лямбда интерпретатор. В таком интерпретаторе имплементация размазана по веткам дерева, в отличие от классических интерпретаторов об одном switch.

Может кто знает пейперы какие есть?

24 ноября 2016, 23:58

23 ноября 2016

nponeccop

Габриэль жжот

http://www.haskellforall.com/2016/07/auto-generate-service-api-endpoints.html
{-# LANGUAGE DeriveGeneric #-}

import Server.Generic

data Command
    = Add      Double Double
    | Multiply Double Double
    deriving (Generic)

instance ParseRecord Command

handler :: Command -> IO Double
handler (Add      x y) = return (x + y)
handler (Multiply x y) = return (x * y)

main :: IO ()
main = serveJSON 8080 handler
If you run the above code, you get a server that has two endpoints:
/add/:double/:double
/multiply/:double/:double
You can run the server and test that they work:
$ curl 'localhost:8080/add/2/3'
5
$ curl 'localhost:8080/multiply/2/3'
6
Ну то есть, если по русски, - пейнлесс тайпед рест

23 ноября 2016, 03:09

HNC - очередная перезагрузка

HNC задумывался как small hackable codebase, но с хакабилити получилось не очень. В-основном, из-за высокотехнологичности - куда ни плюнь, попадёшь в пейпер. Что не обязательно хорошая черта, но помогает уменьшить размер и держать меня мотивированным. Но кроме параморфизмов, мешает ещё и монолитная структура. Буду её разделять. Ну и лигаси (SPL) можно вырезать, всё равно там чекер нерабочий.

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

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

Минимально понадобится:

1. Парсер

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

2. Тайпчекер

- Оставить на UUAG и unfication-fd, но синтезировать дополнительный атрибут - AST, декорированное типами. Сейчас эта декорация сидит внутри UUAG и как бы фьюзится, тут же потребляясь кодогенератором С++, т.е. снаружи UUAG не видна. Соответственно, человек не может посмотреть, какой результат выдает чекер - трассировка сгенерированного UUAG катаморфизма повергнет его в ступор. И не может легко его забрать к себе, поскольку в UUAG нет внутренней модульности атрибутов и не очевидно, какие атрибуты ему нужны, а какие приватны для чекера.
- добавить while и :=
- добавить тайпклассы. Без Ord, Eq, Show жизнь не мила

3. Оптимизатор

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

На самом деле он вообще требует только графа, GraphCompiler/GraphDecompiler у меня и так уже отделены. Но конечно полный игрушечный пайплайн (парсер-графкомпилер-оптимизатор-графдекомпилер-приттипринтер) нужен, поскольку легче ковырять руками, термы понятнее, чем текстовое представление из графа. Можно убрать из декомпилера восстановление дерева скоупов и оставить только восстановление имён, опять же чтобы было понятнее.

4. Классификатор-кодогенератор

Это самый адов ад, просто из-за дебилизма С++ как низкоуровневой хрени, но сейчас пользователь именно его видит в первую очередь https://github.com/nponeccop/HNC/blob/master/Bar.ag#L88 и пугается.

Можно оставить как есть (с зафьюженным модифицированным чекером из п.2, благо в UUAG это выглядит просто как инклуд).

5. AST генерируемого подмножества С++ и его приттипринтер

Они и так отделены в CPP.Intermediate и CPP.Visualise, но можно ещё более отделить в какой-нибудь Data.CPP. Увидел тут, что часть приттипринтера лежит в CPP.BackendTools, надо исправить.

6. Тривиальные бекенды

Допилить Lean (который не тривиален, поскольку типы, но прост), и запилить какие-нибудь JS и PHP. А че, даже парсер + чекер + кодоген в ПХП будет прикольной игрушечкой кому-нить.

23 ноября 2016, 02:25