История изменений
Исправление quasimoto, (текущая версия) :
Представь себе - у нас есть десяток библиотек, в каждой - определяется какая-то коллекция и функции для работы с ней, при этом любая коллекция может быть отсортирована.
Но зачем?
Вообще что-то странное говоришь — в примитивных случаях голая коллекция и её свойства распадаются (в dependent pattern matching) как элементы кортежа, свойство можно выкинуть и спокойно использовать голую коллекцию, верифицуруемая по части свойств функция просто добавляет свойств в свой аргумент (типа sort : Seq -> SeqSorted), причём их можно потаскать и потом стереть при компиляции. А сложные свойства требуют модификации самих типов контейнеров (как в GADTs) для облегчения доказательств свойств функций, но всё тоже волне стирается.
Для примера — безопасная индексация к std::array<T, n> x, то есть гарантия при size_t i; x[i]; что i < n может делаться как operator[](size_t i){i < n} что заставит везде проверять if (i < n) в dependent-if для неявной передачи свойства в operator[], такое свойство легко стирается при компиляции после проверки.
если у нас код был написан для одной, то мы другие не можем использовать
Какой код? Всё равно не знаю о каких проблемах ты говоришь :)
Можешь доказать что std::copy (<algorithm>) для упорядоченного итератора даст упорядоченный итератор, std::vector со свойством sorted превратится в std::list, свойство (итератора, а значит и контейнера) сохранится.
Исправление quasimoto, :
Представь себе - у нас есть десяток библиотек, в каждой - определяется какая-то коллекция и функции для работы с ней, при этом любая коллекция может быть отсортирована.
Но зачем?
Вообще что-то странное говоришь — в примитивных случаях голая коллекция и её свойства распадаются (в dependent pattern matching) как элементы кортежа, свойство можно выкинуть и спокойно использовать голую коллекцию, верифицуруемая по части свойств функция просто добавляет свойств в свой аргумент (типа sort : Seq -> SeqSorted), причём их можно потаскать и потом стереть при компиляции. А сложные свойства требуют модификации самих типов контейнеров (как в GADTs) для облегчения доказательств свойств функций, но всё тоже волне стирается.
Для примера — безопасная индексация к std::array<T, n> x, то есть гарантия при size_t i; x[i]; что i < n может делаться как operator[](size_t i){i < n} что заставит везде проверять if (i < n) в dependent-if для неявной передачи свойства в operator[], такое свойство легко стирается при компиляции после проверки.
если у нас код был написан для одной, то мы другие не можем использовать
Какой код? Всё равно не знаю о каких проблемах ты говоришь :)
Можешь доказать что std::copy (<algorithm>) для упорядоченного итератора даст упорядоченный итератор, std::vector со свойством sorted превратится в std::list, свойство сохраниться.
Исходная версия quasimoto, :
Представь себе - у нас есть десяток библиотек, в каждой - определяется какая-то коллекция и функции для работы с ней, при этом любая коллекция может быть отсортирована.
Но зачем?
Вообще что-то странное говоришь — в примитивных случаях голая коллекция и её свойства распадаются (в dependent pattern matching) как элементы кортежа, свойство можно выкинуть и спокойно использовать голую коллекцию, верифицуруемая по части свойств функция просто добавляет свойств в свой аргумент (типа sort : Seq -> SeqSorted), причём их можно потаскать и потом стереть при компиляции. А сложные свойства требуют модификации самих типов контейнеров (как в GADTs) для облегчения доказательств свойств функций, но всё тоже волне стирается.
Для примера — безопасная индексация к std::array<T, n> x, то есть гарантия при size_t i; x; что i < n может делаться как operator[](size_t i){i < n} что заставит везде проверять if (i < n) в dependent-if для неявной передачи свойства в operator[], такое свойство легко стирается при компиляции после проверки.
если у нас код был написан для одной, то мы другие не можем использовать
Какой код? Всё равно не знаю о каких проблемах ты говоришь :)
Можешь доказать что std::copy (<algorithm>) для упорядоченного итератора даст упорядоченный итератор, std::vector со свойством sorted превратится в std::list, свойство сохраниться.