A64m
короче говоря он не мог установить, что аргумент у mergeSort убывает, потому что сплит, как он думал, мог возвратить (аргумент, []) так что сорт опять вызывался бы с аргументом той же длины
A64m
пришлось в посткондишене для сплита записать что длины списков которые он выдает не отличаются больше чем на 1
A64m
этот посткондишн он смог проверить, и потом понял, что сплит не вернет [] ведь пустой список и список единичной длины в эту ветку не попадает
A64m
полный пример
module MergeSort where
import Data.Set (singleton, union, empty, Set)
{-@ measure toSet @-}
toSet :: (Ord a) => [a] -> Set a
toSet [] = empty
toSet (x:xs) = singleton x `union` toSet xs
{-@ predicate Break X Y Z = len X = len Y + len Z @-}
{-@ predicate Complete X Y Z = toSet X = Set_cup (toSet Y) (toSet Z) @-}
{-@ type IncrList a = [a]<{\xi xj -> xi <= xj}> @-}
{-@ split :: x:[a] -> ([a], [a])<{\y z -> (Break x y z && Complete x y z && len y - len z <= 1 && len z - len y <= 1)}> @-}
split :: [a] -> ([a], [a])
split (x:y:zs) = (x:xs, y:ys) where (xs, ys) = split zs
split xs = (xs, [])
{-@ merge :: (Ord a) => xs: IncrList a -> ys: IncrList a -> { zs: IncrList a | Break zs xs ys && Complete zs xs ys } / [len xs + len ys] @-}
merge xs [] = xs
merge [] ys = ys
merge (x:xs) (y:ys) | x <= y = x : merge xs (y:ys)
| otherwise = y : merge (x:xs) ys
{-@ mergeSort :: (Ord a) => xs:[a] -> {ys : IncrList a | len xs = len ys && toSet xs = toSet ys } / [len xs] @-}
mergeSort [] = []
mergeSort [x] = [x]
mergeSort xs = merge (mergeSort ys) (mergeSort zs) where (ys, zs) = split xs
A64m
да я с этого и начинал, но там доказывается только то, что список отсортированный
A64m
ни то, что элементы в результате те же, что и раньше, ни даже вроде то, что длина списка сохраняется там не проверяется. Ну и завершимость не проверяется
Alexander
я кстати могу нармсовать алгоритм неплохой
Alexander
sort = const []
Alexander
отлично сортурет, даже Ord не требует
Alexander
есть ещё кстати один
Alexander
sort xs@(a:_) = replicate (length xs) a
A64m
да, такой вроде посткондишены из учебника пропустят
Alexander
а этот и твоё пройдет наверное
Alexander
а нет
A64m
так что мне пришлось множества добавить
Alexander
у тебя toSet
Denis
прикольно, казуальненько
Denis
я на коке когда insertion sort и merge sort доказывал чуть ёжика не родил
A64m
ну так это специально придумано, чтоб ежей не рожать
A64m
впрочем, я не поручусь что там все условия которые нужны заданы и не получится как-то его поломать чтоб ликвидхаскель это съел
Denis
ну так это пруф только если в боттомы не верить
Alexander
это доказательство ломается с одинаковыми значениями
Alexander
т.к. [b,a,b,d] ~> [a,a,b,d]
Denis
на 8.2.1 еще не работает LH?
Alexander
по алгоритму проходит
Alexander
по типу
A64m
да точно
Alexander
там нужно честную перестановку возращать
A64m
надо там мапы а не сеты
Alexander
если по взрослому
Alexander
или мапы, так тоже прокатит
A64m
но вот можно ли такой баг в коде сделать, чтоб одних элементов становилось настолько же больше, чем других меньше?
A64m
это надо непростую логику в код добавлять
Alexander
не знаю как сделать такой баг
Alexander
это ведь нормально посылать один и тот же доклад на fby и fpconf
Alexander
на разных языках правда
Aleksei (astynax)
Аудитории получятся не слишком пересекающиеся, так что норм
Aleksei (astynax)
Да и видео с fpconf не успеют выложить к началу fbyby, так что контент, можно сказать, уникальный будет
Denis
меня с fpconf просили неповторяющиеся доклады то ли год, то ли два подряд
Alexander
в смысле не делать такой же доклад в других местах, или что ты такой раньше не делал?
Denis
оба, по идее
Alexander
хм ну ок
Denis
@qnikst ну ты это, если явно не просили, то и не морочься
Denis
тем паче что доклады, которые получается несколько раз рассказать, с повторами улучшаются
Denis
ферментируются, типа
Alexander
мне вообще не нравится идея одного и того
Alexander
но у ребят из fby "много заявок и решение затягивается"
Alexander
а в списке докладчиков уже появились Nikolay Rizhikov из health samirai и oskar wisktrom и они уже один раз "потеряли заявку", и я как-то очень concerned об этой огранизации
Alexander
хотя выступать бы там хотелось
Alexander
я не знаю может они там завалены заявками от Well Typed и FPCO и StandardChartered что не могут выбрать, и каждая вторая фирма согласна на какую-то форму sponsorship
Alexander
но как-то сомнительно это
Алексей
@qnikst а о чем доклад, кстати?
Alexander
на fby?
Alexander
про alphasheets: Architecting a Haskell SaaS that runs on your son's Windows laptop.
Alexander
girlfriend's laptop звучит лучше, но нечестно рассказывать, когда нету girlfiend-ов :)
Anonymous
а fby на ютюбе будет?
Alexander
про ютуб не знаю но записи с прошлых лет есть
Anonymous
где?
Alexander
вообще тут огранизаторы есть
Alexander
https://www.youtube.com/watch?v=aYA4AAjLfT0&list=PLpVeA1tdgfCA1qKPJUXkwhEDK3dnWhYXf
Anonymous
оо thx
Alexander
/me стало не так стыдно за свой английский
Anonymous
по сравнению с большим количеством подобных конференций здесь очень интересные темы
Alexander
в смысле haskell xchange, icfp и т.п.?
Alexander
@anarchostatist ^
Anonymous
эти тоже хорошие)
Alexander
@PineappleZombie вроде там есть что рассказать и хорошего и плохого
Кабачок
Да, акцент у Божидара жестокий, но привычный.
Alexander
русский акцент веселый и узнаваемый
Кабачок
Но он болгарин 🌚
Alexander
да одна фигня вплоть до чехии и польши
Alexander
я хотел написать восточных славян, но поленился
Алексей
Чехия и Польша не восточные славяне
Alexander
ну совсем завалили : (
Alexander
ок, и западные тоже
Alexander
стоп
Alexander
я чехию и польшу не включал