Comments 24
let (_, v1) = parse_i64_discarding!(«1,2,3,four,5»);
let (_, v2) = parse_i64_discarding!(«1,two,3,4,5»);
assert_eq!(
Equiv::check().map(|proof| zip_sum(v1.retag(proof), v2).into_native()),
Some(vec![2, 5, 7, 10])
);
Хорошо, у нас векторы одинаковой длины и мы это доказали. А если они разной длины?
Репы нет по ссылке.
Спасибо, пофиксил.
А если они разной длины?
Тогда Equiv::check() вернёт None, и, следовательно, использовать их в zip_sum (или любой другой функции, которой нужны векторы непременно одинаковой длины) мы не можем.
del
а гуй на шаблонах можно сделать?
Спасибо за статью! Достаточно интересный подход. Отчасти напоминает Ghosts of departed proofs, не читали?
Спасибо, очень крутая статья.
С таким уровнем упорством мне кажется уже стоит самому идрис потыкать, он в разы проще чем, что вы тут смогли сделать, так что никаких проблем полагаю с ним у вас не возникнет.
Завтипы это мощь. Хотя в прод, наверное, я бы ничего сложнее конст генериков не потащил :)
std:make_pair(1, std::make_pair(2, 3)) — вот вам и туплы.А практически… любая, самая простейшая задача на C++98 превращается в боль. Да даже на C++11. Скажем попробуйте написать на C++98 или C++11 функцию, которая принимает произвольное число аргументов, проверяет, что только один из них — целое число и, если такое случилось, возводит это число в квадрат. А в противном случае возвращает нуль.
Вот как это выглядит на C++17:
template<typename... Args>
auto foo(const Args&... args) {
if constexpr ((std::numeric_limits<Args>::is_integer + ... + 0) == 1) {
auto [arg] = std::tuple_cat([](const auto& arg){
if constexpr (
std::numeric_limits<std::decay_t<decltype(arg)>>::is_integer) {
return std::tuple(arg);
} else {
return std::tuple();
}
}(args)...);
return arg * arg;
} else {
return 0;
}
}
То же самое и с завтипами: появятся достаточно быстрые и удобные компиляторы — можно будет много чего на них делать. Не появятся… ну значит и без них обойдутся.
Теоретическая реализуемость не равна практической полезности, как бы…
Ну идрис мне кажется достаточно удобным. Доказывать всё подряд я бы на нём не стал, но писать на нём как на хаскелле с возможность не продолбаться при работе с данными из рантайма — одно удовольствие. Читаю ту книжку, которую рекомендовали в том комменте на который ссылается статья, очень классно написано. И это чуть ли не первая книжка, где очень много текста уделено работе с автоматическими рефакторингами IDE, которые чем сильнее типы, тем вкуснее становятся. Что странно, учитывая, что на практике как раз при углублении в типчики люди начинают рефакторингами всё активнее пользоваться.
Возьмите C++. Теоретически — почти всё что можно сделать в области метопрограммирования в C++17 — можно и в C++98.
Да я прекрасно понимаю. Я помню боль, когда у нас на проекте никак не могли перейти на пятый шарп с авсинк/авейт, и мы писали колбасу из коллбеков (хотя уже читали аннонс про авейты и даже попробовали в игрушечных проектах), Так писать можно, но совершенно ужасно. Особенно вещи вроде таймеров — без стейт-машины они весьма нетривиальны.
Да, чуть многословно, но в общем… жить можно.
Не знаю насчет многословно, но на мой взгляд просто очень страшно. Непонятно, зачем + 0 в конце (просто потому что сделать +… язык запрещает?), auto [arg] (похоже на деконструкцию, но лямбда возвращает либо тапл из 1 элемента, либо пустой, как они вообще друг с другом дружат?)...
В общем, я плюсы в свое время прошел стороной, дорогой паскаль-делфи-сишарп, и моей интуиции и универских познаний недостаточно, чтобы понять этот код. Издалека кажется, что он работает для вараргов длиной 1, а для всех остальных возвращает 0.
Непонятно, зачем + 0 в конце (просто потому что сделать +… язык запрещает?)Если не будет ни одного аргумента, то возникнет вопрос: «а какого типа 0 вам нужен». Может
int, может long, а может вообще какие-нибудь бегемоты. Операторы в C++ можно перекрывать для разных типов, не забывайте. В данном случае это не слишком важно, конечно. Но если опустить "+ 0", то функция не скомилируется при вызове без параметров.похоже на деконструкцию, но лямбда возвращает либо тапл из 1 элемента, либо пустой, как они вообще друг с другом дружат?Мы уже убедились, что там один целочисленный элемент. Каждая лямбда даёт либо тупл из одного элемента, либо из нуля. Дальше мы всё эту конструкцию «сплющиваем», но так как мы уже убедились, что там один целочисленный элемент — то можем потом спокойно это деконструировать.
Обратите внимание на общий фомат:
std::tuple_cat(λ(args)...). Если вы знаете что такое туплы (а должны бы — они в Haskell активно пользуются), что такое cat (это из Unix) — то относительно несложно понять что это всё должно делать.В общем, я плюсы в свое время прошел стороной, дорогой паскаль-делфи-сишарп, и моей интуиции и универских познаний недостаточно, чтобы понять этот код.Ну здравствуйте. Идеи там те же, что и в типичной программе не Haskell или Indris. В новой части, с метапрограмированием связанной. Хотя у каждого языка — свои заморочки, конечно. Тот факт что у вас, как бы, два языка в одном (ленивый функциональный при работе с шаблонами и классическое императивное наследие C) — немного бесит, но, в общем, при некотором опыте это всё не так сложно и читать и писать.
Издалека кажется, что он работает для вараргов длиной 1, а для всех остальных возвращает 0.Вот это как раз странно. Там же жорошо видно, что нам если там будет много аргументов (но только один целочисленный), то мы пойдём в ветку с деконструкцией. А деконструкция с неправильным числом агументов в C++ — это такая же ошибка компиляции, как и в Haskell или Idris…
То есть я понимаю, если бы предположили, что для 2-3-10 аргументов оно не скомпилируется… но как оно сможет 0 вернуть?
P.S. И да — об
auto [args...] уже тоже думают. Странно что ни в C++17, ни в C++20 не включили. Видимо потому что «острота проблемы» незаметна пока пишешь маленькие программы, а переход на C++17 (где только и появилась деконструкция) не так давно случился — пока компиляторы обновились, пока люди на них перешли… в C++ всё небыстро происходит…Обратите внимание на общий фомат: std::tuple_cat(λ(args)...). Если вы знаете что такое туплы (а должны бы — они в Haskell активно пользуются), что такое cat (это из Unix) — то относительно несложно понять что это всё должно делать.
ну что такое тапл конечно понятно, cat — я это лично понимаю как просто утилиту которая печатает файлы в stdout. Как они могут дружить не сильно понятно :)
Дальше мы всё эту конструкцию «сплющиваем», но так как мы уже убедились, что там один целочисленный элемент — то можем потом спокойно это деконструировать.
А зачем вся эта конструкция, если мы и так знаем что там один элемент? Или это просто иллюстрация возможностей?
но, в общем, при некотором опыте это всё не так сложно и читать и писать.
Понятно, спасибо за интересный пример. Хотя всё ещё непонятно, как работает деконструкция в случае
} else {
return std::tuple();
}Или это просто иллюстрация возможностей?Нет.
А зачем вся эта конструкция, если мы и так знаем что там один элемент?Ну вот потому что нет в стандартной библиотеке соответствующих средств, позволяющих из набора элементов выбрать один.
Она вообще, по меркам функциональных языков, бедновата. Представьте что у вас есть Haskell — но без вот этого вот всего набора
filter, zipWith и прочего. fold есть, map (это вот как раз три точки) и вот tuple_cat. И всё.Жить уже можно, но, да выглядит страшноватенько. Возникает желание написать себе более полную библиотеку, но это было бы разумно, если бы все, кто с вами работает Haskell знали — а так будет больше вопросов, чем упрощения…
Понятно, спасибо за интересный пример. Хотя всё ещё непонятно, как работает деконструкция в случаеДык она там не работает!
} else { return std::tuple(); }
Ну грубо говоря — тут мы получим единственный позитивный элемент из списка:
get_positive = decompose . concat . map lambda
where decompose (x:[]) = x
lambda x | x > 0 = [x]
| otherwise = []
Правда ошибка будет в рантайме если их там больше, чем один. А в С++ мы работаем примерно также, только всё в компайл-тайм происходит.
P.S. Если я вам скажу, что с туплами в C++ работают примерно как с HList'ами в Haskell — станет понятнее? Или наоборот?
P.P.S. И, кстати, продолжайте рассказывать про то, что вы не знаете как
cat может быть с туплами связан… а я вам, типа, даже поверю. concat же в Haskell делает вот ровно то же, что std::tuple_cat в C++. Только в C++ он, внезапно, работает с туплами и с массивами (а списки в C++ — это немного о другом, в компайл-тайме с ними нельзя работать).
Concat это понятно, а вот cat у обычный людей это просто кошка :)
P.S. Если я вам скажу, что с туплами в C++ работают примерно как с HList'ами в Haskell — станет понятнее? Или наоборот?
Стало понятнее)
P.P.S. И, кстати, продолжайте рассказывать про то, что вы не знаете как cat может быть с туплами связан… а я вам, типа, даже поверю. concat же в Haskell делает вот ровно то же, что std::tuple_cat в C++. Только в C++ он, внезапно, работает с туплами и с массивами (а списки в C++ — это немного о другом, в компайл-тайме с ними нельзя работать).
Для меня cat — это утилита командной строки UNIX, а concat — это уже функция которая склеивает значения. Если бы было написано во втором варианте у меня вопросов бы не возникло. Запутался немного.
Но, в конечном итоге, конечно, это всё-таки отдельный язык. Со своими очень странными странностями. Например зачем в такой вот табличке
TypeTag:template<typename X, X p>
class TypeTag;
template<typename>
class RPCInfo;
template<typename X>
class RPCInfo<TypeTag<int (X::*)(int), &X::foo>> {
public:
static constexpr auto RPCtag = "FOO_INT";
};
template<typename X>
class RPCInfo<TypeTag<int (X::*)(int, int), &X::foo>> {
public:
static constexpr auto RPCtag = "FOO_INT_INT";
};
template<typename X>
class RPCInfo<TypeTag<int (X::*)(int), &X::bar>> {
public:
static constexpr auto RPCTag = "BAR_INT";
};
Немного потыкал, но пока что руки не доходят погрузиться глубже, слишком много всего интересного вокруг :)
Интересное построение. Смущает, что очень многое зависит от правильности деклараций и компилятор не проверяет их. Например, вот эта функция:
impl<Item, N: Nat> Vect<Item, N> {
pub fn retag<New: Nat>(self, _proof: Equiv<N, New>) -> Vect<Item, New> {
Vect(self.0, PhantomData)
}
}Объект Equiv здесь никак не используется, можно было бы убрать этот аргумент и компиляция бы не сломалась. В Idris вы не сможете написать функцию типа Vect n a -> Vect m a, потому что без доказательства n = m это преобразование сделать невозможно.
Имитируем функционал зависимых типов в системе типов Rust