Comments 85
Для всех кого заинтересовала данная тема, советую посмотреть на liquidhaskell.
А почему это будущее-то? Поиск по странице по слову «будущее» находит три вхождения: в заголовке, в тегах и в подзаголовке выбора «светлого будущего» из трех будущих, мягко говоря, вообще никак даже не пытающихся прикинуться аргументированными.
А почему это будущее-то?
Потому что позволяет получать больше статических гарантий, способы получения которых с адекватными трудозатратами и обсуждаются в этой статье.
У вас есть какие-то причины, почему они могут не быть полезны?)
Я эту мантру овердевятьтысяч раз из каждого холодильника уже слышал, и даже сам [в некотором приближении] с ней согласен. Просто, если «будущее» появляется в заголовке и тегах, можно как-то ну хотя бы попытаться что-нибудь похожее доказать (ну, типа).
Больше статических гарантий — это очень хорошо, но в реальном мире у нас бизнес-логика все время лезет в ансейф, и все гарантии именно в трудных местах — идут лесом.
Больше статических гарантий — это очень хорошо, но в реальном мире у нас бизнес-логика все время лезет в ансейф, и все гарантии именно в трудных местах — идут лесом.
Бизнес логика это весьма неоднозначное понятие, потому я не могу судить, о каких конкретно ограничениях вы говорите. Можете привести примеры?
Например, общение со сторонним провайдером данных, который эти самын данные генерирует левой пяткой.
Например, общение со сторонним провайдером данных, который эти самын данные генерирует левой пяткой.
Мы не можем гарантировать корректность внешней системы, внешнего мира.
В случае получения данных от внешней системы нам в любом случае придётся проверять их на уровне нашего приложения, а там уже некорректность обнаружится и обработается как предполагается.
Прохождение валидации я и безо всяких типов могу гарантировать. Валидацию в любом случае надо будет написать, и это еще бабушка надвое сказала, что выгоднее: pattern-matching, или типы.
Валидацию в любом случае надо будет написать, и это еще бабушка надвое сказала, что выгоднее: pattern-matching, или типы
А они разве противоречат друг другу?
Не так, потому что в обычных языках у вас прохождение валидации — это действие, а не значение.
Ох.
def preprocess(%{
foo: [:bar | _],
int: 42,
any: any,
nested: %{type: type} = nested
} = value) when type in [:a, :b], do: {:ok, value, {any, nested}}
def preprocess(value), do: {:error, value}Действие, так действие.
А вы точно хотя б на хаскеле писали?
Да, но, как я говорил, это было в 2000–2003 и с тех пор я только научпоп почитываю. Я отдаю себе отчет в том, что могу не видеть за деревьями леса, но обычно (чисто статистически) внятные аргументы меня убеждают.
А противопоставление действий — значениям — нет.
Непонятно, но споры об этом идут уже почти 30 лет =)
Учитывая, сколько фичей переехало из хаскеля в мейнстрим и продолжает перетекать, можно ответить философски: для кого прошлое, а для кого и будущее.
Ну, я для себя решил все же попробовать. Приятно все-таки писать настолько безопасный и гибкий код, который на остальных языках начнут писать только через 5-10 лет. И людям все равно придется учить все те же концепции, когда они попадут во всякие Java/C++, но эти 5-10 лет они потеряют, пользуясь менее удобными инструментами.
В общем, каждому своё, мой выбор меня пока устраивает.
Ну, более удобного языка я не знаю. Из распространенных ФП языков есть только хаскель и скала, остальное всё сырое и непонятное. И, кто бы что ни говорил, а получение работающей программы во время обучения важно. Я вот на хаскелле на день забахал простенький рест-сервер со сваггером, который отдавал пару константных сущеностей. Правда, на этом моего шапочного знакомства хватать перестало, и когда я БД подключил у меня всё поломалось, так что пришлось идти читать learnyahaskell, но в целом можно написать что-то рабочее.
В хаскелле хватает "исторически сложилось", но если выбирать между ним и скалой, то в ML варианте получается сильно проще — по крайней мере после прочтения красной книги и курса по хаскелю на степике. Просто сравните:
val optionFunctor: Functor[Option] = new Functor[Option] {
def map[A,B](fa: Option[A])(f: A => Option[B]): Option[B] = fa match
case None => None
case Some(x) => Some(f(x))
}И
instance Functor Maybe where
fmap _ Nothing = Nothing
fmap f (Just x) = Just (f x)И это еще не говоря про сложности с имплиситами, отсутствием запрета на нечистые действия, и прочее, прочее...
В общем, возможно где-то есть более хорошие для изучения ФП языки, но я их не знаю.
А под него есть всякие идеи с автокомплитом и хуглом как для хаскеля? Потому как всё это важно.
Я пользуюсь идеей с плагином, причем на Windows. Умеет она всякое разное, например простенькие рефакторинги
Подсказка типов (без необходимости писать дырку и спрашивать что за тип)
Автоматические импорты, которые очень выручают, особенно меня как новичка, когда я пишу код из интернета а он почему-то не работает
Ну и в целом я не согласен с
Хугла нет (так как нет пакетного менеджера), но для изучения это и не нужно, имхо.
Как раз когда я начал пытаться склеить сервант с персистом я понял, зачем нужен МТЛ и трансформеры. До этого это было теоретическим знанием с игрушечными примерами "Обойдите дерево и сохраните сколько узлов вы обошли", а вот реальный пример позволяет прочувстввоать, что это и зачем.
А вообще прикольно, надо тоже попробовать. Я пробовал прикрутить плагин к CLion, оно установилось, но что-то не сработало. Попробую с голой Idea. vim, конечно, хорошо, но изолента проглядывает. И да, сколько это все счастье ест памяти? А то у меня hie счастливо десяток гигов на проект съесть может.
Ну я ничего крупного не открывал, но на моих маленьких крудах — 500мб.
Это с hlint, или там свои диагностики?
К сожалению понятия не имею. Оно жаст воркс, и глубже я не лезу. Из проблем только то что после изменение кабал/стак файла нужно перегружать репл. Но зависимости не так часто добавляются, так что жить можно.
Это уже просто следующий уровень изучения.
Но в него очень быстро упираешься. Сортировать числа и факториалы считать очень весело, но все же утомляет. А реальное приложение с БД без этих знаний не написать.
Для хаскелля я нашел хороший курс на степике от Москвина. Для идриса таких не видел.
Учитывая, сколько фичей переехало из хаскеля в мейнстрим и продолжает перетекать, можно ответить философски: для кого прошлое, а для кого и будущее.
В общем-то из вещей специфичных именно для хаскеля очень мало что переехало. Если вообще хоть что-то, мне вот навскидку ничего в голову не приходит. Разве что тайпклассы в какой-то форме, ну и higher-kinds с их кодировками
Вряд ли вы добьетесь любви к Хаскелу у людей, которые его еще не любят (особенно пишущих на С и С++), используя фразы типа "Языки с небезопасным доступом к памяти, такие как C, приводят к самым серьезным ошибкам и уязвимостям (например, переполнение буфера, утечки памяти). Иногда такие языки нужны, но чаще всего их применение – идея так себе."
Я, например, считаю, что эта фраза просто ошибочна. В некоторых областях разработки (где очень много людей работает) вас просто засмеют.
С другой стороны, хотя бы кодировка для них у нас есть!
Нет, ее нет. Зависимые типы, в отличии от каких-нибудь higher-kind, не кодируются в более слабых системах.
То, что описано далее — это простой лифтинг на уровень типов, возможный в любой системе с параметрическим полиморфизмом. Работает он только тогда, когда тип известен в компайлтайме.
А можно пример когда не работает? Вот у меня с консоли считывается булка и вполне себе на неё потом можно прицепить SBool: https://repl.it/@Pzixel/PowerfulBulkyLightweightprocess
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
data SBool (b :: Bool) where
STrue :: SBool 'True
SFalse :: SBool 'False
fromSBool :: SBool b -> Bool
fromSBool STrue = True
fromSBool SFalse = False
data SomeSBool where
SomeSBool :: SBool b -> SomeSBool
withSomeBool :: SomeSBool -> (forall (b :: Bool) . SBool b -> r) -> r
withSomeBool (SomeSBool sbool) f = f sbool
toSomeBool :: Bool -> SomeSBool
toSomeBool True = SomeSBool STrue
toSomeBool False = SomeSBool SFalse
main = do
b <- readLn
let
someBool = toSomeBool b
bool = withSomeBool someBool fromSBool
putStrLn (show bool)
Все работает, если постараться :) https://gist.github.com/int-index/743ad7b9fcc54c9602b4eecdbdca34b5
Максимум, что позволяет подобная кодировка — это "расщепить" типы по паттерн-матчингу. Ну т.е. как если бы у тебя в АТД каждый элемент суммы был как бы отдельным типом (как это, допустим, в тайпскрипте происходит, когда ты пишешь что-то вроде type Yoba = { type: 'Foo' } | { type: 'Bar' }), то type Foo = { type: 'Foo' } и type Bar = { type: 'Bar' } — это сами отдельные типы. С-но, ты можешь сделать кейз на тип и потом где-то дальше уже знать, что твое значение это не какой-то непонятный Yoba, а вполне себе конкретный Foo (т.е. значение соответствует паттерну, и этот факт выражается в типе — ты можешь сформулировать тип которому принадлежат только те значения, что соответствуют паттерну). Но на этом все.
Ну мне тут в контрпримером бросились, такое ощущение, что можно: https://gist.github.com/Nexmean/56c98ff9563ff25a05b70512a7de6848
Для зав. типов надо уметь параметризовать тип термом. В данном случае мы можем параметризовать тип термом, который можно вычислить в компайл тайме (лифтанув этот терм в типы). Но мы не можем параметризовать тип термом, который в компайлтайме неизвестен.
Т.е. ты можешь написать vector<5> или vector<10>.
Ты можешь написать vector<*>, где * неизвестно (при этом эффективно vector<*> будет означать тип всех векторов), считать этот вектор, а потом разматчить этот вектор на vector<5>, vector<10>, vector<Greater<5>> и т.п.
Но ты не можешь написать vector<*>, где * у тебя переменная в локальном скопе.
Обрати внимание на определяющую разницу с предыдущим пунктом — в первом случае vector<*> это _любой_ вектор, а во втором — это конкретный вектор с конкретным *, которого мы не знаем (но который будет однозначно фиксирован в момент исполнения).
Как это не можем? Вот мы число с консольки считываем, как по мне это вполне считается за границу "неизвестное значение".
Ну напиши :)
Ты вот в примере выше с булями если считаешь подряд два булевых значения, то у них будут одинаковые типы. А если ты считаешь два булевых значения с dependent types — типы будут разные. И ты сможешь написать ф-ю test, которая, например, будет чекаться если були равны и не будет — если они не равны.
> Вот мы число с консольки считываем, как по мне это вполне считается за границу «неизвестное значение».
Ну вот тут оно будет «какое-то число», а в зависимых типах — «конкретное число». В случае «конкретное число» ты сможешь, например, сделать vectorRef с k < n, а в случае «какое-то число» операция vectorRef будет запрещена для любого k. Т.е. ты можешь создать vector, но при этом ничего с таким вектором не сможешь сделать. Тебе сначала надо будет преобразовать его к какому-нибудь более конкретному типу.
А как сделать Fin n, где n это узнаем в рантайм. У bool только два типа, поэтому сделать матч значение в тип можно, а для бесконечных множеств как? Нужен чтобы каждый вызов функции создавал новый тип, как ефекты в идрисе.
Я после bool еще один пример скинул, там вполне себе Fin n
Так это то же самое что bool только с рекурсией. Всё равно у вас функция которая аргументу сопоставляет тип. А мне кажется надо выдавать именно что уникальный тип. Иначе я не понимаю как это работает, вот вы считываете А и В, они получается в рантайме конкретный тип получают по своему значению? А какой тогда тип у А + В, как доказать что А + B больше А для натуральных чисел?
Хм. А были какие-то движения в сторону поддержки haskell кода? Я к тому что ФП языков мало, и если бы я захотел написать новый, я бы взял в рассчёт некоторую совместимость с более популярными языками.
например, хаскель не различает данные и коданные
Почему не различает? Есть же strictness аннотации. Все, что с ними — это данные, без них — коданные.
И хаскель, в который добавят завтипы, не будет «полноценным идрисом».
Refinement типы можно добавить. Будет все, что можно сделать на зависимых, но только проще и удобнее.
который не пойми что
Почему не пойми что? Вы можете на, допустим, агде без коиндукции написать аналог хаскелевского []? Нет. Значит, это коиндуктивный тип. Как и все вообще типы хаскеля без strictness аннотаций. data Nat = Zero | Succ x — тоже коиндуктивный, например. Тут, конечно, тот момент что x seq f(x) это не совсем то же самое, что и force, но по факту это детали реализации.
mega.nz/#!PrInzYAa!zPnzW6Dj4hRQz5qJSPFBnnC5YCAII_1-9eFZuj2qYs8
и краткая биография Шмаина
mega.nz/#!XjBHmKBB!qh7Bme8Zx1_rOPWFNOERtm-59_tVTxjTPg6zpyVrkbU
Ссылки копировать целиком (почему-то плохо вставляются)
gen.lib.rus.ec/book/index.php?md5=43A67A9BF71F483E34879816454E04EF
но чтение не простое). Но эти схемы не наглядны с самого начала, даже маленькие. С другой стороны, у категорщиков теперь есть пруфчекер Globular, позволяющий строить доказательства о категориях в виде картинок в графическом редакторе
golem.ph.utexas.edu/category/2015/12/globular.html
(на картинки полюбуйтесь, даже узел из ниток получается).
А в текстовом виде будто умещаются.
И тулинг – дело наживное.
— Что, братишка, не получается?
Ничто в этих сигнатурах типов не отражает требования, что индекс должен быть неотрицательным и меньше длины коллекции
А в Pascal диапазоны есть издревле:
const
minlist = 1;
maxlist = 5;
maxword = 7;
type
listrange = minlist .. maxlist;
wordrange = 1..maxword;
word = record
contents: packed array [wordrange] of char;
length: wordrange
end;
wordlist = array[listrange] of word;
var
i: integer;
words: wordlist;
procedure CreateList(var w: wordlist);
begin
w[1].contents := 'print ';
w[1].length := 5;
w[2].contents := 'out ';
w[2].length := 3;
w[3].contents := 'the ';
w[3].length := 3;
w[4].contents := 'text ';
w[4].length := 4;
w[5].contents := 'message';
w[5].length := 7;
end;
begin
CreateList(words);
for i := minlist to maxlist do
with words[i] do
WriteLn(contents: length);
for i := maxlist downto minlist do
with words[i] do
WriteLn(contents: length)
end.В который раз убеждаюсь, что паскалиное семейство незаслуженно забыто. Относительно C язык довольно безопасный: указатели строго типизированные, массивы защищены от выхода за границы. При этом не генерирует огромные бинари, как Go и Haskell, и не компилируется полчаса, поливая матом код до полного прилизывания, как Rust. А Lazarus вдобавок позволяет делать графические приложения, которые прозрачно собираются с GTK+ или Qt, удовлетворяя тулкитофобов обоих лагерей. Что ещё нужно для счастья?
Ну не знаю, я вот спокойно записал по индексу 0 и 55 два значения, и меня компилятор не остановил.
Главное, что сегфолта нету. И компилятор таки ругается.
@bq:00:42:39:/tmp/dl$ fpc a.pas
Free Pascal Compiler version 3.0.4+dfsg-23 [2019/11/25] for x86_64
Copyright (c) 1993-2017 by Florian Klaempfl and others
Target OS: Linux for x86-64
Compiling a.pas
a.pas(20,5) Warning: range check error while evaluating constants (0 must be between 1 and 5)
a.pas(32,5) Warning: range check error while evaluating constants (55 must be between 1 and 5)
Linking a
/usr/bin/ld.bfd: предупреждение: link.res содержит выходные разделы; забыли указать -T?
43 lines compiled, 0.5 sec
2 warning(s) issuedИ есть ключик для более строгой проверки.
@bq:00:46:44:/tmp/dl$ fpc -Cr a.pas
Free Pascal Compiler version 3.0.4+dfsg-23 [2019/11/25] for x86_64
Copyright (c) 1993-2017 by Florian Klaempfl and others
Target OS: Linux for x86-64
Compiling a.pas
a.pas(20,5) Error: range check error while evaluating constants (0 must be between 1 and 5)
a.pas(32,5) Error: range check error while evaluating constants (55 must be between 1 and 5)
a.pas(44) Fatal: There were 2 errors compiling module, stopping
Fatal: Compilation aborted
Error: /usr/bin/ppcx64 returned an error exitcodeНу, это кстати неплохо.
А можно вместо константы использовать аргумент? Например, чтобы CreateList была не процедурой, а функцией, и возвращала массив длины n для передавнного зачения n. Тогда он тоже скажет что значение вышло за границы?
Главное, что сегфолта нету.
В этом только не уверен. Запись мимо массива — это очень нехорошо. Если компилятор конечно не вырезал этот код нафиг, но он вроде так не должен делать.
Или есть какая-то математическая магия которая хотя бы частично это покрывает?
как на стадии компиляции гарантировать, что индекс не выйдёт за пределы массива, при том что значение индекса будет известно только в рантайме — мне кажется это в принципе невозможно.
Можно гарантировать, что сделана проверка на выход за пределы.
Ну это уже в рантайме
Нет, наличие проверки статически гарантируется.
Так я и говорю что наличие проверки в рантайме гарантируется на стадии компиляции, но если на стадии компиляции всё известно, то проверку в рантайм можно не добавлять.
Реальный индекс может быть известен только в рантайме. Но гарантируя наличие проверки мы гарантируем что выхода за границы при обращении не будет.
Да, но если вы можете статически доказать, что индекс за границы не выйдет, то никаких проверок в рантайме не будет.
А есть какой-то способ без проверок рантайма доказать, что произвольное считанное число не выходит за границы? :)
Где-то проверка будет, просто не обязательно прямо в месте обращения к элементу массива.
Зависимые типы в Haskell: почему это будущее разработки программного обеспечения