Пару дней назад 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 строк нечитаемого кода
}Теперь мы требуем не просто возможности сравнения на равенство — мы требуем, чтобы это сравнение являлось отношением эквивалентности. Это несколько сужает круг возможных параметров, но зато теперь и типы, и тесты подсказывают (пусть и не указывают явно), что ожидаемое поведение действительно должно попадать в спецификацию.
Этот вариант не имеет отношения к исходной задаче, зато является, на мой взгляд, хорошей иллюстрацией к принципу: "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, основанный на типаже
Иначе говоря, таким образом мы написали функцию, которая гарантированно возвращает неотрицательное (беззнаковое) число, меньшее, чем исходный размер массива (вернее, конечно, она возвращает этот самый trait object, у которого мы позже должны вызвать метод as_usize, гарантированно возвращающий такое число).
Подвохов у данного подхода ровно два:
- Мы можем ощутимо потерять в производительности. Если вдруг по какой-то причине такая наша функция окажется на "горячем" участке программы, постоянная необходимость в динамических вызовах может оказаться одной из самых медленных операций. Впрочем, этот недостаток вполне может быть не так значителен, как кажется, но есть и второй:
- Чтобы эта функция корректно скомпилировалась, нам потребуется либо фактически написать внутри неё самой доказательство корректности её работы, либо "обмануть" систему типов через
unsafe. Первое слишком сложно для пятничной статьи, ну а второе — попросту жульничество.
Заключение
Разумеется, на практике в подобных случаях будет использоваться либо вторая реализация (принимающая срез произвольного типа), либо реализация под спойлером (принимающая итерируемый объект). Все последующие рассуждения почти наверняка не несут практического интереса и служат исключительно упражнением по работе с системой типов.
Тем не менее, сам факт, что на системе типов Rust можно суметь эмулировать одну из особенностей заведомо более сильной системы типов Idris, на мой взгляд, достаточно показателен.
Комментарии (51)
0xd34df00d
20.09.2019 22:49Годнота.
Но, если я правильно понимаю, читерство :) У вас в последнем варианте размер массива так или иначе известен статически, верно?
Cerberuser Автор
20.09.2019 22:57У вас в последнем варианте размер массива так или иначе известен статически, верно?
Совершенно верно, для GenericArray это часть типа. А в чём "читерство"?
0xd34df00d
20.09.2019 23:11Ну, фишка идриса с
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 Автор
20.09.2019 23:25Кстати, спасибо, тоже интересная задача: можно ли сгенерировать GenericArray с неизвестной заранее длиной, и если да, то как его можно будет использовать: вернуть из функции, например, заведомо нельзя — точнее, можно, но только в виде trait object, — а вот передать глубже по дереву вызовов, может быть, и получится.
Amomum
21.09.2019 02:57+2Собственно, это ключевая фича зависимых типов — можно ли выражать терм-левел зависимости в типах, которые могут быть вычислены лишь во время выполнения, или нет.
А вас не затрудник немножко разжевать это для несведующих?
Как это происходит?0xd34df00d
21.09.2019 23:14+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
Тут написано две следующее:
- Вектор — это такая штука, которая параметризована своей длиной (натуральным числом) и типом элементов и является типом.
- Вектор можно создать при помощи конструктора
Nil, и его длина будет нулём. - Вектор можно создать при помощи конструктора
::, имея уже какой-то вектор любой длины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
22.09.2019 00:55Огого! Спасибо большое за подробный ответ!
Не уверен, что все понял, к сожалению, очень уж синтаксис непривычный.
У меня есть ощущение, что что-то частично подобное можно сделать на шаблонах С++, скажем, у std::array размер — шаблонный параметр, довольно легко написать функцию, которая складывает только массивы одной длины.
Но вот кусок, который родит нужный класс в рантайме в зависимости от прочитанной из файла длины — вот тут сходу не получается.
0xd34df00d
22.09.2019 01:05Но вот кусок, который родит нужный класс в рантайме в зависимости от прочитанной из файла длины — вот тут сходу не получается.
И не сходу с теми же гарантиями тоже не получится :)
Собственно, как я писал чуть выше, в этом вся разница — обязательно ли знать значения всех этих числовых параметров при компиляции или нет.
PsyHaSTe
23.09.2019 19:53data Vect: (n: Nat) -> (ty: Type) -> Type where
Nil: Vect 0 ty
(::): ty -> Vect n ty -> Vect (S n) tyЯ правильно понимать, что если мы уберем последнее
-> Typeто мы сможем объявить тайп конструктор с одной дыркой?0xd34df00d
23.09.2019 21:47Я не уверен, что понял вопрос. Что значит «с одной дыркой»?
Собственно, просто убрать последнее
-> 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
23.09.2019 22:03Я не уверен, что понял вопрос. Что значит «с одной дыркой»?
Это значит что конструктору нужно передать один тип чтобы получить тип. Я взял термин из скаловой тусовки, думал он общепринят.
Собственно, просто убрать последнее -> Type у вас не получится, даже если не рассматривать конструкторы, это синтаксическая ошибка:
Я просто думал можно написать метод над тайп конструктором а не обычным типом, а-ля скаловое
def Foo[F[_]]
Если вы теперь напишете data Vect: (n: Nat) -> Type, то это вполне легитимная запись, но вопрос в том, что вы будете делать с конструкторами.
Применять где-то позже, логично же :)
0xd34df00d
23.09.2019 22:11Ну я скалу совсем не знаю, она меня своими квадратными скобками пугает. А в идрисовской (да и вообще, похоже, в формально-доказательной) тусовке дырка — отсутствующий proof term, как вон вся та ерунда со знаками вопроса в комменте выше.
Vect— в каком-то смысле просто функция на типах, и вы там указываете её сигнатуру.-> Typeв конце будет почти всегда. Напишетеdata Vect : Nat -> Type -> Type, будет тип данных, параметризованный числом и типом. Напишетеdata Vect : Type -> Type— будет тип данных, параметризованный только типом (собственно, список определяется какdata List : Type -> Type).
Надеюсь, это хоть немного в тему того, что вы спрашивали.
PsyHaSTe
23.09.2019 22:57Ну я скалу совсем не знаю, она меня своими квадратными скобками пугает.
Это нормально. Нужно пообвыкнуть и чуть-чуть смириться.
А в идрисовской (да и вообще, похоже, в формально-доказательной) тусовке дырка — отсутствующий proof term, как вон вся та ерунда со знаками вопроса в комменте выше.
Под дыркой имеется ввиду незакрепленный генерик. Например, в терминах сишарпа
List<>— тайп-конструктор с одной дыркой,HashMap<,>— с двумя, и так далее.Cerberuser Автор
24.09.2019 04:23По идее,
(n: Nat) -> (ty: Type) -> Type— это тип с двумя дырками, получается. По крайней мере, до тех пор, пока мы не подставим конкретное число n и конкретный тип ty.0xd34df00d
24.09.2019 04:34Да, если я таки правильно понял, что такое дырка.
Или в коде:
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
24.09.2019 11:39не совсем, тут та же разница, как между
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
24.09.2019 10:03Синтаксис непривычный, но фишка классная, надо вам писать статью про ФП в примерах.
technic93
22.09.2019 15:15(тут мне стало интересно, можно ли похожее на плюсах, хехе)
с границами известными в compile-time легко, есть уже всякие библиотеки, может даже как часть буста, например https://www.boost.org/doc/libs/1_69_0/libs/safe_numerics/doc/html/tutorial/6.html.
Весь интерес в том чтобы это работало в рантайм, как Вы написали ниже.
inv2004
20.09.2019 22:54Спасибо за наводку на typenum .
Cerberuser Автор
20.09.2019 23:00+1Приятно слышать, что подобный подход может быть полезен) Сам пока что из практических применений видел только пакет nalgebra, где typenum-овские типы позволяют статически гарантировать, что операции с матрицами будут корректны (особенно перемножение).
apro
20.09.2019 23:17А зачем
Option<Box<dyn Trait>>, нельзя просто Option` вернуть?Cerberuser Автор
20.09.2019 23:27Не совсем понимаю, "просто Option" — это в данном случае что?
apro
21.09.2019 00:59Option<impl Trait>неудачное редактирование съело правильное форматированиеCerberuser Автор
21.09.2019 06:14Соль в том, что
Option<impl Trait>— это "Option с конкретным неназванным типом внутри". А здесь у нас на каждый вариант ответа, т.е. на каждую позицию в списке, тип будет разный.
bm13kk
20.09.2019 23:45> пройти тест…
> foo(&[std::f64::NAN], std::f64::NAN) = None
Все правильно. Это НЕ особенность реализации флоат. Это отличная демонтрация различия между мышлением математика и программиста. И флоат тут сделан математически правильно.
Для программиста флоат — набор битов. Если два набора битов совпадает — значения совпадают. Почти все баги с null связаны с таким мышлением.
Однако тут флоат — это абстракция с определенной реализацией. Абстракция чисел. И в этой абстракции NaN != NaN. Что и реализовано.0xd34df00d
20.09.2019 23:49Среди чисел нет таких, которые не были бы равны сами себе. Это так себе абстракция, математики не одобряют.
Флоат — это такая узкая специализация монады Maybe, где вместо одного Nothing есть с пяток разных вариантов «ошибки».
bm13kk
21.09.2019 00:07Флоат — это не абстракция «некоторый набор чисел» это абстракция «числового поля». Когда бесконечное поле надо обстрагировать конечной сущностью — обычно делают преобразование бесконейной линии в круг. Непомню как оно называется но на ночь искать лениво.
пример тут 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
21.09.2019 00:21А где там наны-то?
Ссылки, похоже, тут не очень релевантны, потому что круг тоже бесконечный (и равномощен прямой), да и в R, Q и прочих подобных нет элемента «бесконечность». Он, конечно, есть в нестандартном аналоге R, но давайте не будем вскрывать эту тему (и он там равен сам себе, потому что forall x. x = x принадлежит теории R, а значит и ее нестандартному расширению).
То есть, понятно, что можно придумывать произвольные правила обращения с закорючками на бумаге, но вопрос в том, имеет ли это отношение к реальному миру.
bm13kk
21.09.2019 00:01Надо прочитать оригинальную статью.
Но эта статья — полностью неверна в своем тезисе. Хотя и было интересно узнать про некоторые детали.
Все разбивается об елементарный пример. Функция которая возвращает количество елементов равных заданному имеет ту-же* сигнатуру. Поэтому без теста не обойтись.
* Если совсем точным — в этом варианте** сужение, так как она никогда не вернет None. Но компилятор Раста такой ошибки не найдет.
** Если учесть мой первый комментарий что правильно использовать таки partialEq то сужения не будет. None будет для случая когда y!=y0xd34df00d
21.09.2019 00:07Поэтому без теста не обойтись.
Осталось научиться придумывать тесты.
foo([1, 2, 3], 2) == 1не обнаружит проблему в вашем варианте функции. Поэтому без формального доказательства не обойтись.bm13kk
21.09.2019 00:131 не надо ограничивать елементарными тестами
`foo([32, 16, 18, 3, 44, 3456, 3], 3)`
2 надо добавлять случайные тесты. Но оно работает только при строгих процессах. Когда упавшый СИ не перезапускают от лени — а каждый раз разбираются и ищут
3 мутационные тесты0xd34df00d
21.09.2019 00:22+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
23.09.2019 19:57В поддержку этого комментария: я гарантирую, что у вас уйдет больше 15 минут на написание всех необходимых тестов + они еще и не дадут того уровня уверенности. Типы — Тесты 1:0.
Cerberuser Автор
21.09.2019 06:18По второму пункту — эх, а мне ж хотелось сделать набросок случайно генерируемого теста, но решил, что это будет всё-таки оффтопом… Видимо, ошибся, спасибо за наводку)
sshikov
21.09.2019 16:37>Функция которая возвращает количество елементов равных заданному имеет ту-же* сигнатуру.
Число функций, имеющих такую сигнатуру, скорее всего бесконечно.
>Поэтому без теста не обойтись.
Мы пока только убедились, что такая сигнатура не позволяет нам судить о правильности работы функции. Ну то есть правильный вывод — что такой системы типов недостаточно. А уж нужны ли нам тесты (или там формальное доказательство) — это отдельная тема все-таки.0xd34df00d
21.09.2019 17:47Число функций, имеющих такую сигнатуру, скорее всего бесконечно.
Не уверен. Например, можно формально показать (но эта алгебра пока за пределами моих навыков), что функций с сигнатурой
(a : Type) -> a -> aровно одна.
Я бы скорее интуитивно ожидал, что функций с сигнатурой из последнего примера конечное число (по крайней мере, в сеттинге чистого ФП).
sshikov
21.09.2019 18:14Хм. На входе вектор и элемент. На выходе «индекс элемента». А точнее не индекс, а целое (потому что из сигнатуры этого не следует). В каком смысле такая функция одна?
0xd34df00d
21.09.2019 23:19В каком смысле такая функция одна?
Это я про
a -> a.
Хм. На входе вектор и элемент. На выходе «индекс элемента». А точнее не индекс, а целое (потому что из сигнатуры этого не следует).
Хм, похоже, вы правы. Достаточно рассмотреть все функции вида
(n : Nat) -> Fin n(т. е. которые опираются просто на длину вектора), а их уже, похоже, бесконечное число (правда, ещё интересный вопрос в том, сколько из них вычислимы, но то такое).
PsyHaSTe
23.09.2019 19:59Не уверен. Например, можно формально показать (но эта алгебра пока за пределами моих навыков), что функций с сигнатурой (a: Type) -> a -> a ровно одна.
Мне кажется тут можно попробовать цепануть что-то из категорий. Там же показывается, что id морфизм единственен.
0xd34df00d
23.09.2019 21:52Проблема в том, что там надо идти «в другую сторону» — у вас всего лишь есть тип
?a : *. a -> a, и вам надо показать, что его реализация единственна (экстенсионально; синтаксически их как раз бесконечно много —id,id . id,id . id . id, ...).
Точно так же, как можно показать, что у
?a : *. a -> b -> aтоже ровно один обитатель, а у?a : *. a -> a -> a— ровно два.
qwerty19106
21.09.2019 06:15+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 Автор
21.09.2019 06:16Мы все их ждём, да :) Но я всё-таки писал, исходя из того, что есть на stable.
eyeofhell
22.09.2019 07:41Python — динамически типизированный, информации минимум, какие-то подсказки дают только тесты;
Странное в оригинальной статье утверждение А что мешает использовать Gradual Typing и оставить мета информацию о типах?Cerberuser Автор
22.09.2019 07:47+1Исходная статья была написана в 2016 году, тогда, по идее, это ещё не было реализовано. Сейчас — да, возможно, может быть смысл внести поправку.
eyeofhell
22.09.2019 08:01+1Для истории: поддержка типов со всем тулингом в Python с версии 3.5, это 2015 год. Начиная с 3.6, 2016 год, типы можно использовать не только в сигнатурах функций, а вообще везде)
Cerberuser Автор
22.09.2019 08:17+1Спасибо, значит, я что-то не то нашёл при попытке проверить сведения (сам с Python почти не работал, так что, думаю, мне простительно :)).
saipr
Трудно не согласиться.