Тесты или типы? — Rust version

    Пару дней назад 0xd34df00d опубликовал здесь перевод статьи, описывающей, что можно узнать о функции в разных языках, если рассматривать её как "чёрный ящик", не используя информацию о её реализации (но, разумеется, не мешая ей пользоваться компилятору). Разумеется, получаемая информация очень сильно зависит от языка — в исходной статье рассматривались четыре примера:


    • Python — динамически типизированный, информации минимум, какие-то подсказки дают только тесты;
    • C — слабо статически типизированный, информации ненамного больше;
    • Haskell — сильно статически типизированный, с чистыми функциями, информации существенно больше;
    • Idris — язык с зависимыми типами, информации достаточно, чтобы во время компиляции доказать корректность функции.

    "Есть C, есть Haskell, а где же Rust?!" — немедленно прозвучал вопрос. Ответ — под катом.


    Напомним условие задачи:


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

    Для нетерпеливых — все рассмотренные ниже варианты можно увидеть в Rust playground.
    Погнали!


    Простой поиск


    Мы начнём с почти наивной сигнатуры, которая, по сути, от кода на C отличается только некоторыми идиоматичными элементами:


    fn foo(x: &[i32], y: i32) -> Option<usize> {
        // 10000 строк нечитаемого кода
    }

    Что мы знаем об этой функции? Ну… не так и много, на самом деле. Конечно, иметь в возвращаемых значениях Option<usize> — это гораздо лучше, чем то, что предоставлял нам C, но никакой информации о семантике функции у нас всё равно нет. В частности, нет никакой гарантии отсутствия побочных эффектов, как нет и возможности как-либо проверить ожидаемое поведение.


    Может ли ситуацию исправить грамотно написанный тест? Смотрим:


    #[test]
    fn test() {
        assert_eq!(foo(&[1, 2, 3], 2), Some(1));
        assert_eq!(foo(&[1, 2, 3], 4), None);
    }

    В общем-то, ничего нового мы не получили — все те же самые проверки мы спокойно могли проделывать и с Python (и, забегая вперёд, тесты практически ничего не дадут и в дальнейшем).


    Use the generics, Luke!


    Но разве ж это хорошо, что мы вынуждены использовать только знаковые 32-битные числа? Непорядок. Исправляем:


    fn foo<El>(x: &[El], y: El) -> Option<usize>
    where
        El: PartialEq,
    {
        // 10000 строк нечитаемого кода
    }

    Ага! Это уже кое-что. Теперь мы можем принимать срезы (slice), состоящие из любых элементов, которые мы можем сравнивать на равенство. Явный полиморфизм почти всегда лучше неявного и почти всегда лучше его отсутствия, не так ли?


    Однако такая функция может неожиданно для нас пройти вот такой тест:


    fn refl<El: PartialEq + Copy>(el: El) -> Option<usize> {
        foo(&[el], el) // should always return Some(0), right?
    }
    #[test]
    fn dont_find_nan() {
        assert_eq!(refl(std::f64::NAN), None);
    }

    Это сразу указывает на некоторый недочёт с нашей стороны, потому как по изначальной спецификации такой вызов должен был бы вернуть Some(0). Разумеется, проблема здесь из-за специфики типов с частично определённым сравнением вообще и float-ов в частности.
    Допустим, теперь мы хотим избавиться от такой проблемы, — для этого всего лишь ужесточим требования на тип El:


    fn foo<El>(x: &[El], y: El) -> Option<usize>
    where
        El: Eq,
    {
        // 10000 строк нечитаемого кода
    }

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


    Лирическое отступление: we want to go MORE generic!

    Этот вариант не имеет отношения к исходной задаче, зато является, на мой взгляд, хорошей иллюстрацией к принципу: "be liberal in what you accept, be conservative in what you do". Иначе говоря: если есть возможность без ущерба для эргономики и производительности сделать тип принимаемых значений более общим — есть смысл именно так и поступить.


    Рассмотрим вот такой вариант:


    fn foo<'a, El: 'a>(x: impl IntoIterator<Item = &'a El>, y: El) -> Option<usize>
    where
        El: Eq,
    {
        // 10000 строк нечитаемого кода
    }

    Что мы теперь знаем об этой функции? Всё то же самое, только теперь она принимает на вход не список и не срез, а какой-то произвольный объект, который можно заставить выдавать поочерёдно ссылки на объекты типа El и сравнивать их с искомым: аналогом в Java, если я правильно помню, была бы функция, принимающая Iterable<Comparable>.


    Как раньше, только строже


    Однако, допустим, гарантий, предлагаемых компилятором на уже известных этапах, нам мало. Или, скажем, мы не хотим (по тем или иным причинам) лезть в кучу, а хотим работать на стеке, — а это значит, что нам нужен массив вместо вектора, — но при этом хотим, чтобы наш код обобщался на разные размеры массива. Или мы хотим, чтобы функция была максимально оптимизирована под каждый конкретный размер входного списка.

    Короче говоря, нам нужен generic array — и в Rust уже есть пакет, предоставляющий дословно это.


    Теперь в нашем распоряжении уже такой код:


    use generic_array::{GenericArray, ArrayLength};
    
    fn foo<El, Size>(x: GenericArray<El, Size>, y: El) -> Option<usize>
    where
        El: Eq,
        Size: ArrayLength<El>,
    {
        // 10000 строк нечитаемого кода
    }

    Что мы знаем из этого кода? Что функция принимает массив некоторого фиксированного размера, отражённого в её типе (и для каждого такого размера скомпилируется независимо). Пока что это почти ничего не меняет — в конце концов, точно такие же гарантии, только не на этапе мономорфизации, а в рантайме, обеспечивал и предыдущий вариант со срезом.


    Но мы можем пойти ещё дальше.


    Арифметика уровня типов


    В исходной статье упоминались несколько гарантий, которую мы получили от Idris и не смогли получить ни от кого более. Одна из них — и, пожалуй, сама простая, потому что для неё даже не нужно писать полноценное доказательство или полноценный тест, а только чуть конкретизировать тип, — гласит, что возвращаемое значение, если оно есть (т.е. если оно не Nothing), гарантированно не будет превосходить длины входного списка.

    Казалось бы, необходимое условие для такой гарантии — наличие зависимых типов, ну, или хотя бы какого-то их подобия, и странно было бы ожидать подобного от Rust, верно?


    Встречайте — typenum. С его помощью наша функция может быть изображена вот так:


    use generic_array::{ArrayLength, GenericArray};
    use typenum::{IsLess, Unsigned, B1};
    trait UnsignedLessThan<T> {
        fn as_usize(&self) -> usize;
    }
    
    impl<Less, More> UnsignedLessThan<More> for Less
    where
        Less: IsLess<More, Output = B1>,
        Less: Unsigned,
    {
        fn as_usize(&self) -> usize {
            <Self as Unsigned>::USIZE
        }
    }
    
    fn foo<El, Size>(x: GenericArray<El, Size>, y: El) -> Option<Box<dyn UnsignedLessThan<Size>>>
    where
        El: Eq,
        Size: ArrayLength<El>,
    {
        // 10000 строк нечитаемого кода
    }

    "Что это за чёртова чёрная магия?!" — спросите вы. И будете, безусловно, правы: typenum — это та ещё чёрная магия, а попытки его хоть как-то вменяемо использовать — вдвойне.

    И тем не менее, сигнатура этой функции достаточно однозначна.


    • Функция принимает массив элементов El длины Size и один элемент типа El.
    • Функция возвращает значение Option, которое, если оно является Some,
      • представляет собой trait object, основанный на типаже UnsignedLessThan<T>, который принимает в качестве параметра тип Size;
      • в свою очередь, типаж UnsignedLessThan<T> реализован для всех типов, реализующих Unsigned и IsLess<T>, для которых IsLess<T> возвращает B1, т.е. true.

    Иначе говоря, таким образом мы написали функцию, которая гарантированно возвращает неотрицательное (беззнаковое) число, меньшее, чем исходный размер массива (вернее, конечно, она возвращает этот самый trait object, у которого мы позже должны вызвать метод as_usize, гарантированно возвращающий такое число).


    Подвохов у данного подхода ровно два:


    1. Мы можем ощутимо потерять в производительности. Если вдруг по какой-то причине такая наша функция окажется на "горячем" участке программы, постоянная необходимость в динамических вызовах может оказаться одной из самых медленных операций. Впрочем, этот недостаток вполне может быть не так значителен, как кажется, но есть и второй:
    2. Чтобы эта функция корректно скомпилировалась, нам потребуется либо фактически написать внутри неё самой доказательство корректности её работы, либо "обмануть" систему типов через unsafe. Первое слишком сложно для пятничной статьи, ну а второе — попросту жульничество.

    Заключение


    Разумеется, на практике в подобных случаях будет использоваться либо вторая реализация (принимающая срез произвольного типа), либо реализация под спойлером (принимающая итерируемый объект). Все последующие рассуждения почти наверняка не несут практического интереса и служат исключительно упражнением по работе с системой типов.


    Тем не менее, сам факт, что на системе типов Rust можно суметь эмулировать одну из особенностей заведомо более сильной системы типов Idris, на мой взгляд, достаточно показателен.

    Поделиться публикацией

    Похожие публикации

    AdBlock похитил этот баннер, но баннеры не зубы — отрастут

    Подробнее
    Реклама

    Комментарии 55

      0
      слишком сложно для пятничной статьи

      Трудно не согласиться.

        +2

        Годнота.


        Но, если я правильно понимаю, читерство :) У вас в последнем варианте размер массива так или иначе известен статически, верно?

          0
          У вас в последнем варианте размер массива так или иначе известен статически, верно?

          Совершенно верно, для GenericArray это часть типа. А в чём "читерство"?

            +5

            Ну, фишка идриса с Fin n в том, что это работает и для неизвестных в процессе компиляции n. То есть, у вас может быть код типа


            readVectFromFile : String -> IO (n ** Vect n Int)    -- (1)
            readVectFromFile = ...
            
            findIndex : Eq a => a -> Vect n a -> Maybe (Fin n)
            findIndex = ...
            
            readAndFind : IO ()
            readAndFind = do
              (n ** vec) <- readVectFromFile someFile      -- (2)
              let maybeFinIdx = findIndex 10 vec           -- (3)
              ...

            В (1) как раз магия зависимых типов — функция возвращает вектор длины n (и саму длину n), но n не известна в компилтайме.
            В (2) обычный паттерн-матчинг по зависимой паре, поэтому мы знаем, что vec — вектор длины n.
            В (3) всё вполне себе будет работать, несмотря на то, что n известен только в рантайме.


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


            То есть, я не хочу сказать, что раст плохой и негодный, это действительно очень круто, что на нём можно такое сделать (тут мне стало интересно, можно ли похожее на плюсах, хехе). Просто вопрос «будет ли это работать с данными, считанными из файла или из сети» — это такой дискриминатор между завтипами и более слабыми системами типов (правда, примитивный и не очень точный).

              0

              Кстати, спасибо, тоже интересная задача: можно ли сгенерировать GenericArray с неизвестной заранее длиной, и если да, то как его можно будет использовать: вернуть из функции, например, заведомо нельзя — точнее, можно, но только в виде trait object, — а вот передать глубже по дереву вызовов, может быть, и получится.

                +4
                Собственно, это ключевая фича зависимых типов — можно ли выражать терм-левел зависимости в типах, которые могут быть вычислены лишь во время выполнения, или нет.

                А вас не затрудник немножко разжевать это для несведующих?
                Как это происходит?

                  +7

                  Если в двух словах, то «по индукции».


                  Если чуть подробнее, то тайпчекеру неважно, какое именно значение будет в условном n в коде выше, он просто проверяет, что везде, где ожидается n, используется n, а везде, где некоторая функция f(n) — именно она. При этом конкретно в случае языков типа идриса, агды или кока некоторые хорошие свойства метатеории языка гарантируют, что все такие функции, которые могут использоваться в типах, завершимы (то есть, это не тьюринг-полный язык), и что независимо от порядка вычисления функций они дадут один и тот же ответ (конфлюэнтность, или теорема Черча-Россера). Поэтому если вдруг в типах встречается функция, её можно просто начать вычислять.


                  Если чуть формальнее, то есть правила вывода, которые позволяют индуктивно проводить тайпчекинг выражений. Выглядят примерно так (для calculus of constructions, одной из систем типов с зависимыми типами):



                  Рассказывать конкретно, что тут и как, тянет не то что на статью, а на главу-две в какой-нибудь книге, но если вы готовы потратить 20-30-100 вечеров ненапряжного чтения, чтобы в этом разобраться, то стукнитесь в личку, скину вам неплохую книгу (собственно, откуда и взята эта картинка). Если же вы хотите скорее просто попрактиковаться в написании такого кода, то рекомендую Type-driven development in Idris.


                  Дальше идёт пример, который наверняка нифига не будет понятен, потому что всё сумбурно и сжато, но тем не менее.


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


                  data Vect : (n : Nat) -> (ty : Type) -> Type where
                    Nil : Vect 0 ty
                    (::) : ty -> Vect n ty -> Vect (S n) ty

                  Тут написано две следующее:


                  1. Вектор — это такая штука, которая параметризована своей длиной (натуральным числом) и типом элементов и является типом.
                  2. Вектор можно создать при помощи конструктора Nil, и его длина будет нулём.
                  3. Вектор можно создать при помощи конструктора ::, имея уже какой-то вектор любой длины n и элемент типа ty, при этом получится вектор длины 1 + n.

                  Попробуем написать функцию суммирования двух векторов. Её тип будет


                  sumVectors : Vect n Int -> Vect n Int -> Vect n Int

                  Я специально выбираю n одним и тем же во всех трёх вхождениях, чтобы в типах указать на связь размеров входных и выходных векторов (а мог бы ещё написать appendVectors : Vect n Int -> Vect m Int -> Vect (n + m) Int, например).


                  Теперь я могу сгенерировать определение этой функции (среда разработки за меня напишет «рыбу» sumVectors xs ys = ?sumVectors_rhs, и мне нужно просто написать часть справа).


                  Идрис даёт возможность посмотреть, какие термы каких типов мне доступны в каждой точке. Например, для ?sumVectors_rhs:


                    n : Nat
                    xs : Vect n Int
                    ys : Vect n Int
                  --------------------------------------
                  sumVectors_rhs : Vect n Int

                  то есть, у меня есть n типа Nat (это длина вектора, она неявный параметр для этой функции), и xs и ys с понятными типами. Под чертой — тип того, что мне нужно произвести.


                  Логично рассмотреть варианты на то, какой конструктор использовался для создания xs. Это может быть либо Nil, либо :: (идрис достаточно умный, чтобы применять некоторые распространённые синтаксические сокращения, например, [] вместо Nil для конструкторов, имеющих подобную форму):


                  sumVectors : Vect n Int -> Vect n Int -> Vect n Int
                  sumVectors [] ys = ?sumVectors_rhs_1
                  sumVectors (x :: y) ys = ?sumVectors_rhs_2

                  Посмотрим, что нам доступно в ?sumVectors_rhs_1:


                    ys : Vect 0 Int
                  --------------------------------------
                  sumVectors_rhs_1 : Vect 0 Int

                  Здесь произошла очень важная магия. Мы рассматриваем случай, когда xs создан конструктором Nil. Но если он создан конструктором Nil, значит, n равно нулю (потому что это прямо указано в конструкторе). Значит, можно везде вместо n подставить 0. Теперь справа я могу написать ys, и это будет корректной реализацией (потому что его длина ноль), но это не так интересно. Давайте попросим идрис сделать разбить ys на случаи.


                  sumVectors : Vect n Int -> Vect n Int -> Vect n Int
                  sumVectors [] [] = ?sumVectors_rhs_3
                  sumVectors (x :: y) ys = ?sumVectors_rhs_2

                  Он сам подставил [] вместо ys, не рассматривая случай, когда ys создан при помощи ::. Почему? Ну, давайте попробуем дописать этот случай руками, добавив следующую строчку:


                  sumVectors [] (y :: ys) = ?sumVectors_rhs_3

                  Однако, у нас ничего не получится:


                  Type checking ./Sample.idr
                  Sample.idr:12:1-10:
                     |
                  12 | sumVectors [] (y :: ys) = ?sumVectors_rhs_3
                     | ~~~~~~~~~~
                  When checking left hand side of sumVectors:
                  When checking an application of Sample.sumVectors:
                          Type mismatch between
                                  Vect (1 + n) ty (Type of _ :: _)
                          and
                                  Vect 0 Int (Expected type)
                  
                          Specifically:
                                  Type mismatch between
                                          S n
                                  and
                                          0

                  Действительно, если xs создан через Nil, то n = 0, а если ys создан через ::, то n = S n' для некоторого n'. Получили противоречие, такого быть не может. Ну а справа вместо знака вопроса можно написать [].


                  Перейдём теперь ко второй ветке. Если мы аналогично попросим разбить ys, то идрис по аналогичным соображениям отбросит Nil и оставит нам только


                  sumVectors : Vect n Int -> Vect n Int -> Vect n Int
                  sumVectors [] [] = []
                  sumVectors (x :: y) (z :: w) = ?sumVectors_rhs_1

                  Посмотрим на типы:


                    x : Int
                    z : Int
                    n : Nat
                    y : Vect n Int
                    w : Vect n Int
                  --------------------------------------
                  sumVectors_rhs_1 : Vect (S n) Int

                  Логично сложить y и w рекурсивно, а потом к ним спереди приписать сумму x и z:


                  sumVectors : Vect n Int -> Vect n Int -> Vect n Int
                  sumVectors [] [] = []
                  sumVectors (x :: y) (z :: w) = (x + z) :: sumVectors y w

                  Всё.


                  Давайте теперь, наконец, прочитаем их из файла:


                  readFromFile : String -> IO (n ** Vect n Int)

                  Эта функция принимает имя файла и возвращает прочитанный из него вектор вместе с его длиной. Её я писать не буду, но там ничего принципиально нового нет, все те же идеи, к которым, правда, надо привыкнуть.


                  Теперь из двух файлов + суммирование. Давайте напишем простой и очевидно неправильный код:


                  sumFromFiles : IO ()
                  sumFromFiles = do
                    (n1 ** vec1) <- readFromFile "a.txt"
                    (n2 ** vec2) <- readFromFile "b.txt"
                    let sum = sumVectors vec1 vec2
                    print "done"

                  Компилятор ругнётся:


                  When checking an application of function Sample.sumVectors:
                          Type mismatch between
                                  (\n => Vect n Int) n2 (Type of vec2)
                          and
                                  Vect n1 Int (Expected type)
                  
                          Specifically:
                                  Type mismatch between
                                          n2
                                  and
                                          n1

                  Мы помним, что sumVectors ожидает векторы одинаковой длины, а компилятор видит, что мы передаём векторы длин n1 и n2 (и их рантайм-значение совсем неважно, даже если оно вдруг окажется совпадающим — это ещё один ключевой момент). Про это он нам и говорит: не, типа, сорян, не могу синтаксически совместить n1 и n2.


                  По факту компилятор нас заставляет выполнить проверку n1 и n2 на равенство (причём, более строгое, чем то равенство, к которому мы все привыкли) в рантайме. Для тех типов, для которых это возможно, есть тайпкласс DecEq с методом decEq:


                  *Sample> :doc decEq
                  Decidable.Equality.decEq : DecEq t => (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
                      Decide whether two elements of t are propositionally equal
                  
                      The function is Total
                  *Sample> :doc Dec
                  Data type Prelude.Basics.Dec : Type -> Type
                      Decidability. A decidable property either holds or is a contradiction.
                  
                  Constructors:
                      Yes : (prf : prop) -> Dec prop
                          The case where the property holds
                          Arguments:
                              prf : prop  -- the proof
                  
                      No : (contra : prop -> Void) -> Dec prop
                          The case where the property holding would be a contradiction
                          Arguments:
                              contra : prop -> Void  -- a demonstration that prop would be a contradiction

                  То есть, мы либо получаем доказательство того, что n1 = n2, либо доказательство того, что они не равны. Воспользуемся этой функцией:


                  sumFromFiles : IO ()
                  sumFromFiles = do
                    (n1 ** vec1) <- readFromFile "a.txt"
                    (n2 ** vec2) <- readFromFile "b.txt"
                    case decEq n1 n2 of
                         Yes prf => ?rhs_1
                         No contra => ?rhs_2
                    print "done"

                  Посмотрим на то, что нам доступно в ?rhs_1:


                    n1 : Nat
                    n2 : Nat
                    prf : n1 = n2
                    vec2 : Vect n2 Int
                    vec1 : Vect n1 Int
                    a : Type
                  --------------------------------------
                  rhs_1 : IO ()

                  Пришло время посмотреть внимательнее на тип =.


                  *Sample> :doc (=)
                  Data type (=) : (x : A) -> (y : B) -> Type
                      The propositional equality type. A proof that x = y.
                  
                      To use such a proof, pattern-match on it, and the two equal things will then need to be the same pattern.
                  
                      Note: Idris's equality type is potentially heterogeneous, which means that it is possible to state equalities between values of potentially different
                      types. However, Idris will attempt the homogeneous case unless it fails to typecheck.
                  
                      You may need to use (~=~) to explicitly request heterogeneous equality.
                      Arguments:
                          (implicit) A : Type  -- the type of the left side of the equality
                  
                          (implicit) B : Type  -- the type of the right side of the equality
                  
                  Constructors:
                      Refl : x = x
                          A proof that x in fact equals x. To construct this, you must have already shown that both sides are in fact equal.
                          Arguments:
                              (implicit) A : Type  -- the type at which the equality is proven
                  
                              (implicit) x : A  -- the element shown to be equal to itself.

                  То есть, это тип вида x = y, у которого есть один конструктор (Refl), принимающий один аргумент x и производящий значение типа x = x. Поэтому, совершенно аналогично нашей функции sumVectors выше, если мы рассмотрим возможные конструкторы этого типа (которых одна штука), то мы совершенно аналогично будем знать, что аргумент слева от знака равенства равен аргументу справа. Собственно, так как конструктор один, рассмотрение сводится к замене prf на Refl, и тогда компилятор будет знать, что n1 совпадает с n2:


                    n1 : Nat
                    vec2 : Vect n1 Int
                    vec1 : Vect n1 Int
                    a : Type
                  --------------------------------------
                  rhs_1 : IO ()

                  Вот! Теперь у нас для длин обоих векторов используется один и тот же терм, значит, они заведомо равны по длине, и можно их просуммировать.

                    +1

                    Огого! Спасибо большое за подробный ответ!
                    Не уверен, что все понял, к сожалению, очень уж синтаксис непривычный.


                    У меня есть ощущение, что что-то частично подобное можно сделать на шаблонах С++, скажем, у std::array размер — шаблонный параметр, довольно легко написать функцию, которая складывает только массивы одной длины.


                    Но вот кусок, который родит нужный класс в рантайме в зависимости от прочитанной из файла длины — вот тут сходу не получается.

                      +1
                      Но вот кусок, который родит нужный класс в рантайме в зависимости от прочитанной из файла длины — вот тут сходу не получается.

                      И не сходу с теми же гарантиями тоже не получится :)


                      Собственно, как я писал чуть выше, в этом вся разница — обязательно ли знать значения всех этих числовых параметров при компиляции или нет.

                        0

                        Благодаря twinklede получилось сделать похожее на плюсах и boost::hana. Но в синтаксис языка это не очень вписывается. Если кратко то нам надо на каждую переменную новый тип это будет немного костыльно:


                        auto x = make<source_loc()>(rand());
                        auto y = make<source_loc()>(rand());

                        Теперь у икс и игрек разные типы и раные значения. Далее в hana мы можем работать с темплейтами и типами в них как с обычным структурами данных типа set, dict, etc. Например в типе переменной будет хранится ид и множество ид других переменных которым она равна. Т.е. например auto opt_z= x.equal(y) дает нам std::option в котором кроме null (при рантайм значении x!=y) могут быть две новые переменные x1, y1 в типах которых есть отметка о равенстве. После распаковки можно будет делать static_assert(is_equal(x1, y1)).


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

                      0

                      В закладки и в планы на будущее, спасибо :)

                        0
                        data Vect: (n: Nat) -> (ty: Type) -> Type where
                        Nil: Vect 0 ty
                        (::): ty -> Vect n ty -> Vect (S n) ty

                        Я правильно понимать, что если мы уберем последнее -> Type то мы сможем объявить тайп конструктор с одной дыркой?

                          0

                          Я не уверен, что понял вопрос. Что значит «с одной дыркой»?


                          Собственно, просто убрать последнее -> Type у вас не получится, даже если не рассматривать конструкторы, это синтаксическая ошибка:


                          Type checking ./Test.idr
                          Test.idr:1:38:
                            |
                          1 | data Vect : (n : Nat) -> (ty : Type) where
                            |                                      ^
                          unexpected "wh"
                          expecting "->"

                          Что, в принципе, логично, так как синтаксис (a : B) — это П-биндер, т. е. часть Пa:B в типе Пa:B.C. От неё справа что-то просто обязано стоять.


                          Если вы теперь напишете data Vect : (n : Nat) -> Type, то это вполне легитимная запись, но вопрос в том, что вы будете делать с конструкторами.

                            0
                            Я не уверен, что понял вопрос. Что значит «с одной дыркой»?

                            Это значит что конструктору нужно передать один тип чтобы получить тип. Я взял термин из скаловой тусовки, думал он общепринят.


                            Собственно, просто убрать последнее -> Type у вас не получится, даже если не рассматривать конструкторы, это синтаксическая ошибка:

                            Я просто думал можно написать метод над тайп конструктором а не обычным типом, а-ля скаловое def Foo[F[_]]


                            Если вы теперь напишете data Vect: (n: Nat) -> Type, то это вполне легитимная запись, но вопрос в том, что вы будете делать с конструкторами.

                            Применять где-то позже, логично же :)

                              0

                              Ну я скалу совсем не знаю, она меня своими квадратными скобками пугает. А в идрисовской (да и вообще, похоже, в формально-доказательной) тусовке дырка — отсутствующий proof term, как вон вся та ерунда со знаками вопроса в комменте выше.


                              Vect — в каком-то смысле просто функция на типах, и вы там указываете её сигнатуру. -> Type в конце будет почти всегда. Напишете data Vect : Nat -> Type -> Type, будет тип данных, параметризованный числом и типом. Напишете data Vect : Type -> Type — будет тип данных, параметризованный только типом (собственно, список определяется как data List : Type -> Type).


                              Надеюсь, это хоть немного в тему того, что вы спрашивали.

                                0
                                Ну я скалу совсем не знаю, она меня своими квадратными скобками пугает.

                                Это нормально. Нужно пообвыкнуть и чуть-чуть смириться.


                                А в идрисовской (да и вообще, похоже, в формально-доказательной) тусовке дырка — отсутствующий proof term, как вон вся та ерунда со знаками вопроса в комменте выше.

                                Под дыркой имеется ввиду незакрепленный генерик. Например, в терминах сишарпа List<> — тайп-конструктор с одной дыркой, HashMap<,> — с двумя, и так далее.

                                  0

                                  По идее, (n: Nat) -> (ty: Type) -> Type — это тип с двумя дырками, получается. По крайней мере, до тех пор, пока мы не подставим конкретное число n и конкретный тип ty.

                                    +1

                                    Да, если я таки правильно понял, что такое дырка.


                                    Или в коде:


                                    Idris> :let data Vect : Nat -> Type -> Type where
                                    Idris> :t Vect
                                    Vect : Nat -> Type -> Type
                                    Idris> :t Vect 0
                                    Vect 0 : Type -> Type
                                    Idris> :t Vect 0 Int
                                    Vect 0 Int : Type
                                      0

                                      Да, оно. Понятненько, спасибо.

                                      0

                                      не совсем, тут та же разница, как между List<T> и List<>. В одном случае у нас единственный закрепленный тип T, а в другом — дырка.


                                      Типичный пример, когда это может понадобиться:


                                      def eitherMonad[E] = new Monad[Either[E, *]] {
                                        override def unit[A](a: => A): Either[E, A] = Right(a)
                                        override def flatMap[A, B](ma: Either[E, A])(f: A => Either[E, B]): Either[E, B] = ma.flatMap(f)
                                      }

                                      Обратите внимание на *. Монада это генерик от одного параметра, а мы используем тип Either с двумя. Таким образом мы делаем монаду от типа с одной дыркой, куда нужно подставить один тип (типа результата) чтобы превратить конструктор в тип.

                            0

                            Синтаксис непривычный, но фишка классная, надо вам писать статью про ФП в примерах.

                          0
                          (тут мне стало интересно, можно ли похожее на плюсах, хехе)

                          с границами известными в compile-time легко, есть уже всякие библиотеки, может даже как часть буста, например https://www.boost.org/doc/libs/1_69_0/libs/safe_numerics/doc/html/tutorial/6.html.


                          Весь интерес в том чтобы это работало в рантайм, как Вы написали ниже.

                      +1

                      Спасибо за наводку на typenum .

                        +2

                        Приятно слышать, что подобный подход может быть полезен) Сам пока что из практических применений видел только пакет nalgebra, где typenum-овские типы позволяют статически гарантировать, что операции с матрицами будут корректны (особенно перемножение).

                        0

                        А зачем Option<Box<dyn Trait>>, нельзя просто Option` вернуть?

                          0

                          Не совсем понимаю, "просто Option" — это в данном случае что?

                            0

                            Option<impl Trait> неудачное редактирование съело правильное форматирование

                              0

                              Соль в том, что Option<impl Trait> — это "Option с конкретным неназванным типом внутри". А здесь у нас на каждый вариант ответа, т.е. на каждую позицию в списке, тип будет разный.

                          0
                          > пройти тест…
                          > foo(&[std::f64::NAN], std::f64::NAN) = None

                          Все правильно. Это НЕ особенность реализации флоат. Это отличная демонтрация различия между мышлением математика и программиста. И флоат тут сделан математически правильно.
                          Для программиста флоат — набор битов. Если два набора битов совпадает — значения совпадают. Почти все баги с null связаны с таким мышлением.

                          Однако тут флоат — это абстракция с определенной реализацией. Абстракция чисел. И в этой абстракции NaN != NaN. Что и реализовано.
                            +2

                            Среди чисел нет таких, которые не были бы равны сами себе. Это так себе абстракция, математики не одобряют.


                            Флоат — это такая узкая специализация монады Maybe, где вместо одного Nothing есть с пяток разных вариантов «ошибки».

                              0
                              Флоат — это не абстракция «некоторый набор чисел» это абстракция «числового поля». Когда бесконечное поле надо обстрагировать конечной сущностью — обычно делают преобразование бесконейной линии в круг. Непомню как оно называется но на ночь искать лениво.

                              пример тут math.stackexchange.com/questions/82220/a-circle-with-infinite-radius-is-a-line
                              и тут www.quora.com/Is-there-a-bijective-function-from-a-circle-to-a-line

                              В двух словах
                              нижняя точка круга — 0
                              правая часть — положительные числа. Чем выше по кругу — тем больше
                              лувая — отрицательные
                              верхняя точка круга — символизирует положительную и отрицательную бесконечность
                                +2

                                А где там наны-то?


                                Ссылки, похоже, тут не очень релевантны, потому что круг тоже бесконечный (и равномощен прямой), да и в R, Q и прочих подобных нет элемента «бесконечность». Он, конечно, есть в нестандартном аналоге R, но давайте не будем вскрывать эту тему (и он там равен сам себе, потому что forall x. x = x принадлежит теории R, а значит и ее нестандартному расширению).


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

                            0
                            Надо прочитать оригинальную статью.

                            Но эта статья — полностью неверна в своем тезисе. Хотя и было интересно узнать про некоторые детали.

                            Все разбивается об елементарный пример. Функция которая возвращает количество елементов равных заданному имеет ту-же* сигнатуру. Поэтому без теста не обойтись.

                            * Если совсем точным — в этом варианте** сужение, так как она никогда не вернет None. Но компилятор Раста такой ошибки не найдет.
                            ** Если учесть мой первый комментарий что правильно использовать таки partialEq то сужения не будет. None будет для случая когда y!=y
                              +4
                              Поэтому без теста не обойтись.

                              Осталось научиться придумывать тесты. foo([1, 2, 3], 2) == 1 не обнаружит проблему в вашем варианте функции. Поэтому без формального доказательства не обойтись.

                                0
                                1 не надо ограничивать елементарными тестами
                                `foo([32, 16, 18, 3, 44, 3456, 3], 3)`
                                2 надо добавлять случайные тесты. Но оно работает только при строгих процессах. Когда упавшый СИ не перезапускают от лени — а каждый раз разбираются и ищут
                                3 мутационные тесты
                                  +6

                                  По первому пункту — а как понять, когда набор тестов перестал быть элементарным?


                                  А в совокупности, похоже, проще таки формальное доказательство написать.


                                  Edit: Собственно, у меня ушло примерно 15 минут, чтобы написать всю функцию и доказательство её корректности (и сходить сделать себе чай, и отредактировать комментарий):


                                  module Find
                                  
                                  import Data.Vect
                                  
                                  %default total
                                  
                                  elemToFin : (xs : Vect n a) -> Elem _ xs -> Fin n
                                  elemToFin (_ :: ys) Here = FZ
                                  elemToFin (y :: ys) (There later) = FS (elemToFin ys later)
                                  
                                  findIndex : DecEq a => a -> Vect n a -> Maybe (Fin n)
                                  findIndex x xs = case isElem x xs of
                                                        Yes prf => Just (elemToFin xs prf)
                                                        No contra => Nothing
                                  
                                  elemPrfOk : DecEq a =>
                                              (x : a) -> (xs : Vect n a) ->
                                              (elemPrf : Elem x xs) -> index (elemToFin xs elemPrf) xs = x
                                  elemPrfOk x (x :: ys) Here = Refl
                                  elemPrfOk x (y :: ys) (There later) = elemPrfOk x ys later
                                  
                                  findJustOk : DecEq a =>
                                               (x : a) -> (xs : Vect n a) ->
                                               (prf : findIndex x xs = Just idx) -> index idx xs = x
                                  findJustOk x xs prf with (isElem x xs)
                                    | Yes elemPrf = rewrite sym $ justInjective prf in elemPrfOk x xs elemPrf
                                    | No _ = absurd prf
                                  
                                  findNothingOk : DecEq a =>
                                                  (x : a) -> (xs : Vect n a) ->
                                                  (prf : findIndex x xs = Nothing) -> Not (Elem x xs)
                                  findNothingOk x xs prf y with (isElem x xs)
                                    | Yes _ = absurd prf
                                    | No contra = contra y

                                  Как там с мутационными тестами, случайными тестами и перезапуском СИ?

                                    0

                                    В поддержку этого комментария: я гарантирую, что у вас уйдет больше 15 минут на написание всех необходимых тестов + они еще и не дадут того уровня уверенности. Типы — Тесты 1:0.

                                    +1

                                    По второму пункту — эх, а мне ж хотелось сделать набросок случайно генерируемого теста, но решил, что это будет всё-таки оффтопом… Видимо, ошибся, спасибо за наводку)

                                  0
                                  >Функция которая возвращает количество елементов равных заданному имеет ту-же* сигнатуру.
                                  Число функций, имеющих такую сигнатуру, скорее всего бесконечно.

                                  >Поэтому без теста не обойтись.
                                  Мы пока только убедились, что такая сигнатура не позволяет нам судить о правильности работы функции. Ну то есть правильный вывод — что такой системы типов недостаточно. А уж нужны ли нам тесты (или там формальное доказательство) — это отдельная тема все-таки.
                                    0
                                    Число функций, имеющих такую сигнатуру, скорее всего бесконечно.

                                    Не уверен. Например, можно формально показать (но эта алгебра пока за пределами моих навыков), что функций с сигнатурой (a : Type) -> a -> a ровно одна.


                                    Я бы скорее интуитивно ожидал, что функций с сигнатурой из последнего примера конечное число (по крайней мере, в сеттинге чистого ФП).

                                      0
                                      Хм. На входе вектор и элемент. На выходе «индекс элемента». А точнее не индекс, а целое (потому что из сигнатуры этого не следует). В каком смысле такая функция одна?
                                        0
                                        В каком смысле такая функция одна?

                                        Это я про a -> a.


                                        Хм. На входе вектор и элемент. На выходе «индекс элемента». А точнее не индекс, а целое (потому что из сигнатуры этого не следует).

                                        Хм, похоже, вы правы. Достаточно рассмотреть все функции вида (n : Nat) -> Fin n (т. е. которые опираются просто на длину вектора), а их уже, похоже, бесконечное число (правда, ещё интересный вопрос в том, сколько из них вычислимы, но то такое).

                                          +1
                                          Достаточно рассмотреть все функции вида (n : Nat) -> Fin n (т. е. которые опираются просто на длину вектора), а их уже, похоже, бесконечное число (правда, ещё интересный вопрос в том, сколько из них вычислимы, но то такое).

                                          Да, собственно, и вычислимых уже счётное число, по идее: f m n = floor (n / m) для любых целых m >= 2. Любые две такие функции будут различаться как минимум в точке n = max(m1, m2), и их, очевидно, счётное множество.

                                        0
                                        Не уверен. Например, можно формально показать (но эта алгебра пока за пределами моих навыков), что функций с сигнатурой (a: Type) -> a -> a ровно одна.

                                        Мне кажется тут можно попробовать цепануть что-то из категорий. Там же показывается, что id морфизм единственен.

                                          0

                                          Проблема в том, что там надо идти «в другую сторону» — у вас всего лишь есть тип ∀a : *. a -> a, и вам надо показать, что его реализация единственна (экстенсионально; синтаксически их как раз бесконечно много — id, id . id, id . id . id, ...).


                                          Точно так же, как можно показать, что у ∀a : *. a -> b -> a тоже ровно один обитатель, а у ∀a : *. a -> a -> a — ровно два.

                                            0
                                            Для system F есть теоремы Рейнольдса. Какой есть аналог для зависимых типов?
                                              0

                                              Я [пока] не знаю.


                                              Этим летом на Lambdaconf был воркшоп по всяким подобным вещам, но, увы, мне не удалось выбраться на Lambdaconf.

                                    +2
                                    В nightly уже реализовали const generics (основное обсуждение тут
                                    Tracking issue for const generics (RFC 2000)). Теперь не нужно будет дикое шаманство с typenum и generic_array, которыми я активно пользуюсь.

                                    Пример выше можно переписать как-то так:
                                    fn foo<El: Eq, const Size: usize>(x: [El, {Size}, y: El) -> Option<Box<dyn UnsignedLessThan<{Size}>>>
                                    {
                                        // 10000 строк нечитаемого кода
                                    }
                                    


                                    К сожалению, писать реальный код на const generics пока невозможно из-за большого количества ICE (1, 2, 3, ..). Надеюсь скоро исправят.
                                      0

                                      Мы все их ждём, да :) Но я всё-таки писал, исходя из того, что есть на stable.

                                      0

                                      полезная статья, спасибо

                                        0
                                        Python — динамически типизированный, информации минимум, какие-то подсказки дают только тесты;


                                        Странное в оригинальной статье утверждение А что мешает использовать Gradual Typing и оставить мета информацию о типах?
                                          +1

                                          Исходная статья была написана в 2016 году, тогда, по идее, это ещё не было реализовано. Сейчас — да, возможно, может быть смысл внести поправку.

                                            +1
                                            Для истории: поддержка типов со всем тулингом в Python с версии 3.5, это 2015 год. Начиная с 3.6, 2016 год, типы можно использовать не только в сигнатурах функций, а вообще везде)
                                              +1

                                              Спасибо, значит, я что-то не то нашёл при попытке проверить сведения (сам с Python почти не работал, так что, думаю, мне простительно :)).

                                            +1

                                            И какой наиболее выразительный тип вы сможете написать?

                                          Только полноправные пользователи могут оставлять комментарии. Войдите, пожалуйста.

                                          Самое читаемое