1. C++ / Говнокод #25005

    +1

    1. 1
    2. 2
    3. 3
    4. 4
    5. 5
    6. 6
    7. 7
    8. 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

    Комментарии (174) RSS

    • https://habr.com/post/426971/ вот еще типа ответ:

      > Деление на 0. Интересно, почему эта ошибка является фатальной? Я бы с удовольствием кидал исключение в этом случае и ловил бы ее для последующей обработки. Почему она фатальная? Почему мне навязывается определенное поведение моей собственной программы, и я не могу никак на это повлиять? Разве С++ не про гибкость и про то, что язык повернут лицом к программисту? Хотя...

      Ну че ты как детсадовец, перегрузи себе там деление (или сделай std::div std::mod) и бросай исключения. Хотя вон уже есть какая-то питушня подобная:
      https://docs.microsoft.com/ru-ru/cpp/windows/safeint-functions?view=vs-2017

      Хотя надо еще для всяких плавучих и bigint, bigfloat питухов обобщить, а еще комплексных, кватернионов и прочих гиперкомплексных, итд. Чтоб было куча шаблоноговна для этого, которое будет собираться дольше, чем наступит тепловая смерть вселенной.

      > Разыменование нулевого указателя. Сразу вспоминается Java, там есть NullPointerException, который можно обработать. В библиотеке Poco есть тоже NullPointerException! Так почему разработчики стандарта с упорством глухонемого повторяют одну и ту же мантру?

      Ну так а хули, в C++ разве еще не сделали std::pointer (без всяких smart) который бы бросал исключения при разыменовании нуля? Так сделай

      > Обработка ошибок — это не цель. Всякий раз, когда мы говорим про обработку ошибок, мы сразу приходим в тупик. Потому что это — способ достижения цели. А исходная цель — сделать наш софт надежным, простым и понятным. Именно такие цели надо ставить и всегда их придерживаться. А обработка ошибок — это фуфел, который не стоит обсуждения. Хочется кинуть исключение — да на здоровье! Вернул ошибку — молодец! Хочется монадку? Поздравляю, ты создал иллюзию продвинутости, но только в собственной башке (^4).

      Вот это одобряю. Понасоздавали себе каких-то ебанутых абстракций на своем говноязычке. И это программисты? Говно какое-то
      Ответить
      • > Почему она фатальная
        Разве там фатальность гарантируется? Вроде просто UB...
        Ответить
        • Ну, никто ж не гарантирует что UB тебе не отформатирует жесткий диск, верно? А отформатировать жесткий диск это очень даже фатально

          https://habr.com/company/infopulse/blog/338812/

          Поэтому я за ассемблер - там UB может быть только в работе процессора, если выполнить недокументированную инструкцию
          Ответить
          • Ну суть в том, что я не даже могу положиться на фатальность этой ошибки. На какой-нибудь платформе додумаются забить на неё и тупо вернут 0...
            Ответить
    • Кстати вот интересно, почему std::longjmp есть, а std::setjmp нет (есть только обычный setjmp) ?
      Ответить
    • показать все, что скрытоvanished
      Ответить
      • Если у тебя деление на ноль произошло в каких-то вычислениях, а данные для этих вычислений пришли извне (типа вот написал ты консольный калькулятор, кто-то попробовал поделить на ноль в нем) то наверно падать при этом не надо: надо просто сообщить что делить на 0 нельзя.
        Ответить
    • C++ дает тебе свободу выбора. А что именно выбирать -- пусть решает твой code style.
      Ответить
    • Если запилят гугловые корутины[1], которые по сути монадический сахарок завозят, вообще мякотка будет.

      [1] http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p1063r0.pdf
      Ответить
      • Ничего не понимаю… И это программисты. Говно какое-то, пидоры, блядь. ОС им дала треды — используй, используй треды! Блядь... Не хочу, хочу жрать говно! Что такое? Это многопоточность? Это многопоточность?! Суки. Мудачьё. Программисты! Корутины нацепили, говно жрут — говнокодеры, блядь, ёбаные…
        Ответить
      • Будет забавно, если оба предложения про корутины в стандарт затащат. В лучших традициях крестов.
        Ответить
        • > оба предложения про корутины в стандарт затащат

          Это не страшно, у нас тогда только одно в стайлгайде разрешат. Лишь бы мелкомягкие только своё говно (которое, как всегда, работает только для одного конкретного случая) не протолкнули.
          Ответить
    • Ещё SEH на винде.
      Ответить
      • показать все, что скрытоvanished
        Ответить
      • SEH на винде не является частью стандарта C++.
        Ответить
      • А так вообще, если подойти к вопросу творчески и не ограничивать себя каким-то там официальным стандартом C++, можно на ассемблерных вставках нахреначить свои исключения. Можно ассемблерной вставкой менять стекпоинтер, и вообще творить всякую такую хуйню
        Есть еще такая хрень: 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.
        Ответить
    • исключения не нужны.

      Недавно смотрел презентацию от SPJ про Linear Haskell.

      Так вот, линейные типы не дружат с исключениями! Зачем весь этот геммор с трекингом доказательств времён жизни, если в любой момент может из ниоткуда вылететь исключение и все твои доказательства коту под хвост?

      Вот поэтому в "Rust" паника вместо исключений и явные объекты ошибок.
      Ответить
      • Поэтому я за "PHP" - ставишь "error_reporting(0)" и интерпретатор не ебёт мозги нескончаемыми "хуярнингами", в отличие от влажной "Java".
        Ответить
      • > Так вот, линейные типы не дружат с исключениями!

        Если ты пол часа потратил на написание некоторой программы, решил сохранить ее на жесткий диск, на жестком диске внезапно попался бедблок, а у тебя сохранение файла на диск реализовано через эти линейные типы, то тогда твоя программа тупо крешнется к хренам, не дав тебе ничего никуда сохранить, я правильно понимаю?


        > Зачем весь этот геммор с трекингом доказательств времён жизни

        https://pbs.twimg.com/media/DmWdoXwXoAEzoKN.jpg:large
        Ответить
        • > Если ты пол часа потратил на написание некоторой программы, решил сохранить ее на жесткий диск, на жестком диске внезапно попался бедблок, а у тебя сохранение файла на диск реализовано через эти линейные типы, то тогда твоя программа тупо крешнется к хренам, не дав тебе ничего никуда сохранить, я правильно понимаю?


          Ну что ты несёшь? Суть не в том, чтобы делать обработку ошибок через panic!, как раз наоборот — нужно использовать явные объекты ошибок и control flow.

          > Gödel Incompleteness

          Про totality checker слышал?
          Ответить
          • > Про totality checker слышал?

            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:
            Ответить
            • Там говорится про halting problem. Если отсутствие исключений тебя интересует исключительно в неблагородных целях (ресурсы почистить после успешного выполнения функции), то _зависание_ этой функции тебя не особо волнует, лол. Доказательство отсутствия несматченных паттернов для алгебраических типов эквивалентно доказательству тотальности не-рекурсивных функций, и может быть тривиально автоматизированно. Только это не totality checker в классическом смысле. Видимо Роман-сан об этом говорит.
              Ответить
            • > The check is, therefore, conservative.

              Ключевые слова. Разумеется, halting problem он решить не может. Если чекер не уверен, что твоя программа тотальна — перепиши так, чтобы он был уверен.

              Если в компиляторе нет эпичного бага, то если твоя помеченная как %total функция компилируется, то она тотальна.
              Ответить
          • > Суть не в том, чтобы делать обработку ошибок через panic!, как раз наоборот — нужно использовать явные объекты ошибок и control flow.

            Ну и правильно, вместо исключений конечно же правильней явно проверять все данные. Т.е. если ты делишь число 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)) )

            нужно пропустить их через некий фильтр, после которого бы выполнялось условие контракта!
            Ответить
            • Ну примерно поэтому я крайне скептично смотрю на растишку. Он построен на автоматических статических доказательствах, которые гарантированно обосрутся; и вместо того чтобы дать юзеру возможность убрать эту кучу руками, раст предоставляет только возможность замести её под ковёр.
              Ответить
              • > я крайне скептично смотрю на растишку

                Кстати, SPJ сказал, что линейную систему в расте сначала реализовали, а потом взялись формализовывать. Ко всеобщему удивлению, с теоретической точки зрения там всё оказалось ОК.

                Меня в растишке больше отталкивает обилие закорючек и тот факт, что коммунити на 95% состоит из фанбоев.
                Ответить
                • > Ко всеобщему удивлению, с теоретической точки зрения там всё оказалось ОК.
                  Если учесть, сколько было итераций с поломкой всего, перед тем как язык заморозили...
                  Ответить
            • > Получаем ЗАВИСИМЫЕ ТИПЫ!
              > нужно пропустить их через некий фильтр, после которого бы выполнялось условие контракта!
              Я не понял, это хорошо или плохо?
              Ответить
            • Кстати вот, язык аннотаций ACSL (ANSI/ISO C Specification Language) из Frama-C https://frama-c.com/download/acsl-tutorial.pdf из Frama-C (логика Хоара)
              Для 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 и это может использоваться для дальнейшего суперкомпилирования...
              Ответить
            • > вместо исключений конечно же правильней явно проверять все данные.

              Ты опять мимо, хоть и в тему. Проверь там своим фильтром, что место на диске не закончится, что компьютер на другом конце провода доступен, и что неблокирующее чтение не вернёт EAGAIN.
              Ответить
              • Такие программы нинужны, поэтому конпелятор просто их отвергнет.
                Ответить
              • > Проверь там своим фильтром, что место на диске не закончится, что компьютер на другом конце провода доступен, и что неблокирующее чтение не вернёт EAGAIN.

                А в чем проблема-то? Можно просто РАСШИРИТЬ то, что может вернуть 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};

                и дальше можно сделать фильтр

                size_t a;
                {
                  ssize_t_ext a_ext = write(...);
                
                  if( a_ext.ret_val == -1) // ФИЛЬТР
                  {
                    switch (a_ext.ret_errno)
                    ... // error handle
                    return -1;
                  }
                  else
                  {
                    a = a_ext.ret_val; // all OK, write successful
                  }
                }
                do other stuff...


                Такого же рода фигню можно сделать для open, read и далее по списку. Заранее знать про write, что у нас не будет ошибки при вызове его с такими то аргументами мы конечно не можем (или можем, но в очень редких случаях, когда мы например пытаемся записать на диск файл размером 3 Гб, но у нас файловые системы поддерживают только файлы размером максимум 2 Гб)
                Ответить
                • int pid;
                  
                    switch(pid=fork())
                    {
                    case -1:
                      perror("fork");
                      exit(1);
                    case 0:
                      // CHILD
                      size_t a;
                      {
                        ssize_t_ext a_ext = write(...);
                  
                        if( a_ext.ret_val == -1) // ФИЛЬТР
                        {
                          switch (a_ext.ret_errno)
                          // ... error handle
                          kill(child_pid); // пропаганда суицида
                        }
                        else
                        {
                          a = a_ext.ret_val; // all OK, write successful
                          kill(parent_pid);  // МУХАХАХА!
                          return a;
                        }
                      }
                  
                    default:
                      // PARENT
                      wait(child_pid);
                      fprintf(stderr, "file write failed!\n");
                      fprintf(stderr, "My child died :(\n");
                      // ...
                    }
                  Ответить
                • > Можно просто РАСШИРИТЬ то, что может вернуть write()
                  > struct {ssize_t ret_val, int ret_errno};

                  Поздравляю, ты почти изобрёл std::expected<ssize_t, io_error>!

                  Ключевое отличие в том, что крестобляди опять оказались умнее тебя и догадались взять сумму типов, а не произведение (в прочем, они просто подсмотрели у функциональщиков). В переводе на PHP язык калькуляторов это tagged union
                  struct {
                    enum { RESULT, ERROR } tag;
                    union { ssize_t result; int error; } value;
                  };
                  Разумеется, в отличие от сишной порнографии, std::expected не даст тебе случайно забыть проверить тег.
                  Ответить
                  • показать все, что скрытоvanished
                    Ответить
                    • > но может быть у них и Maybe есть?
                      https://en.cppreference.com/w/cpp/utility/optional
                      Ответить
                      • показать все, что скрытоvanished
                        Ответить
                        • удачи
                          Ответить
                        • > Буду крестовиком

                          Правило одно - все есть объект. Dixi. Операции композиции объектов не определены (в отличие от ФП, где композиция функций имеет смысл) из чего сразу вытекают следующие прелести:

                          1. Объектная декомпозиция - чёрный ящик. Тип композитного объекта не может раскрыть его составные части. Увидеть, что скрывается за абстракцией не посмотрев в код невозможно, использовать автоматику для частичной спецификации композитного объекта на основе его составных частей невозможно.

                          2. Создание комбинаторов объектов невозможно. В отличие от ФП, где комбинаторами являются те же функции, в ООП объекты комбинируются процедурным быдлокодом. Пытаясь вынести его в другие объекты, ты, по сути, ничего не получаешь, потому что в итоге тебе приходится комбинировать большее число объектов тем же быдлокодом.

                          3. Паттерны не могут быть первоклассными объектами. Следует из отсутствия комбинаторов, т.к. паттерны являются некими стандартными комбинациями объектов.

                          Дополнительный вброс:

                          1. Неконтролируемая мутабельность добавляет к этому дополнительные прелести, вроде отсутствия ссылочной прозрачности, проблем с вариантностью, еще больше усложняет автоматический вывод спецификаций.

                          2. Сабтайпинг изрядно усложняет систему типов, не добавляя к ней особой выразительности. Технически, сабтайпинг - это ограниченная универсальная квантификация, тайпклассы позволяют добиваться того же эффекта, только с гораздо более простым выводом типов ок, тут я могу ошибаться, у вас есть шанс поймать меня на некомпетентности, питушки!

                          Вывод - ООП полный фейл. Во всём. ООП создаёт некую иллюзию, что можно работать программистом нихуя при этом не зная, но вообще, во всёх вузах детям выёбывают мозг ОО-программированием. Не знаю, что бы они делали, если бы их всех поголовно не оттрахали в жопу виртуальными деструкторами. С другой стороны, если ты хоть что-то знаешь, мейнстримовые ОО-языки не дадут тебе воспользоваться своими знаниями.
                          Ответить
                  • > Поздравляю, ты почти изобрёл std::expected<ssize_t, io_error>!

                    Данная идея настолько банальна, что я, увы, не могу назвать это изобретением. Меня больше удивляет, что для такой банальной веши понадобилось написать шаблонов вперемешку с констэкспрами на 2277 строк
                    https://github.com/TartanLlama/expected/blob/e5ec75909c415514c6f8353226c41e7925d452ce/tl/expected.hpp


                    > Ключевое отличие в том, что крестобляди опять оказались умнее тебя и догадались взять сумму типов, а не произведение (в прочем, они просто подсмотрели у функциональщиков). В переводе на 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 исполнял исключительно функцию возврата того, сколько там байт записалось, ну типа:
                    struct {
                      enum { RESULT, ERROR } tag;
                      union { size_t result; int error; } value;
                    };

                    - другое дело.
                    Ответить
                    • > А какой смысл в tag, если сам ssize_t result при ошибке уже нам сигнализирует об ошибке своим значением -1?

                      Ну так ssize_t это сам по себе костыль, который нужен для сигнализации ошибки.
                      В нормальных высокоуровневых языках функция возвращает либо полноценное значение, либо значение "ошибка", содержащее тип ошибки и детальное описание.

                      Но тебе, конечно, нравится пердолиться и собирать детали из минус единиц, errno, и прочего говна вроде strerror. Хотя мне сдаётся, что ты нормального кода для обработки ошибок и не пишешь вовсе.

                      > 2277 строк

                      Да там одни оптимизации и метошаблонная питушня. Я на предыдущей работе писал Expected<T> (вторым типом всегда был expection_ptr), там строк 300 от силы было вместе с документацией.
                      Ответить
                      • > Ну так ssize_t это сам по себе костыль, который нужен для сигнализации ошибки.
                        union write_retval
                        {
                          struct
                          {
                            size_t e:1; // signed bit is error code
                            size_t result : sizeof(ssize_t)*CHAR_BIT - 1;
                          } ok;
                          struct
                          {
                            size_t e:1; // signed bit is error code
                            size_t errno : sizeof(ssize_t)*CHAR_BIT - 1;
                          } err;
                        } __attribute__((packed));

                        А так лучше?

                        > В нормальных высокоуровневых языках функция возвращает либо полноценное значение, либо значение "ошибка"

                        Это не свойство языка, это свойство конкретного API, в данном случае:
                        CONFORMING TO
                               SVr4, 4.3BSD, POSIX.1-2001.

                        Сделай другое API - будет тебе структурка с ошибкой и значением раздельно.

                        > Но тебе, конечно, нравится пердолиться и собирать детали из минус единиц, errno, и прочего говна вроде strerror.

                        На самом деле нет. Но мне еще меньше нравится пердолиться с такой убогой и кривой сишконадстройкой, как C++.


                        > Я на предыдущей работе писал Expected<T> (вторым типом всегда был expection_ptr), там строк 300 от силы было вместе с документацией.

                        Это тоже очень дохрена для такой примитивной фигни. В нормальных языках такое должно уклаываться максимум в 50-60 строк от силы.
                        Ответить
                      • > Хотя мне сдаётся, что ты нормального кода для обработки ошибок и не пишешь вовсе.

                        Посоветуй нормальный код для обработки ошибок на микроконтроллере без MMU и с примитивной ОС уровня FreeRTOS когда malloc вернул -1 внутри цикла в каких-то ебенях, например в коде mp3 кодека или TCP/IP стеке.
                        Ответить
                        • Если у тебя malloc в mp3 кодеке - ты явно делаешь что-то не так. Да и tcp/ip стек без malloc посреди работы вполне обходится.
                          Ответить
                          • > Если у тебя malloc в mp3 кодеке - ты явно делаешь что-то не так.

                            Это не я делаю что-то не так. Это проблема сторонних библиотек, в которых этот malloc юзается, которые не писались с расчетом на то, что их засунут в контроллер. Т.е. по-хорошему это всё надо переделывать на статическую память. То же самое касается например алгоритмов эхоподавления, выдранных из WebRTC и еще куча подобного говна.

                            > Да и tcp/ip стек без malloc посреди работы вполне обходится.

                            Ну вообще есть такая хрень https://en.wikipedia.org/wiki/UIP_(micro_IP) но с ограничениями:

                            В отличие от lwIP, uIP оптимизирован с точки зрения ресурсов памяти. lwIP использует динамически выделяемую память (кучу) для работы с сетевыми данными и информацией о соединениях. В uIP дескрипторы соединений создаются на этапе компиляции, а обмен сетевыми данными ведется через специальный статический буфер. Вследствие такой оптимизации uIP не поддерживает некоторые возможности TCP/IP стека, например сборку фрагментированных IP пакетов, алгоритм Нейгла, восстановление правильной последовательности пакетов, несколько пакетов на один ACK и т.п. Проблема резервного хранения неподтвержденных приемной стороной данных вынесена из uIP и возложена на пользователя стека.
                            Ответить
                            • > последовательности пакетов
                              > сборку фрагментов
                              У них вообще буфера нету на сокетах, сразу стримят данные в юзерский коллбек?
                              Ответить
                              • > У них вообще буфера нету на сокетах, сразу стримят данные в юзерский коллбек?

                                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
                                Ответить
            • > Получаем ЗАВИСИМЫЕ ТИПЫ!

              Нет, не получаем. Получаем refinement types, а не dependent types. Иди учи матчасть.
              Ответить
              • > Нет, не получаем. Получаем refinement types, а не dependent types. Иди учи матчасть.

                Ну хз, по-моему это те же яйца, только в профиль.
                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 туда вполне можно пропихнуть, т.к. она не может быть отрицательной.

                Чем же вся описанная мной хрень отличается от зависимых типов?
                Ответить
                • > Ну хз, по-моему это те же яйца, только в профиль.

                  Нет.

                  > Тип 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*.
                  Ответить
                  • > Нет. Тип b2 это int64_t. b2 можно засунуть в любое место, где требуется int64_t.

                    Нет, если у нас будет функция, которая принимает int64_t который обязательно должен быть нечетным и не нулем (хотя ноль часто считают четными числом btw.), у нас будет ошибка компиляции, потому что b2 может быть только четным или нулем. А еще мы знаем что b2 == |b| и это знание может быть использовано, если мы передаем b и b2 в какую-то функцию.

                    > Ключевое различие в том, что системы с refinement types имеют ограничения на возможные предикаты, предикаты записываются в каких-нибудь комментариях и требуют что-то вроде внешнего SAT-солвера, который пытается автоматически проверить твои утверждения.

                    Вообще-то все эти педиканты можно опустить. Точнее, вместо предикатов может быть история вычислений (dataflow) и она может выводиться из самого кода. Ну типа, мы прочитали из стандартного ввода некое число, рассматривать его можно как число, которое может быть каким угодно (никакие контракты и предикаты не запрещают пользователю ввести любую хуиту в качестве входных данных). Пусть это будет число с типом (int32_any).
                    auto a = LOAD_STDIN(int32_any);

                    Потом мы делаем с ним операцию деления на два:
                    a = a/2;

                    - и у нас уже тип, который описывается иначе:
                    ((int32_any) int32div 2). Это уже другой тип, область допустимых значений у него уже, чем у изначального (int32_any). А потом мы можем еще и умножить опять на 2 - получим
                    (((int32_any) int32div 2) int32mul 2).
                    a = a*2;

                    Для этого типа мы еще можем сказать, что он всегда делится на 2 без остатка.
                    ...
                    Ответить
                  • ...
                    А если мы будем создавать новые переменные, и у нас все переменные - константы(иммутабельны):
                    const auto a = LOAD_STDIN(int32_any);
                    const auto a_2 = a/2;   // ((TYPEOF a) int32div 2)
                    const auto a_3 = a_2*2; // ((TYPEOF a_2) int32mul 2)

                    и они будут жить в одной области видимости, то тип a_2 будет описываться через a, тип a_3 будет описываться через тип a_2. И если время жизни типа a_2 закончится раньше времени жизни типа a_3, то тип a_3 мы можем выразить напрямую через тип a, воспользовавшись встроенной системой символьных вычислений для дедукции типа.

                    И если мы передаем тип a и a_3 куда-нибудь в функцию int func(a, b), и функция требует |a| >= |b| (это необязательно задавать предикатами, это может выводиться из кода самой функции) то все тайпчекнется
                    Ответить
                    • Блядь, как всё сложно. Поэтому я за "PHP".
                      Ответить
                  • > Refinement type = базовый тип (int64_t, к примеру) + предикат, ограничивающий возможные значения. b2 не может вдруг стать строкой для некоторых значений b.

                    > Dependent type = тип, параметризованный значением. В системе с зависимыми типами ты можешь сказать, что b2 это строка для b == 0 и вектор флотов для b == 1.

                    void *a;
                    if (we_want_int64)
                    {
                      a = alloca_aligned(sizeof(int64), alignof(int64));
                      typeset(a, int64);
                    }
                    else if (we_want_float_vector)
                    {
                      a = alloca_aligned(sizeof(float)*vectorlen, alignof(float[vectorlen]));
                      typeset(a, float[vectorlen]);
                    }
                    Ответить
        • показать все, что скрытоvanished
          Ответить
    • > почему нет std::goto?

      STL же, std::goto<T>
      Ответить
    • В плюсах будут монады?
      Ответить
      • В "PHP" нет никаких монад. Поэтому я за "PHP".
        Ответить

    Добавить комментарий