+1
- 1
- 2
- 3
- 4
- 5
- 6
- 7
- 8
Что-то я давно не обсирал тут хуиту, которую пишут про
плюсы на хабре
https://habr.com/post/426965/
Идеального способа для обработки ошибок не существует.
До недавнего времени в С++ были почти все возможные
способы обработки ошибок кроме монад.
В этой замечательной статье забыли упомянуть setjmp/longjmp(std::longjmp если угодно), который хоть и из Си, но в C++ его никто не запрещал.
А еще signal (std::signal, если угодно), который хоть и из Си, но в C++ его никто не запрещал.
А еще goto (почему нет std::goto? Запилите быстраблядь!), который хоть и из Си, но в C++ его никто не запрещал.
А вообще, зачем иметь в языке такое количество говна в СТАНДАРТНОЙ БИБЛИОТЕКЕ для такой хуиты?
Вот еще в тему: https://video.twimg.com/tweet_video/De78Qn2XcAAQqfS.mp4
Запостил: j123123,
20 Октября 2018
j123123 20.10.2018 18:28 # +1
> Деление на 0. Интересно, почему эта ошибка является фатальной? Я бы с удовольствием кидал исключение в этом случае и ловил бы ее для последующей обработки. Почему она фатальная? Почему мне навязывается определенное поведение моей собственной программы, и я не могу никак на это повлиять? Разве С++ не про гибкость и про то, что язык повернут лицом к программисту? Хотя...
Ну че ты как детсадовец, перегрузи себе там деление (или сделай std::div std::mod) и бросай исключения. Хотя вон уже есть какая-то питушня подобная:
Хотя надо еще для всяких плавучих и bigint, bigfloat питухов обобщить, а еще комплексных, кватернионов и прочих гиперкомплексных, итд. Чтоб было куча шаблоноговна для этого, которое будет собираться дольше, чем наступит тепловая смерть вселенной.
> Разыменование нулевого указателя. Сразу вспоминается Java, там есть NullPointerException, который можно обработать. В библиотеке Poco есть тоже NullPointerException! Так почему разработчики стандарта с упорством глухонемого повторяют одну и ту же мантру?
Ну так а хули, в C++ разве еще не сделали std::pointer (без всяких smart) который бы бросал исключения при разыменовании нуля? Так сделай
> Обработка ошибок — это не цель. Всякий раз, когда мы говорим про обработку ошибок, мы сразу приходим в тупик. Потому что это — способ достижения цели. А исходная цель — сделать наш софт надежным, простым и понятным. Именно такие цели надо ставить и всегда их придерживаться. А обработка ошибок — это фуфел, который не стоит обсуждения. Хочется кинуть исключение — да на здоровье! Вернул ошибку — молодец! Хочется монадку? Поздравляю, ты создал иллюзию продвинутости, но только в собственной башке (^4).
Вот это одобряю. Понасоздавали себе каких-то ебанутых абстракций на своем говноязычке. И это программисты? Говно какое-то
bormand 20.10.2018 18:43 # 0
Разве там фатальность гарантируется? Вроде просто UB...
j123123 20.10.2018 18:44 # +1
https://habr.com/company/infopulse/blog/338812/
Поэтому я за ассемблер - там UB может быть только в работе процессора, если выполнить недокументированную инструкцию
bormand 20.10.2018 18:49 # +1
j123123 20.10.2018 18:33 # 0
guest8 20.10.2018 18:33 # −999
j123123 21.10.2018 03:15 # 0
Elvenfighter 20.10.2018 20:22 # 0
j123123 21.10.2018 02:51 # 0
guest8 21.10.2018 02:53 # −999
guest8 21.10.2018 03:25 # −999
guest8 21.10.2018 03:31 # −999
guest8 21.10.2018 05:21 # −999
guest8 21.10.2018 12:46 # −999
OBEH 21.10.2018 13:20 # 0
666_N33D135 21.10.2018 14:38 # +3
guest8 21.10.2018 15:16 # −999
guest8 21.10.2018 15:19 # −999
guest8 21.10.2018 15:28 # −999
guest8 23.10.2018 23:35 # −999
roman-kashitsyn 20.10.2018 20:52 # 0
[1] http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p1063r0.pdf
j123123 21.10.2018 06:21 # +3
guest8 21.10.2018 10:49 # −999
bormand 21.10.2018 06:21 # +3
roman-kashitsyn 21.10.2018 16:14 # 0
Это не страшно, у нас тогда только одно в стайлгайде разрешат. Лишь бы мелкомягкие только своё говно (которое, как всегда, работает только для одного конкретного случая) не протолкнули.
bormand 21.10.2018 12:28 # 0
guest8 21.10.2018 12:39 # −999
666_N33D135 21.10.2018 15:15 # 0
j123123 21.10.2018 15:52 # 0
j123123 21.10.2018 16:01 # +1
Есть еще такая хрень: https://gcc.gnu.org/onlinedocs/gcc/Return-Address.html
> When inlining the expected behavior is that the function returns the address of the function that is returned to. To work around this behavior use the noinline function attribute.
roman-kashitsyn 21.10.2018 16:27 # +1
Недавно смотрел презентацию от SPJ про Linear Haskell.
Так вот, линейные типы не дружат с исключениями! Зачем весь этот геммор с трекингом доказательств времён жизни, если в любой момент может из ниоткуда вылететь исключение и все твои доказательства коту под хвост?
Вот поэтому в "Rust" паника вместо исключений и явные объекты ошибок.
OBEH 21.10.2018 17:07 # −1
j123123 21.10.2018 17:09 # 0
Если ты пол часа потратил на написание некоторой программы, решил сохранить ее на жесткий диск, на жестком диске внезапно попался бедблок, а у тебя сохранение файла на диск реализовано через эти линейные типы, то тогда твоя программа тупо крешнется к хренам, не дав тебе ничего никуда сохранить, я правильно понимаю?
> Зачем весь этот геммор с трекингом доказательств времён жизни
https://pbs.twimg.com/media/DmWdoXwXoAEzoKN.jpg:large
roman-kashitsyn 21.10.2018 17:23 # +1
Ну что ты несёшь? Суть не в том, чтобы делать обработку ошибок через panic!, как раз наоборот — нужно использовать явные объекты ошибок и control flow.
> Gödel Incompleteness
Про totality checker слышал?
j123123 21.10.2018 17:42 # 0
http://docs.idris-lang.org/en/latest/tutorial/theorems.html#totality-checking
Note the use of the word “possibly” — a totality check can, of course, never be certain due to the undecidability of the halting problem. The check is, therefore, conservative. It is also possible (and indeed advisable, in the case of proofs) to mark functions as total so that it will be a compile time error for the totality check to fail:
CHayT 21.10.2018 17:56 # −1
roman-kashitsyn 21.10.2018 19:35 # −1
Ключевые слова. Разумеется, halting problem он решить не может. Если чекер не уверен, что твоя программа тотальна — перепиши так, чтобы он был уверен.
Если в компиляторе нет эпичного бага, то если твоя помеченная как %total функция компилируется, то она тотальна.
OBEH 21.10.2018 19:36 # −1
guest8 21.10.2018 19:52 # −999
OBEH 21.10.2018 20:02 # −1
guest8 24.10.2018 18:30 # −999
guest8 21.10.2018 20:09 # −999
guest8 21.10.2018 20:10 # −999
bormand 21.10.2018 20:43 # 0
CHayT 21.10.2018 21:55 # +3
Знал бы ты, сколько головной боли нам доставили эликсирщики, пропихнув в BEAM небольшую несовместимость в ABI... Для пыхарей-то ABI это не проблема, а вот для языков, где ноды в кластере могут друг другу замыкания пересылать...
bormand 21.10.2018 20:40 # +1
guest8 21.10.2018 21:53 # −999
real_escape_string 21.10.2018 21:58 # +1
guest8 21.10.2018 22:24 # −999
guest8 21.10.2018 22:30 # −999
JlEOHuD_Ky4Ma 21.10.2018 22:57 # −1
guest8 22.10.2018 00:51 # −999
guest8 24.10.2018 02:55 # −999
guest8 24.10.2018 12:26 # −999
guest8 24.10.2018 12:26 # −999
guest8 24.10.2018 12:27 # −999
6yJlb 24.10.2018 13:02 # 0
В J тоже есть функции по номерам:
http://www.jsoftware.com/help/dictionary/dodot.htm
http://www.jsoftware.com/help/dictionary/xmain.htm
guest8 24.10.2018 13:40 # −999
6yJlb 24.10.2018 16:05 # 0
Да, для обратных функций. В J ещё много таких функций по номеру.
Но вот самое крутое –— в J можно строить конечные автоматы:
http://www.jsoftware.com/help/dictionary/d332.htm
суёшь этому глаголу таблицу сосояний, маппинг входных данных, начальные параметры и сами данные и он парсит строку или любой массив, на каждой итереции выбирая из таблицы строку по индексу (текущее_сосояние, маппинг_текушего_елемента), в которой записаны 2 чисоа –— номер нового сосояния и код, обозначающий что сделать на этой итереции.
Я обоссался.
roman-kashitsyn 24.10.2018 17:10 # 0
6yJlb 24.10.2018 17:30 # 0
roman-kashitsyn 24.10.2018 17:40 # 0
6yJlb 24.10.2018 17:49 # 0
guest8 24.10.2018 02:51 # −999
j123123 23.10.2018 13:19 # −1
https://i.imgur.com/RVBdWEB.png
j123123 21.10.2018 17:56 # −1
Ну и правильно, вместо исключений конечно же правильней явно проверять все данные. Т.е. если ты делишь число a на число b в каком-то коде (пусть будет функция int div(int a, int b)) и если число a и число b поступают извне (из стандартного ввода или файла) и у нас функция div() потенциально может поделить на 0, то функция int div(int a, int b) должна что делать? Хмм, а давайте сделаем так... int div(int a, int_never_zero b)... Или еще запретить чтоб (a != INT_MIN) и (b != -1)
int div(int a, int b)
// CONTRACT: ( (b != 0) OR ((a != INT_MIN) AND (b != -1)) )
Получаем ЗАВИСИМЫЕ ТИПЫ! И никаких исключений. Мы просто не сможем передать в div такие значения, чтоб там была ошибка. Т.е. если у нас
int a, b;
scanf("%d %d", a, b);
то для a и b могут быть от INT_MIN до INT_MAX
и чтобы эти a b можно было пропихнуть в функцию
int div(int a, int b)
// CONTRACT: ( (b != 0) OR ((a != INT_MIN) AND (b != -1)) )
нужно пропустить их через некий фильтр, после которого бы выполнялось условие контракта!
CHayT 21.10.2018 18:04 # −1
roman-kashitsyn 21.10.2018 23:40 # 0
Кстати, SPJ сказал, что линейную систему в расте сначала реализовали, а потом взялись формализовывать. Ко всеобщему удивлению, с теоретической точки зрения там всё оказалось ОК.
Меня в растишке больше отталкивает обилие закорючек и тот факт, что коммунити на 95% состоит из фанбоев.
CHayT 22.10.2018 00:16 # 0
Если учесть, сколько было итераций с поломкой всего, перед тем как язык заморозили...
gost 21.10.2018 18:06 # 0
> нужно пропустить их через некий фильтр, после которого бы выполнялось условие контракта!
Я не понял, это хорошо или плохо?
guest8 21.10.2018 18:10 # −999
j123123 21.10.2018 18:28 # 0
Для Java есть JML(Java Modeling Language)
На основе подобных языков аннотаций можно даже суперкомпиляцию сделать, или например попробовать сделать какой-нибудь матанистый компилятор, который бы сам выводил (на основе кода!) соответствующие аннотации (контракты).
типа
int a = ( abs(random()) )%10;
// компилятор сам всунет аннотацию, что a находится в диапазоне от 0 до 9
int b = ( abs(random()) )%20 + 1;
// компилятор сам всунет аннотацию, что b находится в диапазоне от 1 до 20
int c = a/b;
// тут компилятор может суперскомпилировать деление, чтобы оно максимально быстро работало для a в диапазоне 0...9 и b 1...20, да и к тому же переменная c может принимать только такие значения, которые могут получиться от деления числа в диапазоне 0...9 на число в диапазоне 1...20 и это может использоваться для дальнейшего суперкомпилирования...
roman-kashitsyn 21.10.2018 19:24 # 0
Ты опять мимо, хоть и в тему. Проверь там своим фильтром, что место на диске не закончится, что компьютер на другом конце провода доступен, и что неблокирующее чтение не вернёт EAGAIN.
bormand 21.10.2018 19:26 # 0
j123123 22.10.2018 01:54 # 0
А в чем проблема-то? Можно просто РАСШИРИТЬ то, что может вернуть write(); Вот например есть у нас обычный write:
ssize_t write(int fd, const void *buf, size_t count);
А мы сделаем вместо возвращаемого ssize_t свой особый ssize_t_ext, который в себя и errno может включать. Т.е. возвращаемый тип ssize_t мы меняем на struct {ssize_t ret_val, int ret_errno};
и дальше можно сделать фильтр
Такого же рода фигню можно сделать для open, read и далее по списку. Заранее знать про write, что у нас не будет ошибки при вызове его с такими то аргументами мы конечно не можем (или можем, но в очень редких случаях, когда мы например пытаемся записать на диск файл размером 3 Гб, но у нас файловые системы поддерживают только файлы размером максимум 2 Гб)
j123123 22.10.2018 05:25 # +2
roman-kashitsyn 22.10.2018 20:48 # +1
> struct {ssize_t ret_val, int ret_errno};
Поздравляю, ты почти изобрёл std::expected<ssize_t, io_error>!
Ключевое отличие в том, что крестобляди опять оказались умнее тебя и догадались взять сумму типов, а не произведение (в прочем, они просто подсмотрели у функциональщиков). В переводе на PHP язык калькуляторов это tagged union Разумеется, в отличие от сишной порнографии, std::expected не даст тебе случайно забыть проверить тег.
guest8 22.10.2018 22:08 # −999
roman-kashitsyn 22.10.2018 22:11 # 0
guest8 22.10.2018 22:15 # −999
roman-kashitsyn 22.10.2018 22:19 # 0
bormand 22.10.2018 22:20 # +3
j123123 23.10.2018 07:40 # 0
Правило одно - все есть объект. Dixi. Операции композиции объектов не определены (в отличие от ФП, где композиция функций имеет смысл) из чего сразу вытекают следующие прелести:
1. Объектная декомпозиция - чёрный ящик. Тип композитного объекта не может раскрыть его составные части. Увидеть, что скрывается за абстракцией не посмотрев в код невозможно, использовать автоматику для частичной спецификации композитного объекта на основе его составных частей невозможно.
2. Создание комбинаторов объектов невозможно. В отличие от ФП, где комбинаторами являются те же функции, в ООП объекты комбинируются процедурным быдлокодом. Пытаясь вынести его в другие объекты, ты, по сути, ничего не получаешь, потому что в итоге тебе приходится комбинировать большее число объектов тем же быдлокодом.
3. Паттерны не могут быть первоклассными объектами. Следует из отсутствия комбинаторов, т.к. паттерны являются некими стандартными комбинациями объектов.
Дополнительный вброс:
1. Неконтролируемая мутабельность добавляет к этому дополнительные прелести, вроде отсутствия ссылочной прозрачности, проблем с вариантностью, еще больше усложняет автоматический вывод спецификаций.
2. Сабтайпинг изрядно усложняет систему типов, не добавляя к ней особой выразительности. Технически, сабтайпинг - это ограниченная универсальная квантификация, тайпклассы позволяют добиваться того же эффекта, только с гораздо более простым выводом типов ок, тут я могу ошибаться, у вас есть шанс поймать меня на некомпетентности, питушки!
Вывод - ООП полный фейл. Во всём. ООП создаёт некую иллюзию, что можно работать программистом нихуя при этом не зная, но вообще, во всёх вузах детям выёбывают мозг ОО-программированием. Не знаю, что бы они делали, если бы их всех поголовно не оттрахали в жопу виртуальными деструкторами. С другой стороны, если ты хоть что-то знаешь, мейнстримовые ОО-языки не дадут тебе воспользоваться своими знаниями.
guest8 23.10.2018 16:21 # −999
j123123 23.10.2018 16:34 # 0
OBEH 23.10.2018 16:36 # 0
guest8 23.10.2018 16:39 # −999
guest8 23.10.2018 16:47 # −999
OBEH 23.10.2018 16:48 # 0
guest8 23.10.2018 21:14 # −999
guest8 23.10.2018 21:16 # −999
guest8 23.10.2018 16:48 # −999
bormand 23.10.2018 18:03 # 0
guest8 23.10.2018 18:09 # −999
CJlEW 23.10.2018 18:14 # 0
guest8 23.10.2018 18:16 # −999
6yJlb 23.10.2018 18:30 # 0
Perevedi_na_PHP 23.10.2018 21:23 # 0
guest8 23.10.2018 21:24 # −999
Perevedi_na_PHP 23.10.2018 21:26 # 0
guest8 23.10.2018 21:33 # −999
j123123 23.10.2018 18:10 # 0
guest8 23.10.2018 18:15 # −999
CJlEW 23.10.2018 18:15 # 0
guest8 23.10.2018 18:05 # −999
guest8 23.10.2018 21:15 # −999
guest8 23.10.2018 22:10 # −999
roman-kashitsyn 23.10.2018 18:37 # +1
Wrong. Сокрытие деталей реализации — одна из лучших идей индустрии, придуманная задолго до ООП (Алан Перлис?)
Coq видел? Прячем детали реализации в модуле, из модуля наружу торчат теоремы, описывающие семантику реализации.
> Сабтайпинг изрядно усложняет систему типов, не добавляя к ней особой выразительности.
Тот сабтайпинг, который в ООП — да.
Если ты спросишь более-менее адекватного хачкелиста, какая основная проблема хачкеля, он скорее всего скажет тебе, что хочет нормальные записи с Row Polymorphism (это, конечно, не сабтайпинг, но рядом). Это нормально работает только в языке с полностью иммутабельными структурами.
Вообще, в хачкеле одна из самых унылых систем для работы с записями за всю историю человечества. Если бы они просто скопировали один-в-один то, что было в Standard ML, было бы в тыщу раз лучше.
> ООП полный фейл
Я давно об этом говорю, а дедушка Степанов (тот самый, который STL написал, ну совсем не ООП-шный) об этом уже лет двадцать назад вещал.
guest8 23.10.2018 19:59 # −999
roman-kashitsyn 23.10.2018 23:42 # 0
Ты у меня что-то непонятное спрашиваешь. В чём дело?
Записи в Хаскеле говно, даже в C++ лучше. Ни Хиндли, ни даже Милнер этого не исправят.
> это ООП или нет?
Проблема в том, что никто толком не может сказать, что такое ООП. Я бы сказал, что ООП в твоём примере и не пахнет, обычный Abstract Data Type, такое хоть в паскале, хоть в сишке делали почти 50 лет назад, когда про ООП ещё никто не слышал.
Кмк, ключевой момент "ООП" — открытая рекурсия. В твоём примере её нет.
guest8 23.10.2018 23:50 # −999
roman-kashitsyn 23.10.2018 23:56 # 0
нет. тут же нет никакого «полиморфизма».
> Как же можно сказать что нечто говно, если вы даже не можете дать этому определения?
Ну если адепты ООП обосрались и не могут дать ему нормального формального определения, сосут свою Жабу и лапочут только что-то неразборчиво "инкапсуляция... наследование... полиморфизм...", то я-то что могу поделать?
В «Common Lisp», например, своё представление об ООП, там в стандарте написано, что такое «ООП». ООП в «Common Lisp» сделано хорошо, годно.
guest8 24.10.2018 00:04 # −999
j123123 23.10.2018 19:23 # 0
Данная идея настолько банальна, что я, увы, не могу назвать это изобретением. Меня больше удивляет, что для такой банальной веши понадобилось написать шаблонов вперемешку с констэкспрами на 2277 строк
> Ключевое отличие в том, что крестобляди опять оказались умнее тебя и догадались взять сумму типов, а не произведение (в прочем, они просто подсмотрели у функциональщиков). В переводе на PHP язык калькуляторов это tagged union
>struct {
> enum { RESULT, ERROR } tag;
> union { ssize_t result; int error; } value;
>};
А какой смысл в tag, если сам ssize_t result при ошибке уже нам сигнализирует об ошибке своим значением -1? И тогда можно уже при ssize_t == -1 доставать errno и смотреть его значение. Вот если бы result исполнял исключительно функцию возврата того, сколько там байт записалось, ну типа:
- другое дело.
roman-kashitsyn 23.10.2018 23:34 # 0
Ну так ssize_t это сам по себе костыль, который нужен для сигнализации ошибки.
В нормальных высокоуровневых языках функция возвращает либо полноценное значение, либо значение "ошибка", содержащее тип ошибки и детальное описание.
Но тебе, конечно, нравится пердолиться и собирать детали из минус единиц, errno, и прочего говна вроде strerror. Хотя мне сдаётся, что ты нормального кода для обработки ошибок и не пишешь вовсе.
> 2277 строк
Да там одни оптимизации и метошаблонная питушня. Я на предыдущей работе писал Expected<T> (вторым типом всегда был expection_ptr), там строк 300 от силы было вместе с документацией.
j123123 24.10.2018 05:21 # 0
А так лучше?
> В нормальных высокоуровневых языках функция возвращает либо полноценное значение, либо значение "ошибка"
Это не свойство языка, это свойство конкретного API, в данном случае:
Сделай другое API - будет тебе структурка с ошибкой и значением раздельно.
> Но тебе, конечно, нравится пердолиться и собирать детали из минус единиц, errno, и прочего говна вроде strerror.
На самом деле нет. Но мне еще меньше нравится пердолиться с такой убогой и кривой сишконадстройкой, как C++.
> Я на предыдущей работе писал Expected<T> (вторым типом всегда был expection_ptr), там строк 300 от силы было вместе с документацией.
Это тоже очень дохрена для такой примитивной фигни. В нормальных языках такое должно уклаываться максимум в 50-60 строк от силы.
j123123 24.10.2018 05:49 # 0
Посоветуй нормальный код для обработки ошибок на микроконтроллере без MMU и с примитивной ОС уровня FreeRTOS когда malloc вернул -1 внутри цикла в каких-то ебенях, например в коде mp3 кодека или TCP/IP стеке.
bormand 24.10.2018 07:30 # 0
j123123 24.10.2018 08:33 # 0
Это не я делаю что-то не так. Это проблема сторонних библиотек, в которых этот malloc юзается, которые не писались с расчетом на то, что их засунут в контроллер. Т.е. по-хорошему это всё надо переделывать на статическую память. То же самое касается например алгоритмов эхоподавления, выдранных из WebRTC и еще куча подобного говна.
> Да и tcp/ip стек без malloc посреди работы вполне обходится.
Ну вообще есть такая хрень https://en.wikipedia.org/wiki/UIP_(micro_IP) но с ограничениями:
В отличие от lwIP, uIP оптимизирован с точки зрения ресурсов памяти. lwIP использует динамически выделяемую память (кучу) для работы с сетевыми данными и информацией о соединениях. В uIP дескрипторы соединений создаются на этапе компиляции, а обмен сетевыми данными ведется через специальный статический буфер. Вследствие такой оптимизации uIP не поддерживает некоторые возможности TCP/IP стека, например сборку фрагментированных IP пакетов, алгоритм Нейгла, восстановление правильной последовательности пакетов, несколько пакетов на один ACK и т.п. Проблема резервного хранения неподтвержденных приемной стороной данных вынесена из uIP и возложена на пользователя стека.
bormand 24.10.2018 08:48 # 0
> сборку фрагментов
У них вообще буфера нету на сокетах, сразу стримят данные в юзерский коллбек?
j123123 24.10.2018 09:04 # 0
http://microsin.net/programming/arm/inside-the-uip-stack.html
Стек uIP использует один глобальный буфер, размер которого конфигурируется на базе максимального поддерживаемого размера пакета для входящих и исходящих пакетов (см. uip-master\unix\uip-conf.h, макроопределение UIP_CONF_BUFFER_SIZE). Поэтому приложение должно обработать пришедший пакет до того, как придет следующий пакет, или приложение может копировать данные пакета в свой собственный буфер, чтобы его обработать позже. Приходящие данные не будут сохранены в буфер пакета, пока приложение не обработает уже имеющиеся данные в буфере.
Оригинал на английском: http://www.drdobbs.com/inside-the-uip-stack/184405971
roman-kashitsyn 21.10.2018 19:28 # 0
Нет, не получаем. Получаем refinement types, а не dependent types. Иди учи матчасть.
j123123 22.10.2018 03:26 # 0
Ну хз, по-моему это те же яйца, только в профиль.
http://www.cse.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf
> Dependent types are types that depend on elements of other types. An example is the type $A^n$ of vectors of length n with components of type A.
Ну так у меня тоже одни типы зависят от других. Фильтры это фактически функции, которые имеют некоторую область определения и область значения. Ну короче. https://en.wikipedia.org/wiki/Bijection,_injection_and_surjection
Ну например:
int32_t b = random(); // b может принимать значение от INT32_MIN до INT32_MAX. Это тип переменной b
int64_t b2 = abs(b); // b_2 принимает значения от 0 до max( abs(INT32_MIN), INT32_MAX ). Тип b2 зависит от значения b. Вот тебе и зависимый тип. Это сюръективное отображение множества значений, которые может принимать переменная b.
int64_t b_b2 = b + b2; // ну тут тип b_b2 ЗАВИСИТ от типа b и b2. И можно доказать, что этот тип может быть 0 (когда b <= 0) или 2*b (тогда, когда b > 0). Ну и из этого следует, что b_b2 всегда будет положительным или нулем.
И если потом у нас будет некая функция, которая принимает только положительное число или 0, например функция sqrt(a)
// CONTRACT (a >= 0)
то вот эту переменную b_b2 туда вполне можно пропихнуть, т.к. она не может быть отрицательной.
Чем же вся описанная мной хрень отличается от зависимых типов?
roman-kashitsyn 22.10.2018 21:00 # 0
Нет.
> Тип b2 зависит от значения b. Вот тебе и зависимый тип.
Нет. Тип b2 это int64_t. b2 можно засунуть в любое место, где требуется int64_t.
Refinement type = базовый тип (int64_t, к примеру) + предикат, ограничивающий возможные значения. b2 не может вдруг стать строкой для некоторых значений b.
Dependent type = тип, параметризованный значением. В системе с зависимыми типами ты можешь сказать, что b2 это строка для b == 0 и вектор флотов для b == 1.
Ключевое различие в том, что системы с refinement types имеют ограничения на возможные предикаты, предикаты записываются в каких-нибудь комментариях и требуют что-то вроде внешнего SAT-солвера, который пытается автоматически проверить твои утверждения.
В системах с dependent types доказательства являются объектами первого рода, всё проверяется обычным компилятором при каждой компиляции, никаких ограничений на предикаты нету, но пердолится с доказательствами надо самому. Ну и все функции на типах и доказательства, как правило, должны быть тотальными.
Оптимум, как всегда, где-то посередине, люди уже скрестили бульдога и носорога, см. язык F*.
j123123 23.10.2018 12:34 # 0
Нет, если у нас будет функция, которая принимает int64_t который обязательно должен быть нечетным и не нулем (хотя ноль часто считают четными числом btw.), у нас будет ошибка компиляции, потому что b2 может быть только четным или нулем. А еще мы знаем что b2 == |b| и это знание может быть использовано, если мы передаем b и b2 в какую-то функцию.
> Ключевое различие в том, что системы с refinement types имеют ограничения на возможные предикаты, предикаты записываются в каких-нибудь комментариях и требуют что-то вроде внешнего SAT-солвера, который пытается автоматически проверить твои утверждения.
Вообще-то все эти педиканты можно опустить. Точнее, вместо предикатов может быть история вычислений (dataflow) и она может выводиться из самого кода. Ну типа, мы прочитали из стандартного ввода некое число, рассматривать его можно как число, которое может быть каким угодно (никакие контракты и предикаты не запрещают пользователю ввести любую хуиту в качестве входных данных). Пусть это будет число с типом (int32_any).
Потом мы делаем с ним операцию деления на два:
- и у нас уже тип, который описывается иначе:
((int32_any) int32div 2). Это уже другой тип, область допустимых значений у него уже, чем у изначального (int32_any). А потом мы можем еще и умножить опять на 2 - получим
(((int32_any) int32div 2) int32mul 2).
Для этого типа мы еще можем сказать, что он всегда делится на 2 без остатка.
...
j123123 23.10.2018 12:34 # 0
А если мы будем создавать новые переменные, и у нас все переменные - константы(иммутабельны):
и они будут жить в одной области видимости, то тип a_2 будет описываться через a, тип a_3 будет описываться через тип a_2. И если время жизни типа a_2 закончится раньше времени жизни типа a_3, то тип a_3 мы можем выразить напрямую через тип a, воспользовавшись встроенной системой символьных вычислений для дедукции типа.
И если мы передаем тип a и a_3 куда-нибудь в функцию int func(a, b), и функция требует |a| >= |b| (это необязательно задавать предикатами, это может выводиться из кода самой функции) то все тайпчекнется
OBEH 23.10.2018 12:36 # −1
j123123 23.10.2018 12:38 # 0
> Dependent type = тип, параметризованный значением. В системе с зависимыми типами ты можешь сказать, что b2 это строка для b == 0 и вектор флотов для b == 1.
gost 23.10.2018 18:31 # 0
6yJlb 23.10.2018 18:33 # 0
guest8 21.10.2018 17:30 # −999
roman-kashitsyn 21.10.2018 19:38 # +1
Perevedi_na_PHP 23.10.2018 21:28 # 0
guest8 23.10.2018 22:20 # −999
guest8 23.10.2018 22:21 # −999
guest8 23.10.2018 22:52 # −999
bormand 23.10.2018 22:52 # 0
CHayT 23.10.2018 22:54 # 0
roman-kashitsyn 23.10.2018 23:48 # 0
guest8 23.10.2018 22:56 # −999
Perevedi_na_PHP 23.10.2018 22:58 # 0
guest8 23.10.2018 22:59 # −999
bormand 23.10.2018 22:59 # 0
guest8 23.10.2018 23:03 # −999
bormand 23.10.2018 23:10 # 0
На работе - в студии. Ну и в NP++ всякую мелкую скриптушню или конфиги. Так то няшный редактор.
А дома на венде я давно ничего не писал, я туда только играться в osu хожу.
guest8 23.10.2018 23:16 # −999
roman-kashitsyn 23.10.2018 23:22 # 0
за полиномиальное время.
bormand 23.10.2018 23:46 # 0
Одно время пытался его юзать, но вообще не зашло. Для редактора - слишком сложно, для IDE - слишком убого. А разный experience меня никогда не напрягал.
guest8 23.10.2018 23:53 # −999
bormand 24.10.2018 00:14 # 0
Под мелочь - mcedit да gedit, лол.
guest8 24.10.2018 00:16 # −999
bormand 24.10.2018 00:21 # 0
Не. Он же платный, а qt creator с крестами вполне справляется.
guest8 24.10.2018 00:23 # −999
OBEH 24.10.2018 00:30 # 0
guest8 24.10.2018 00:34 # −999
guest8 24.10.2018 00:36 # −999
guest8 24.10.2018 00:37 # −999
guest8 24.10.2018 00:38 # −999
guest8 24.10.2018 00:38 # −999
bormand 24.10.2018 00:42 # 0
Ну надо же куда-то утилизировать 32 гига оперативки.
guest8 24.10.2018 00:44 # −999
roman-kashitsyn 24.10.2018 00:44 # 0
Именно поэтому я за «Emacs»
guest8 24.10.2018 02:11 # −999
roman-kashitsyn 24.10.2018 08:57 # 0
Desktop 24.10.2018 10:07 # 0
roman-kashitsyn 24.10.2018 00:34 # 0
YouCompleteMe, например.
На проектах приличного размера всё это превращается в тыкву, как, впрочем, и CLion (как минимум раньше, сейчас ХЗ).
j123123 24.10.2018 05:28 # 0
Хорошо что есть LISP
bormand 24.10.2018 00:32 # 0
Только кошачьи ушки, ня ^_^
j123123 24.10.2018 05:36 # 0
Это жабаговно уже научилось не сжирать 8 гигов оперативки на хелловорде? Оправдана ли покупка этого жабаговна, если я пишу код исключительно на Си, и мне нахер не нужны всякие говнокостыли для автокомплита всякой крестовой поебени с неймспейсами и шаблонами, рефакторинга классов и тому подобной хуйни (хотя ясен хер, что я б этой хуйней и бесплатно под GPLv3 пользоваться не стал бы)? Или может они выпустили особую урезанную версию под Си, которая стоит дешевле или вообще бесплатна (как community edition) ?
guest8 24.10.2018 17:12 # −999
guest8 24.10.2018 00:28 # −999
Elvenfighter 22.10.2018 23:57 # 0
STL же, std::goto<T>
default 24.10.2018 11:15 # 0
OBEH 24.10.2018 11:43 # 0