где к "типу" можно предикат добавлять и он на каждый чих будет в рантайме проверяться

ну если нигде нету проверки, то ликвидхаскель тоже бессилен будет

ну смотря какая операция

хотя да, тоже бессилен

кто-нибудь ликвидкаскель пробовал, кстати?

я только ради hello world

а как в виме вместо jk

по словам

говорят #serokell юзали

вместо jk, wb, WB, IA, $^, по скобкам по абзацам

да, я тоже только с проверками мерджсорта поигрался

так вроде Денис Шевченко не выдержал этого канала, он что-то говорил

вместо jk, wb, WB, IA, $^, по скобкам по абзацам

ещё /word и ?word, когда надо быстро прыгнуть в точку текста

вот в виме с ( ) я запомнить не могу

как он себя ведёт

я активно использую f и t, но не так активно F и T - переход на символ в строке

о!

/me высылает виртуальных напитков @aragaer

вот в виме с ( ) я запомнить не могу

а что эти команды делают вообще? я ими не пользуюсь

вот { } пользусь

( - начало абзаца, первая строка перед пустой или что-то такое

в общем оно сложное

увидел как-то на форуме док-во инсертсорта на Dafny и конечно подумал, вот сейчас мерджсорт докажу, но я, как обычно, в своем репертуаре делал это года полтора

) Jump forward one sentence.

(работы там минут на 10, если ничего про ликвидхаскель не знать, правда)

забавно

на идрисе то уже сортировки доказали

> вот сейчас … докажу

такая постановка вопроса это почти всегда фейл у меня

@bravit111 говорил что был человек с блогом который долго и упорно доказывал, но так и не довёл до конца

ибо доказать не поговнякать код

мы асинхронщину моделировали на spin/promela

норм было, но если именно модель

хотя не доказал еще, завершимость там не чекается

) Jump forward one sentence.

а, это для художественного текста что ль

открыл файл с хаскель-кодом, он у меня по композициям прыгать начал

т.е. по точкам

а вот черт знает что они предложением считают

у меня по -> прыгал

@qnikst круто, мне про модел чекинг интересно на практике

можешь рассказать про то что проверяли и какой опыт?

там очень простое было

про spin/promela

багов отловили немного в программе

хм.. тема для fpconf?

самые интересные модельки Факундо делал пока я ещё и не работал там

я лично только модельку протокола смены лидера с таймером делал

но вообще идея хорошая

правда плохо про это рассказывать когда нету опыта с isabela, T-что-то-там

в которых умные люди что-то доказывают

isabela?

ты не про isabelle/hol случаем?

это не говоря про sequential calculus и вообще все что @antontrunov и их группа делают

ликвидхаскель сам понимает что split :: [a] -> ([a], [a]) split (x:y:zs) = (x:xs, y:ys) where (xs, ys) = split zs split xs = (xs, []) завершается для того чтоб понять что завершается merge xs [] = xs merge [] ys = ys merge (x:xs) (y:ys) | x <= y = x : merge xs (y:ys) | otherwise = y : merge (x:xs) ys ему требуется хинт / [len xs + len ys] но вот mergeSort [] = [] mergeSort [x] = [x] mergeSort xs = merge (mergeSort ys) (mergeSort zs) where (ys, zs) = split xs мы с ним уже не тянем

печалька

о в рабочем чятике про опетопы

https://twitter.com/nikitonsky/status/922908427353026561

когда программист говорит "улучшить" он подразумевает "сифицировать"

потому что куда уж лучше си. писать на си, правда, обычно не хочет

по-моему там какой-то js получился

так так и задумано

предполагается, что на ризоне будет писать джаваскриптер и компилировать в джаваскрипт

Они хоть ML из названия убрали, чтобы не позориться

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

что не делай, а получится ̶г̶о̶в̶н̶о̶ js

Не чтоб не позориться, а чтоб не отпугнуть практика каким-то эмелем

хотя 99.99% все равно расшифруют ML как машин лернинг

https://github.com/steshaw/plt

где к "типу" можно предикат добавлять и он на каждый чих будет в рантайме проверяться

контракт же

ок, я вечно забываю как что в лиспах зовется

в реккете как минимум ето называют контрактами

к ризонтвиту потрясающие реплаи, я сначала подумал, что человек шутит, но оказалось что он поехавший

@qnikst слоан говорил на HEAD обновляться чтоли? % stack upgrade Current Stack version: 1.5.1, available download version: 1.5.1 Skipping binary upgrade, you are already running the most recent version shadowed dependencies повсюду

говорил, что да, я не перепроверил

binary?

stack upgrade --git?

@catamorphism ^

я вообще могу попробовать снова и отрепортить если не работает, я не перепроверял

у меня и так обновление окружения на nix было, ещё и на это время терять

так, доказал завершимость

как?