Category: it

office

Operator :))

Сегодня на работе писал очень веселый код - со смайликами!
...
mergeTypes t1 (t2:ts) = (t2 :) <$> mergeTypes t1 ts
...
fs <- mapM (\(fld, ty) -> silly ty <&> (Str (fld ++" : ") :)) $ M.assocs row
...

Много ли языков их используют?
office

о гарантиях

fn helper<'a, 'b, T>(_: &'a &'b (), v: &'b T) -> &'a T { v }

/// Turn any `&T` into a `&'static T`. May introduce undefined behavior.
pub fn make_static<'a, T>(input: &'a T) -> &'static T {
    let f: fn(_, &'a T) -> &'static T = helper;
    f(&&(), input)
}

(отсюда)
Не ожидал, что так просто. Безо всякого unsafe берем и превращаем "одолженную" ссылку на временное значение в "вечную", с соответствующими use-after-free последствиями. А просто дырка в borrow checker'e, и давно уже, все никак не залатают.
office

спецолимпиадное

По мотивам поста Никиты про разницу в производительности "высокоуровнего/функционального" и "низкоуровнего/императивного" кода. Взял буквально его пример с созданием массива пар чисел. Его оригинал на кложе:
(concat
 (mapv
    (fn [y] [from-x y])
    (range from-y (quot to-y 2)))
  (mapv
    (fn [y] [to-x y])
    (range (quot to-y 2) to-y)))

Как быстро он работает - не представляю.

Попробовал обе версии - "функциональную" и "императивную" - записать на D в качестве эксперимента, посмотреть, насколько компилятор справляется это дело развернуть.
struct Point { int x, y; }

auto f(int from_y, int to_y, int from_x, int to_x) {
    return chain( iota(from_y, to_y/2).map!(y => Point(from_x, y)),
                  iota(to_y/2, to_y)  .map!(y => Point(to_x, y)) ).array;   
}

auto g(int from_y, int to_y, int from_x, int to_x) {
    auto res = new Point[to_y - from_y];
    foreach(y; from_y .. to_y)
        res[y - from_y] = Point(y < to_y / 2 ? from_x : to_x, y); 
    return res;
}

На 60 миллионах точек ( f(20_000_000, 80_000_000, 1, 2) ) "функциональный" у меня работает 167 мс, "императивный" - 146 мс, разница в пределах 15%. Терпимо.
(полный текст тут, компилятор - LDC)

Попробовал записать это дело на хаскеле, но в нем я нуб, не знаю, как правильно его готовить. Вот такой вариант
import qualified Data.Vector.Unboxed as V
type Point = (Int, Int)

f :: Int -> Int -> Int -> Int -> V.Vector Point
f from_y to_y from_x to_x =
    let a = V.generate (to_y `div` 2 - from_y) (\y -> (from_x, y+from_y))
        b = V.generate (to_y - to_y `div` 2)   (\y -> (to_x, y + to_y `div` 2))
    in V.concat [a, b]

на тех же исходных данных работает 1.33 сек, т.е. примерно на порядок медленнее. Другие варианты, что я пробовал, еще медленнее. Например, если data Point = P {-# UNPACK #-} !Int !Int, то оно уже не Unboxed, и если просто Data.Vector для них использовать, то время больше трех секунд уже.
Вопрос хаскелистам: как вы unboxed массив простых структур делаете?
office

Cloud computing

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

В искривленном пространстве. Часть 2

Ну и вот. Написал я тогда модуль символьных вычислений, который умеет арифметику, умеет частные производные, в том числе тригонометрии и сложных ф-й, умеет немного упрощать (выносить за скобки, сокращать дроби, знает, что sin^2 + cos^2 = 1) и умеет генерить код. Этот модуль используется в компайл-тайме, и из одного лишь уравнения поверхности выводит все необходимые формулы и генерит код для каждой фигуры, который тут же компилятором оптимизируется. Посмотрим на примере все той же сферы.
Задаем уравнение поверхности, отображение 2D координат (u,v) в 3D (x,y,z).

Expr[] sphereEq() {
    auto R = new Var("R");
    return [mul(R, mul(new Cos("u"), new Cos("v"))),
            mul(R, new Sin("v")),
            mul(R, mul(new Sin("u"), new Cos("v")))  ];
}

Ф-я возвращает массив из трех выражений - для x, для y и для z. X у меня идет вправо, Y вверх и Z вдаль. Координата u это долгота, координата v - широта, считается от экватора. Имея эти выражения как три компоненты ф-ии
X(u,v) = [R * cos(u) * cos(v), R * sin(v), R * cos(v) * sin(u)]
первым делом находим базисные вектора - производные X(u,v) по u и по v:
    auto Xu = X.diff("u"); 
    auto Xv = X.diff("v");

Получаем вектора
Xu: [[-1 * R * cos(v) * sin(u)], 0, [R * cos(u) * cos(v)]]
Xv: [[-1 * R * cos(u) * sin(v)], [R * cos(v)], [-1 * R * sin(u) * sin(v)]]
Collapse )
bednota

