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



Пару дней назад 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, на мой взгляд, достаточно показателен.

Вы можете помочь и перевести немного средств на развитие сайта



Комментарии (51):

  1. saipr
    /#20649731

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

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

  2. 0xd34df00d
    /#20649747

    Годнота.


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

    • Cerberuser
      /#20649801

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

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

      • 0xd34df00d
        /#20649843

        Ну, фишка идриса с 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 известен только в рантайме.


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


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

        • Cerberuser
          /#20649881

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

        • Amomum
          /#20650233 / +2

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

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

          • 0xd34df00d
            /#20652891 / +2

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


            Если чуть подробнее, то тайпчекеру неважно, какое именно значение будет в условном 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 ()

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

            • Amomum
              /#20653097

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


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


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

              • 0xd34df00d
                /#20653115

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

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


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

            • Cerberuser
              /#20653379

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

            • PsyHaSTe
              /#20660441

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

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

              • 0xd34df00d
                /#20661027

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


                Собственно, просто убрать последнее -> 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, то это вполне легитимная запись, но вопрос в том, что вы будете делать с конструкторами.

                • PsyHaSTe
                  /#20661123

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

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


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

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


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

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

                  • 0xd34df00d
                    /#20661157

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


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


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

                    • PsyHaSTe
                      /#20661373

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

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


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

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

                      • Cerberuser
                        /#20662083

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

                        • 0xd34df00d
                          /#20662101

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


                          Или в коде:


                          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

                          • PsyHaSTe
                            /#20663449

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

                        • PsyHaSTe
                          /#20663471

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

            • technic93
              /#20662785

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

        • technic93
          /#20654327

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

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


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

  3. inv2004
    /#20649783

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

    • Cerberuser
      /#20649809 / +1

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

  4. apro
    /#20649853

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

    • Cerberuser
      /#20649885

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

      • apro
        /#20650081

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

        • Cerberuser
          /#20650329

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

  5. bm13kk
    /#20649921

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

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

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

    • 0xd34df00d
      /#20649935

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


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

      • bm13kk
        /#20649973

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

        пример тут 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
        правая часть — положительные числа. Чем выше по кругу — тем больше
        лувая — отрицательные
        верхняя точка круга — символизирует положительную и отрицательную бесконечность

        • 0xd34df00d
          /#20650003

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


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


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

  6. bm13kk
    /#20649961

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

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

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

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

    • 0xd34df00d
      /#20649971

      Поэтому без теста не обойтись.

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

      • bm13kk
        /#20649987

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

        • 0xd34df00d
          /#20650007 / +3

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


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


          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

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

          • PsyHaSTe
            /#20660471

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

        • Cerberuser
          /#20650339

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

    • sshikov
      /#20651819

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

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

      • 0xd34df00d
        /#20652081

        Число функций, имеющих такую сигнатуру, скорее всего бесконечно.

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


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

        • sshikov
          /#20652165

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

          • 0xd34df00d
            /#20652905

            В каком смысле такая функция одна?

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


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

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

        • PsyHaSTe
          /#20660481

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

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

          • 0xd34df00d
            /#20661055

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


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

  7. qwerty19106
    /#20650331 / +1

    В 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, ..). Надеюсь скоро исправят.

    • Cerberuser
      /#20650335

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

  8. mahatimas
    /#20650337

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

  9. eyeofhell
    /#20653407

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


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

    • Cerberuser
      /#20653409 / +1

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

      • eyeofhell
        /#20653421 / +1

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

        • Cerberuser
          /#20653427 / +1

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

    • 0xd34df00d
      /#20654173

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