Щастье

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

office

LDC

Сегодня узнал, что в андроидном Termux'e можно сказать "apt install ldc" и можно прям на телефоне писать на D:

До этого у меня там уже стояли gcc, python и ruby. Там же есть vim, он уже знает про все эти языки. Пока что единственное применение было - написал солвер для одной игрушки.
house, tucan

fooling people with theorem provers

Занятный доклад на свежем FP Conf про equational reasoning и теорем пруверы:
https://www.youtube.com/watch?v=TRAPqhRdAH0
Докладчик рассказал, почему Liquid Haskell и F* пока не годятся, потом показал как он на Isabelle верифицировал вывод radix sort'a из tree sort'a, взятый из старинной статьи Gibbons'a. Типа, вот у нас реализация сортировки через построение дерева, вот мы тут колдуем-колдуем с эквивалентными преобразованиями кода и вот свели сортировку к foldr по списку, получился радикс сорт, сортирует за один проход, красота.
Только это все неправда.
То, что там названо treesort'ом, внутри себя уже реализует принципы радикссорта. Идея такая. Вот есть у нас список, условно, коротких строк ограниченной длины, [a]. И есть функции извлечения "букв" a -> b, где тип "букв" b принадлежит классам Bounded и Enum, т.е. все его возможные значения можно перечислить по порядку списком
rng = [minBound .. maxBound]
Тогда входной список "строк" можно разбить на подпоследовательности / бакеты - по одной для каждого значения "буквы". Partitioning function:
ptn :: (Bounded b, Enum b) => (a->b) -> [a] -> [[a]]
ptn d xs = [ filter ((m==) . d) xs | m <- rng ]

Здесь d - функция извлечения "буквы" b из "строки" a.
Тогда возьмем набор функций [a->b] по извлечению из условной строки первой буквы, второй буквы, третьей... Разобьем входные данные на бакеты по первой букве, каждый из них - на бакеты по второй, те - по третьей и т.д., получим дерево списков. В каждом узле дерева бакеты идут по порядку возрастания "букв", так что в итоговом дереве все окажется уже отсортированным, останется лишь его сплющить в один выходной список.
data Tree a = Leaf a | Node [Tree a]

mktree :: (Bounded b, Enum b) => [a->b] -> [a] -> Tree [a]
mktree [] xs = Leaf xs
mktree (d:ds) xs = Node (map (mktree ds) (ptn d xs))

treesort :: (Bounded b, Enum b) => [a->b] -> [a] -> [a]
treesort ds xs = flatten (mktree ds xs)

Тут важно, что mktree принимает два списка, ds и xs, первый это короткий список функций по извлечению "букв", второй - сами данные, которые уже будем сортировать, и организована mktree индукцией по списку функций. И flatten имеет очевидное устройство тоже индукцией по дереву. Ну и вот, дальше Gibbons и вслед за ним наш докладчик просто берут эти mktree и flatten и выражают их через foldr, заменяют явную рекурсию стандартным катаморфизмом, плюс избавляются от промежуточной структуры дерева, т.к. собранное mktree дерево тут же flatten'ом разбирается обратно. И, собственнно, весь equational reasoning и вся верификация на Isabelle сводятся к тому, чтобы показать, что реализация на foldr равна процитированной тут реализации на явной рекурсии. Это дело чистой механики и переписывания термов, сам алгоритм там не меняется ни сколько. Получается
radixsort :: (Bounded b, Enum b) => [a->b] -> [a] -> [a]
radixsort = foldr ft id
  where ft d g = concat . ptn d . g

Вот он, один проход по списку, но это проход по списку функций извлечения "букв", а не по входным данным! А вот по входным данным мы будем елозить внутри ptn, в каждом узле дерева входной список данных будет пройден L раз, где L - размер алфавита. Причем Gibbons в статье это понимает и честно отмечает, предлагая в конце альтернативную реализацию функции раскидывания по бакетам ptn. Но исходные рассуждения и доказательства проводятся не с ней, а с наивным вариантом. Докладчик с FPConf же то ли честно не понимал, что делает, то ли решил публику обмануть ради пущего эффекта. Вот, говорит, сортировка за один проход списка foldr'ом. А что совсем не того списка - не сказал. :) Ну и "доказал корректность" довольно простой тавтологии (radixsort == treesort), молодец.