Этого треда уже нет.
Это копия, сохраненная 15 октября 2015 года.
Скачать тред: только с превью, с превью и прикрепленными файлами.
Второй вариант может долго скачиваться. Файлы будут только в живых или недавно утонувших тредах. Подробнее
Если вам полезен архив М.Двача, пожертвуйте на оплату сервера.
Это копия, сохраненная 15 октября 2015 года.
Скачать тред: только с превью, с превью и прикрепленными файлами.
Второй вариант может долго скачиваться. Файлы будут только в живых или недавно утонувших тредах. Подробнее
Если вам полезен архив М.Двача, пожертвуйте на оплату сервера.
669 Кб, 479x1417
ИТТ обсуждают языки с зависимыми типами (Idris, Agda, Coq, ATS и другие).
Что: зависимый тип — тип, который может быть параметризован не только другим типом, но и термом. Простой пример такого типа — Vect n a, где n — натуральное число, а a — тип. Кроме того, в языках с зависимыми типами типы являются объектами первого класса.
Зачем: благодаря изоморфизму Карри — Ховарда, можно не только писать факториалы и числа Фибоначчи, но и доказывать корректность их реализации. Также можно доказать корректность реализации FizzBuzz'а, сортировки слиянием, даже неба, даже аллаха. Кроме того, зависимые типы обладают большей выразительностью, чем, к примеру, система типов в Haskell.
Что: зависимый тип — тип, который может быть параметризован не только другим типом, но и термом. Простой пример такого типа — Vect n a, где n — натуральное число, а a — тип. Кроме того, в языках с зависимыми типами типы являются объектами первого класса.
Зачем: благодаря изоморфизму Карри — Ховарда, можно не только писать факториалы и числа Фибоначчи, но и доказывать корректность их реализации. Также можно доказать корректность реализации FizzBuzz'а, сортировки слиянием, даже неба, даже аллаха. Кроме того, зависимые типы обладают большей выразительностью, чем, к примеру, система типов в Haskell.
>>483770
Только изоморфизм Карри — Ховарда существует между программами на лямбда исчихлении с типами и мат. логикой. Так как 99% программ - не на лямбда исчислении, а многие из них ещё и без типов, то доказывать остаётся только собственные факториалы на хачкеле. Охуенно.
Только изоморфизм Карри — Ховарда существует между программами на лямбда исчихлении с типами и мат. логикой. Так как 99% программ - не на лямбда исчислении, а многие из них ещё и без типов, то доказывать остаётся только собственные факториалы на хачкеле. Охуенно.
И теперь вопрос, зачем это всё нужно, если есть логика Хоара и Сепарационная логика, с помощью которых можно верифицировать обычные императивные программы с мутабельными структурами, в том числе содержащие указатели?
>>483777
Зависимые типы пригодны не только для ФП. См. ATS (http://www.ats-lang.org/Papers.html) как пример.
Зависимые типы пригодны не только для ФП. См. ATS (http://www.ats-lang.org/Papers.html) как пример.
>>483770
Нихуя не понял. Я в крестах могу такое сделать, в чем соль-то?
>Простой пример такого типа — Vect n a, где n — натуральное число, а a — тип
Нихуя не понял. Я в крестах могу такое сделать, в чем соль-то?
Я так понимаю эта хуйня имеет прикладное применение только в академии? Т.е. обычному быдлу вроде меня кроме как дома за борщом оно нигде не пригодится?
>>483861
Что-то вроде
И?
Что за зависимые типы, нахуй? Пиздец.
> тип вектора зависит от его длины
Что-то вроде
> template<uint n, typename T> Vector
И?
Что за зависимые типы, нахуй? Пиздец.
>>483879
Что нет? Почему нет? Если ты нормально объяснить не можешь, значит ты нихуя не понимаешь в теме, и нахуй ты тогда тред создал, мудила? У меня бомбит прямо.
Что нет? Почему нет? Если ты нормально объяснить не можешь, значит ты нихуя не понимаешь в теме, и нахуй ты тогда тред создал, мудила? У меня бомбит прямо.
>>483880
да
да
>>483873
Малаца. А теперь пусть твой `uint n` неизвестен во время компиляции.
> template<uint n, typename T> Vector
Малаца. А теперь пусть твой `uint n` неизвестен во время компиляции.
>>483961
Так у вас сдесь динамикодрисня? Почему сразу не предупреждаете?
> усть твой `uint n` неизвестен во время компиляции
Так у вас сдесь динамикодрисня? Почему сразу не предупреждаете?
>>483982
Ну, статическая типизация - тип определяется во время объявления, тоесть известен во время компиляции. Динамическая типизация - тип определяется по время присваивания значения, тоесть может не быть известен во время компиляции.
Вердикт - динамикодрисня.
>попробуй ещё раз
Ну, статическая типизация - тип определяется во время объявления, тоесть известен во время компиляции. Динамическая типизация - тип определяется по время присваивания значения, тоесть может не быть известен во время компиляции.
> твой `uint n` неизвестен во время компиляции
Вердикт - динамикодрисня.
Например, пусть есть функция конкатенации двух списков вида:
(++) : Vect n a -> Vect m a -> Vect (n + m) a
Компилятор, вообще говоря, не знает, чему равно n. И чему равно m не знает. Но тем не менее, он способен статически проверить, что функция (++) действительно для любых двух векторов с длинами n и m вернёт вектор с длиной (n + m).
>>483997
Неправильно, попробуй ещё раз.
(++) : Vect n a -> Vect m a -> Vect (n + m) a
Компилятор, вообще говоря, не знает, чему равно n. И чему равно m не знает. Но тем не менее, он способен статически проверить, что функция (++) действительно для любых двух векторов с длинами n и m вернёт вектор с длиной (n + m).
>>483997
> Вердикт - динамикодрисня.
Неправильно, попробуй ещё раз.
>>484000
Чтобы еще раз услышать вскукареки динамикопитушка? Я лучше скрою тред.
> ко ко ко ко
> попробуй ещё раз
Чтобы еще раз услышать вскукареки динамикопитушка? Я лучше скрою тред.
>>484006
Окай, но что мешает заебашить твои термы на типах в тех же крестах и проверять себе что хочешь на этапе компиляции, м?
Окай, но что мешает заебашить твои термы на типах в тех же крестах и проверять себе что хочешь на этапе компиляции, м?
>>484014
Лол, ну заебашь.
Лол, ну заебашь.
41 Кб, 373x457
обиженный байтуx пытается устроить срач итт
oкрoпил yриной мaнькин рoтeшник
брызги урины алсо задели рнр тредик
oкрoпил yриной мaнькин рoтeшник
брызги урины алсо задели рнр тредик
>>484023
Такие-то проекции. Иди кушать, борщ стынет.
Такие-то проекции. Иди кушать, борщ стынет.
>>484000
http://ideone.com/MeKYz1
Вот так нужно сделать или что?
Вообще я считал что плюсы единственный мейнстримный язык с зависимыми типами. Конечно корявыми, но вроде утверждение верное. Да даже если бы и нельзя было складывать эти инты - всё равно анон должен был почуять что обосрался когда один тип начал зависеть от некоторой величины.
_другой анон_
http://ideone.com/MeKYz1
Вот так нужно сделать или что?
Вообще я считал что плюсы единственный мейнстримный язык с зависимыми типами. Конечно корявыми, но вроде утверждение верное. Да даже если бы и нельзя было складывать эти инты - всё равно анон должен был почуять что обосрался когда один тип начал зависеть от некоторой величины.
_другой анон_
>>484056
ха лол может звездочками сработает
ха лол может звездочками сработает
>>484056
Нет же. Вот простой пример: http://ujeb.se/WBxyC
`n` в Vect n a не просто так: для пустого списка он всегда 0, а для любого списка `xs` с длиной `n`, список `x::xs` будет иметь длину `(n+1)`.
Компилятор гарантирует, что для списков с длинами `n` и `m` функция (++) вернёт список с длиной `n + m`.
Вот что ты получишь, если функцию (++) реализовать неправильно: http://ujeb.se/cb9at
Can't unify
Vect (k + k) a (Type of xs ++ xs)
with
Vect (plus k m) a (Expected type)
Specifically:
Can't unify
plus k k
with
plus k m
Изобрази мне пример подобной проверки типов на С++.
Нет же. Вот простой пример: http://ujeb.se/WBxyC
`n` в Vect n a не просто так: для пустого списка он всегда 0, а для любого списка `xs` с длиной `n`, список `x::xs` будет иметь длину `(n+1)`.
Компилятор гарантирует, что для списков с длинами `n` и `m` функция (++) вернёт список с длиной `n + m`.
Вот что ты получишь, если функцию (++) реализовать неправильно: http://ujeb.se/cb9at
Can't unify
Vect (k + k) a (Type of xs ++ xs)
with
Vect (plus k m) a (Expected type)
Specifically:
Can't unify
plus k k
with
plus k m
Изобрази мне пример подобной проверки типов на С++.
>>484056
А можешь сделать так, чтобы дефолтный конструктор возвращал вектор нужной длины в зависимости от типа?
А можешь сделать так, чтобы дефолтный конструктор возвращал вектор нужной длины в зависимости от типа?
>>483871
Даже в академических кругах эту хуйню считают слишком академической, там что копай глубже.
Даже в академических кругах эту хуйню считают слишком академической, там что копай глубже.
73 Кб, 315x332
dotty anyone?
>>484093
Удобно что есть определение натуральных чисел и операций над ними (вычитать их можно? а если 0 - 1?) и ошибки типов написаны по-человечески.
начал уже было писать
```
template <typename T, int N>
vec<T, N + 1> append(vec<T, N> v, T item){
\t//constructing
\treturn vec<T, N + 1>();
}
```
наверное опять проебу разметку
и дальше специализировать plusplus для случая M = 0. Остановился на том что не могу деструктуризировать vec.
Но да я вижу что ты мне хочешь сказать, что кроме зависмости типа он ещё предоставляет некоторые проверки, в то время как C++ не выдаст ошибки если в эту неправильную функцию подать массивы одинаковых размеров.
В тоже время ты волен не добавлять информации о размере вектора в тип, что как-то портит идею. Сам себе создаёшь правила и сам следуешь по ним. Все равно что ассертов расставить по коду. Тоже конечно здорово, но не сказать что без зависимых типов ты сосёшь хуи.
А если допустим ты пишешь функции с этим вектором стандартным а потом понимаешь что нужно будет определить длину вектора в рантайме то ты такой типа списочек хуйнёшь? Или же эти проверки исключительно для корректности функций и ты где-нибудь сможешь сделать что-то вроде
set : a -> (n:Nat) -> Vect n a
Разумеется я не знаю как это выглядит
Удобно что есть определение натуральных чисел и операций над ними (вычитать их можно? а если 0 - 1?) и ошибки типов написаны по-человечески.
начал уже было писать
```
template <typename T, int N>
vec<T, N + 1> append(vec<T, N> v, T item){
\t//constructing
\treturn vec<T, N + 1>();
}
```
наверное опять проебу разметку
и дальше специализировать plusplus для случая M = 0. Остановился на том что не могу деструктуризировать vec.
Но да я вижу что ты мне хочешь сказать, что кроме зависмости типа он ещё предоставляет некоторые проверки, в то время как C++ не выдаст ошибки если в эту неправильную функцию подать массивы одинаковых размеров.
В тоже время ты волен не добавлять информации о размере вектора в тип, что как-то портит идею. Сам себе создаёшь правила и сам следуешь по ним. Все равно что ассертов расставить по коду. Тоже конечно здорово, но не сказать что без зависимых типов ты сосёшь хуи.
А если допустим ты пишешь функции с этим вектором стандартным а потом понимаешь что нужно будет определить длину вектора в рантайме то ты такой типа списочек хуйнёшь? Или же эти проверки исключительно для корректности функций и ты где-нибудь сможешь сделать что-то вроде
set : a -> (n:Nat) -> Vect n a
Разумеется я не знаю как это выглядит
>>484104
Странная просьба не находишь?
Вот если бы ты попросил ограничить тип в темплейте то да я бы сказал что тут плюсы сосут (хотя есть костыли со специализацией). Хотя я их вроде и не защищал здесь.
А так вроде конструктор создаётся при вызове пользователем vec<T,N> v; где T и N любые.
Можно сделать внешнюю функцию с типом T и специализировать под несколько типов
template<>
vec<int> vec_constructor<int>{
return vec<int, 4>();
}
Странная просьба не находишь?
Вот если бы ты попросил ограничить тип в темплейте то да я бы сказал что тут плюсы сосут (хотя есть костыли со специализацией). Хотя я их вроде и не защищал здесь.
А так вроде конструктор создаётся при вызове пользователем vec<T,N> v; где T и N любые.
Можно сделать внешнюю функцию с типом T и специализировать под несколько типов
template<>
vec<int> vec_constructor<int>{
return vec<int, 4>();
}
>>484130
Хитрость в том, что все эти `n` существуют только во время компиляции, во время выполнения это самый что ни на есть обычный список. Так что если тебе нужна длина вектора в рантайме, то придётся таки вычислить его длину, и потратить O(n) времени.
Правда если потом ты хочешь передать этот в функцию вроде `Vect 5 a -> ...`, то нужно, чтобы функция, вычисляющая длину, возвращала зависимую пару (n Vect n a). Тогда ты сможешь вручную проверить, что n действительно равно пяти, и если так, передать уже вектор в функцию.
С другой стороны, можно и доказывать, что данные обладают требуемым функцией свойствами. Список, к которому добавили элемент не может быть пустым, остаток от деления меньше делителя, моноидальная операция чего-либо с нейтральным элементом вернёт то самое «чего-либо» и так далее.
В принципе, вычитание могло бы требовать доказательства, что первое число не меньше второго, но в Idris сделали всё довольно топорно.
> А если допустим ты пишешь функции с этим вектором стандартным а потом понимаешь что нужно будет определить длину вектора в рантайме то ты такой типа списочек хуйнёшь?
Хитрость в том, что все эти `n` существуют только во время компиляции, во время выполнения это самый что ни на есть обычный список. Так что если тебе нужна длина вектора в рантайме, то придётся таки вычислить его длину, и потратить O(n) времени.
Правда если потом ты хочешь передать этот в функцию вроде `Vect 5 a -> ...`, то нужно, чтобы функция, вычисляющая длину, возвращала зависимую пару (n Vect n a). Тогда ты сможешь вручную проверить, что n действительно равно пяти, и если так, передать уже вектор в функцию.
С другой стороны, можно и доказывать, что данные обладают требуемым функцией свойствами. Список, к которому добавили элемент не может быть пустым, остаток от деления меньше делителя, моноидальная операция чего-либо с нейтральным элементом вернёт то самое «чего-либо» и так далее.
> вычитать их можно? а если 0 - 1
В принципе, вычитание могло бы требовать доказательства, что первое число не меньше второго, но в Idris сделали всё довольно топорно.
Я слышал, что в agde охуенно удобно строить edsl'и.
Хотелось бы увидеть пример такого на какой-нибудь приближенной к реальности задаче, а не факториалах.
Хотелось бы увидеть пример такого на какой-нибудь приближенной к реальности задаче, а не факториалах.
>>484153
По-твоему лучше бы тред шёл в своём прежнем рейдж-русле? Все же началось с того что int в темпейте это совсем не то что нужно.
Но да сравнение забавное.
По-твоему лучше бы тред шёл в своём прежнем рейдж-русле? Все же началось с того что int в темпейте это совсем не то что нужно.
Но да сравнение забавное.
>>484147
Idris больше направлен в сторону DSL. Но приближённый к реальной задаче пример доставить не могу.
Idris больше направлен в сторону DSL. Но приближённый к реальной задаче пример доставить не могу.
>>484156
Я не про содержание треда, просто интересно в очередной раз наблюдать типичное поведение крестовика/лиспера при обсуждении какой-то фичи: статическая типизация — ой, да можно на макросах сделать; сопоставление с образцом — да хуйня, за пару деньков на шаблонах/макросах можно накидать; зависимые типы — я в крестах могу такое сделать.
И иногда это "можнозделоть" даже выливается в полурабочую горстку костылей, отдаленно напоминающую предмет разговора. Но даже при всей очевидности их неприменимости на практике, фанатичная убежденность лишпера/крестоблядка во всемогуществе, всепременимости и безальтернативности его предмета обожания остается непробиваемой.
Я не про содержание треда, просто интересно в очередной раз наблюдать типичное поведение крестовика/лиспера при обсуждении какой-то фичи: статическая типизация — ой, да можно на макросах сделать; сопоставление с образцом — да хуйня, за пару деньков на шаблонах/макросах можно накидать; зависимые типы — я в крестах могу такое сделать.
И иногда это "можнозделоть" даже выливается в полурабочую горстку костылей, отдаленно напоминающую предмет разговора. Но даже при всей очевидности их неприменимости на практике, фанатичная убежденность лишпера/крестоблядка во всемогуществе, всепременимости и безальтернативности его предмета обожания остается непробиваемой.
>>484184
Кто-то и без меня уже начал: https://gist.github.com/david-christiansen/3660d5d45e9287c25a5e
Кто-то и без меня уже начал: https://gist.github.com/david-christiansen/3660d5d45e9287c25a5e
>>484188
Ну это чушь какая-то. Где доказательство того, что она корректную последовательность на экране напечатает? Его нет. Есть доказательство тривиальных фактов из арифметики.
Ну это чушь какая-то. Где доказательство того, что она корректную последовательность на экране напечатает? Его нет. Есть доказательство тривиальных фактов из арифметики.
>>484192
Для этого нужно как минимум переписать компилятор idris на idris и полностью покрыть доказательствами.
> Где доказательство того, что она корректную последовательность на экране напечатает?
Для этого нужно как минимум переписать компилятор idris на idris и полностью покрыть доказательствами.
>>484193
Дык. Не надо тогда нам лапшу на уши вешать. Физбаз он верифицировать может. Эта задача находится далеко за пределами возможностей таких систем.
А то доказательство про тупую реализацию остатка от деления можно было написать и на системах двадцатилетней давности. Собственно с тех пор ничего не изменилось. Толкут воду в ступе с умным видом.
Дык. Не надо тогда нам лапшу на уши вешать. Физбаз он верифицировать может. Эта задача находится далеко за пределами возможностей таких систем.
А то доказательство про тупую реализацию остатка от деления можно было написать и на системах двадцатилетней давности. Собственно с тех пор ничего не изменилось. Толкут воду в ступе с умным видом.
>>484130
Ну так запилят же вроде скоро. Алсо, D.
> кроме зависмости типа он ещё предоставляет некоторые проверки
Ну так запилят же вроде скоро. Алсо, D.
Увы, подобные треды вредны для человечества. Они по факту являются необоснованным и ничем не подкреплённым разогревом интереса к профессии. Но вот беда: на практике это всё нахуй не нужно, а наличие зависимых типов на дваче никоим образом не делает программирование более интересной и интеллектуальной работой.
>>484195
А вот это тебе следует обосновать.
> Эта задача находится далеко за пределами возможностей таких систем.
А вот это тебе следует обосновать.
>>484394
Понятие печати текста в консоль нигде не формализовано. Но это еще простой случай, а вот если программа будет содержать интерактивные или графические элементы - тут вообще кранты.
Понятие печати текста в консоль нигде не формализовано. Но это еще простой случай, а вот если программа будет содержать интерактивные или графические элементы - тут вообще кранты.
2014 Кб, 2776x2464
>>484425
Можно эмулировать оборудование вроде пикрелейта и на самом деле юникс-подобные ОС это и делают, у него спецификации должны быть.
а вообще, просто предполагается, что среда, в которой запускается программа, идеальна, проверяется, что программа корректно взаимодействует со средой, и на этом, вообще говоря, задача верификации завершена
> Понятие печати текста в консоль нигде не формализовано.
Можно эмулировать оборудование вроде пикрелейта и на самом деле юникс-подобные ОС это и делают, у него спецификации должны быть.
а вообще, просто предполагается, что среда, в которой запускается программа, идеальна, проверяется, что программа корректно взаимодействует со средой, и на этом, вообще говоря, задача верификации завершена
>>483873
Тред не читал, сразу отвечал. Не слушай петухов, в крестах есть зависимые типы, полиморфные (или шаблонные, как принято называть их в крестах) функции - один из примеров. Другое дело, что в С++ типы могут зависеть только от других типов (или констант времени компиляции, которые по сути эквивалентны типам), а в языках с полноценной поддержкой - от любого выражения. И да, не от значения а от выражения, это важно, потому что рантайм-значение на момент компиляции не известно.
Тред не читал, сразу отвечал. Не слушай петухов, в крестах есть зависимые типы, полиморфные (или шаблонные, как принято называть их в крестах) функции - один из примеров. Другое дело, что в С++ типы могут зависеть только от других типов (или констант времени компиляции, которые по сути эквивалентны типам), а в языках с полноценной поддержкой - от любого выражения. И да, не от значения а от выражения, это важно, потому что рантайм-значение на момент компиляции не известно.
>но и доказывать корректность их реализации
Ну докажи мне корректность гостевухи или цмски, например.
>>484207
Лисп, хаскель, алгоритмы, олимпиадки, архитектурка - это всё этакое самопорождённое и самоподдерживающееся ассоциативное чёрное SMM от быдлокодинга.
Вот вам красивый аналог попроще: http://vk.com/anime_onlineparty
Хаскешиз? Гоу нырять в энтерпрайз-парашу на скале, ведь у нас есть scalaz, а теперь и cats!
Схемофаз? Гоу пилить круды на рельсах, ведь в раби есть callcc и вообще дух метапетушения выдержан!
Лисп, хаскель, алгоритмы, олимпиадки, архитектурка - это всё этакое самопорождённое и самоподдерживающееся ассоциативное чёрное SMM от быдлокодинга.
Вот вам красивый аналог попроще: http://vk.com/anime_onlineparty
Хаскешиз? Гоу нырять в энтерпрайз-парашу на скале, ведь у нас есть scalaz, а теперь и cats!
Схемофаз? Гоу пилить круды на рельсах, ведь в раби есть callcc и вообще дух метапетушения выдержан!
>>484505
Нашел таки тусовку?
Нашел таки тусовку?
>>484460
Это называется параметрическим полиморфизмом. Хотя он формально и относится к некоторому подмножеству зависимых типов, к языкам с зависимыми типами относят именно те, что позволяют зависеть от выражения.
> Другое дело, что в С++ типы могут зависеть только от других типов
Это называется параметрическим полиморфизмом. Хотя он формально и относится к некоторому подмножеству зависимых типов, к языкам с зависимыми типами относят именно те, что позволяют зависеть от выражения.
>>484473
Ты, наверное, хотел спросить в чем принципиальная разница между языками, в которых типы как-то ограничены, и теми, в которых тип может быть представлен произвольным выражением. В сложности алгоритма проверки типов главным образом (и как следствие - в геморе использования такого языка). Если типы - простые значения, их можно просто сравнивать, например Int не равен String. Если там выражения, то их надо как-то унифицировать, чтобы понять эквивалентны они или нет, в некоторых случаях это вообще неразрешимая задача.
>>484528
Что значит "зависеть от выражения"? Тащем-то тип полиморфной функции зависит от типов аргументов.
>В чем принципиальная разница между выражением и типом?
Ты, наверное, хотел спросить в чем принципиальная разница между языками, в которых типы как-то ограничены, и теми, в которых тип может быть представлен произвольным выражением. В сложности алгоритма проверки типов главным образом (и как следствие - в геморе использования такого языка). Если типы - простые значения, их можно просто сравнивать, например Int не равен String. Если там выражения, то их надо как-то унифицировать, чтобы понять эквивалентны они или нет, в некоторых случаях это вообще неразрешимая задача.
>>484528
Что значит "зависеть от выражения"? Тащем-то тип полиморфной функции зависит от типов аргументов.
>>484534
Да, только вот в большинстве языков тип не может быть представлен произвольным выражением, пусть даже гарантируемо вычислимым.
> Тащем-то тип полиморфной функции зависит от типов аргументов
Да, только вот в большинстве языков тип не может быть представлен произвольным выражением, пусть даже гарантируемо вычислимым.
Сьебите в /sci/, больные ублюдки.
Бамп.
>>485133
В скале есть path dependent types (http://stackoverflow.com/questions/24960722/what-is-the-difference-between-path-dependent-types-and-dependent-types, http://stackoverflow.com/questions/12935731/any-reason-why-scala-does-not-explicitly-support-dependent-types) и, кроме того, есть https://github.com/lampepfl/dotty.
Так что, может быть, можно сделать, но в том же Idris'е всё это проще и естественнее.
В скале есть path dependent types (http://stackoverflow.com/questions/24960722/what-is-the-difference-between-path-dependent-types-and-dependent-types, http://stackoverflow.com/questions/12935731/any-reason-why-scala-does-not-explicitly-support-dependent-types) и, кроме того, есть https://github.com/lampepfl/dotty.
Так что, может быть, можно сделать, но в том же Idris'е всё это проще и естественнее.
Бамп.
Я так и не понял зачем все это петушение нужно.
Кто-нибудь покажите рабочий production код, где эти ваши типы реально используются, и для сравнения тот же код без их использования.
Кто-нибудь покажите рабочий production код, где эти ваши типы реально используются, и для сравнения тот же код без их использования.
>>484534
Все равно не очень понял. Вернемся к тому примеру с массивом, там было выражение n. Первый крестобог попытался это выразить в виде template<int n, class a>, что неверно. Но можно же сделать, скажем, template<class Expression, class a> где в качестве Expression можно задавать, например, Variable<"N"> или Plus<Variable<"N">, Constant<1>>. Т.е. сделать на шаблонах систему выражений. Чем это будет отличаться тогда от настоящих зависимых типов?
Все равно не очень понял. Вернемся к тому примеру с массивом, там было выражение n. Первый крестобог попытался это выразить в виде template<int n, class a>, что неверно. Но можно же сделать, скажем, template<class Expression, class a> где в качестве Expression можно задавать, например, Variable<"N"> или Plus<Variable<"N">, Constant<1>>. Т.е. сделать на шаблонах систему выражений. Чем это будет отличаться тогда от настоящих зависимых типов?
>>486420
Попробуй, лол. Не забывай, что тебе по этим выражениям ещё корректность доказывать. И всё это писать на ебанутом языке шаблонов.
Тем, что это будет кривая и неюзабельная хуита, головной и жопной боли от которой в разы больше, чем пользы
хотя плюсоёбам не привыкать.
Алсо, страшно представить, какими простынями будет плеваться компилятор при ошибках.
>сделать на шаблонах систему выражений.
Попробуй, лол. Не забывай, что тебе по этим выражениям ещё корректность доказывать. И всё это писать на ебанутом языке шаблонов.
>Чем это будет отличаться тогда от настоящих зависимых типов?
Тем, что это будет кривая и неюзабельная хуита, головной и жопной боли от которой в разы больше, чем пользы
>Plus<Variable<"N">, Constant<1>>
хотя плюсоёбам не привыкать.
Алсо, страшно представить, какими простынями будет плеваться компилятор при ошибках.
>>486503
Что там пробовать? Ты сомневаешься, что можно нафигачить шаблонных классов для всех действий и т.д.?
Вот тут бы поподробнее. Какие именно манипуляции в твоих языках возможны? Как их применять?
На шаблонах можно много чего сделать.
Слабовато. У тебя есть два пути.
1)
Ясно.
2)
Вот теперь тебя люблю я!
Пока что я вижу скорее 1).
>Попробуй, лол.
Что там пробовать? Ты сомневаешься, что можно нафигачить шаблонных классов для всех действий и т.д.?
>Не забывай, что тебе по этим выражениям ещё корректность доказывать.
Вот тут бы поподробнее. Какие именно манипуляции в твоих языках возможны? Как их применять?
На шаблонах можно много чего сделать.
>Тем, что это будет кривая и неюзабельная хуита, головной и жопной боли от которой в разы больше, чем пользы
Слабовато. У тебя есть два пути.
1)
>Вот вам язык. Его основная фича - сахарок для одной эзотерической операции. Эту операцию вообще-то можно реализовать и стандартными средствами крестов, но этого никто не делает, потому что это никому не нужно.
Ясно.
2)
>Вот вам язык. Его основная фича, Х, позволяет делать У, что невозможно на других языках. Вот простой абстрактный пример: ... А вот пример того, как этим можно воспользоваться в реальном проекте: ... На других языках полный аналог этих примеров написать нельзя.
Вот теперь тебя люблю я!
Пока что я вижу скорее 1).
224 Кб, 552x830
>>486642
Спермопроблемы.
Спермопроблемы.
>>486620
Можносделать зашкаливает! Ну и нафигачь, давай. Но мы-то знаем, что ничего, что можно было бы назвать зависимыми типами, у тебя не получится.
Слабовато. У тебя есть один путь: можносделать, но никто не делает и не будет делать из-за, ВНЕЗАПНО, уёбищности крестов, усложняющих и без того сложную задачу, из-за уёбищности результата, который в и без того уёбищных крестах никто в здравом уме использовать не будет.
>Ты сомневаешься, что можно нафигачить шаблонных классов для всех действий и т.д.?
>можно нафигачить
>На шаблонах можно много чего сделать.
Можносделать зашкаливает! Ну и нафигачь, давай. Но мы-то знаем, что ничего, что можно было бы назвать зависимыми типами, у тебя не получится.
>>Тем, что это будет кривая и неюзабельная хуита, головной и жопной боли от которой в разы больше, чем пользы
>Слабовато. У тебя есть два пути.
Слабовато. У тебя есть один путь: можносделать, но никто не делает и не будет делать из-за, ВНЕЗАПНО, уёбищности крестов, усложняющих и без того сложную задачу, из-за уёбищности результата, который в и без того уёбищных крестах никто в здравом уме использовать не будет.
140 Кб, 1263x776
Почему rewrite не срабатывает?
И еще интереснее, почему нет никаких сообщений по этому поводу?
И еще интереснее, почему нет никаких сообщений по этому поводу?
1 Кб, 330x19
И еще. WTF? Зависимые типы ебут мое корыто, даже во время простоя (просто запущен repl, никаких операций не выполняется). Очень хотелось бы их угомонить.
>>486736
Да, переименовали (что вполне естественно, так как типы и конструкторы везде с большой буквы).
> Я правильно понимаю, что они решили переименовать refl в Refl?
Да, переименовали (что вполне естественно, так как типы и конструкторы везде с большой буквы).
>>486736
Хм, смутила надпись (Admin) в заголовке и значок UAC в табе.
Хм, смутила надпись (Admin) в заголовке и значок UAC в табе.
Бамп.
Я понял!!! Андрюше нужно писать на PHP! Ведь как учит языки нормальный человек: лисп (аморфная красота) -> хаскель (строгая красота) -> агда (математически строгая красота). А история Андрюши очень трагичная, братюни. Сначала все начиналось хорошо: общелисп -> хаскель -> скала + агда. Помню даже писал Андрюша пасты про то, что хотел бы соседа лиспера на дачу, потому что лисперы слишком практичные.
Но потом что-то пошло не так: -> хаскель -> кресты -> джаваскрипт -> питон.
И я все ломал голову, как человек может так ненавидеть красивое и сложное, так хотеть деградации, что пишет на питоне? Но для Андрюши практичное уродство и есть красота. А дальше PHP, Verilog, соцреализм, диктатура пролетариата и экономическое чудо по китайскому образцу. Скай из зе лимит!
Но потом что-то пошло не так: -> хаскель -> кресты -> джаваскрипт -> питон.
И я все ломал голову, как человек может так ненавидеть красивое и сложное, так хотеть деградации, что пишет на питоне? Но для Андрюши практичное уродство и есть красота. А дальше PHP, Verilog, соцреализм, диктатура пролетариата и экономическое чудо по китайскому образцу. Скай из зе лимит!
на ваших зависимых типах можно зделать так:
data Img = Img {
width :: Nat,
height :: Nat,
pixels :: Vec (width * height) Pixel
}
чтоб width и height не были известны на этапе компиляции?
data Img = Img {
width :: Nat,
height :: Nat,
pixels :: Vec (width * height) Pixel
}
чтоб width и height не были известны на этапе компиляции?
>>487807
да
да
1
>>487189
Всё хорошо до тех пор, пока игнорируешь цели программирования. Как только включаешь ЦЕЛЕСООБРАЗНОСТЬ, так сразу вдруг обнаруживаются удивительные вещи: что на ноджс и петоне все программы пишутся в 100 раз быстрее, работают производительнее, код гораздо чище, проще, и поддерживаемее, библиотеки для всего уже написаны, и так далее.
Нет, суть не в том, что это красиво, а в том, что попытки искать в программировании красоту - глупые и обречены на провал. Сколько такой хуйнёй не страдай, тебе потом ноджсник или питонщик за вечер по губам проведёт, решив ту же задачу гораздо проще и компактнее. И твоя красота сливается по полной, потому что сил в неё вбухано намного больше, а для других программистов она сложнее и трудноподдерживаемее. Не все настолько изощрены в искусстве отрицания и самообмана, чтобы упорно продолжать в том же духе даже после многочисленных подобных отсосов.
Любителям красоты могу только посочувствовать и посоветовать перекат в области, где искусство ради искусства, где композиция выразительных элементов - сама цель деятельности, а критерии её качества - "красиво", "интересно", "прикольно", и так далее. Причём не обязательно в качестве производителя. Можно просто быть потребителем и соревноваться в элитности вкусов, наслушанности, начинатанности, количестве просмотренных тайтлов, глубоком анализе деталей такой-то серии такой-то анимы, открывающем абсолютно альтернативную трактовку сюжета, умении видеть 100500 отсылок к творчеству других писателей или мифологии, вкладывать в семиотические структуры такое содержание, которое даже автор открытого текста не мог себе представить, знании поджанров, музыкальной теории, умении сдетектировать ритм, инструменты, эффекты, классифицировать трек как комбинацию таких-то поджанровых тегов и накатать техничную рецензию в духе allmusic и так далее. Искусство и существует ради красоты, глубины, интересности, а вот программирование - оно не для этого. Программирование существует ради того, чтобы решать скучные бытовые инфраструктурные проблемки, являющиеся препятствием на пути к развлечениям и искусству. И чем проще и быстрее это делать, тем больше времени и сил будет оставаться на то, ради чего, собственно, всё и затевалось.
Всё хорошо до тех пор, пока игнорируешь цели программирования. Как только включаешь ЦЕЛЕСООБРАЗНОСТЬ, так сразу вдруг обнаруживаются удивительные вещи: что на ноджс и петоне все программы пишутся в 100 раз быстрее, работают производительнее, код гораздо чище, проще, и поддерживаемее, библиотеки для всего уже написаны, и так далее.
> уродство и есть красота
Нет, суть не в том, что это красиво, а в том, что попытки искать в программировании красоту - глупые и обречены на провал. Сколько такой хуйнёй не страдай, тебе потом ноджсник или питонщик за вечер по губам проведёт, решив ту же задачу гораздо проще и компактнее. И твоя красота сливается по полной, потому что сил в неё вбухано намного больше, а для других программистов она сложнее и трудноподдерживаемее. Не все настолько изощрены в искусстве отрицания и самообмана, чтобы упорно продолжать в том же духе даже после многочисленных подобных отсосов.
Любителям красоты могу только посочувствовать и посоветовать перекат в области, где искусство ради искусства, где композиция выразительных элементов - сама цель деятельности, а критерии её качества - "красиво", "интересно", "прикольно", и так далее. Причём не обязательно в качестве производителя. Можно просто быть потребителем и соревноваться в элитности вкусов, наслушанности, начинатанности, количестве просмотренных тайтлов, глубоком анализе деталей такой-то серии такой-то анимы, открывающем абсолютно альтернативную трактовку сюжета, умении видеть 100500 отсылок к творчеству других писателей или мифологии, вкладывать в семиотические структуры такое содержание, которое даже автор открытого текста не мог себе представить, знании поджанров, музыкальной теории, умении сдетектировать ритм, инструменты, эффекты, классифицировать трек как комбинацию таких-то поджанровых тегов и накатать техничную рецензию в духе allmusic и так далее. Искусство и существует ради красоты, глубины, интересности, а вот программирование - оно не для этого. Программирование существует ради того, чтобы решать скучные бытовые инфраструктурные проблемки, являющиеся препятствием на пути к развлечениям и искусству. И чем проще и быстрее это делать, тем больше времени и сил будет оставаться на то, ради чего, собственно, всё и затевалось.
>>487189
Всё хорошо до тех пор, пока игнорируешь цели программирования. Как только включаешь ЦЕЛЕСООБРАЗНОСТЬ, так сразу вдруг обнаруживаются удивительные вещи: что на ноджс и петоне все программы пишутся в 100 раз быстрее, работают производительнее, код гораздо чище, проще, и поддерживаемее, библиотеки для всего уже написаны, и так далее.
Нет, суть не в том, что это красиво, а в том, что попытки искать в программировании красоту - глупые и обречены на провал. Сколько такой хуйнёй не страдай, тебе потом ноджсник или питонщик за вечер по губам проведёт, решив ту же задачу гораздо проще и компактнее. И твоя красота сливается по полной, потому что сил в неё вбухано намного больше, а для других программистов она сложнее и трудноподдерживаемее. Не все настолько изощрены в искусстве отрицания и самообмана, чтобы упорно продолжать в том же духе даже после многочисленных подобных отсосов.
Любителям красоты могу только посочувствовать и посоветовать перекат в области, где искусство ради искусства, где композиция выразительных элементов - сама цель деятельности, а критерии её качества - "красиво", "интересно", "прикольно", и так далее. Причём не обязательно в качестве производителя. Можно просто быть потребителем и соревноваться в элитности вкусов, наслушанности, начинатанности, количестве просмотренных тайтлов, глубоком анализе деталей такой-то серии такой-то анимы, открывающем абсолютно альтернативную трактовку сюжета, умении видеть 100500 отсылок к творчеству других писателей или мифологии, вкладывать в семиотические структуры такое содержание, которое даже автор открытого текста не мог себе представить, знании поджанров, музыкальной теории, умении сдетектировать ритм, инструменты, эффекты, классифицировать трек как комбинацию таких-то поджанровых тегов и накатать техничную рецензию в духе allmusic и так далее. Искусство и существует ради красоты, глубины, интересности, а вот программирование - оно не для этого. Программирование существует ради того, чтобы решать скучные бытовые инфраструктурные проблемки, являющиеся препятствием на пути к развлечениям и искусству. И чем проще и быстрее это делать, тем больше времени и сил будет оставаться на то, ради чего, собственно, всё и затевалось.
Всё хорошо до тех пор, пока игнорируешь цели программирования. Как только включаешь ЦЕЛЕСООБРАЗНОСТЬ, так сразу вдруг обнаруживаются удивительные вещи: что на ноджс и петоне все программы пишутся в 100 раз быстрее, работают производительнее, код гораздо чище, проще, и поддерживаемее, библиотеки для всего уже написаны, и так далее.
> уродство и есть красота
Нет, суть не в том, что это красиво, а в том, что попытки искать в программировании красоту - глупые и обречены на провал. Сколько такой хуйнёй не страдай, тебе потом ноджсник или питонщик за вечер по губам проведёт, решив ту же задачу гораздо проще и компактнее. И твоя красота сливается по полной, потому что сил в неё вбухано намного больше, а для других программистов она сложнее и трудноподдерживаемее. Не все настолько изощрены в искусстве отрицания и самообмана, чтобы упорно продолжать в том же духе даже после многочисленных подобных отсосов.
Любителям красоты могу только посочувствовать и посоветовать перекат в области, где искусство ради искусства, где композиция выразительных элементов - сама цель деятельности, а критерии её качества - "красиво", "интересно", "прикольно", и так далее. Причём не обязательно в качестве производителя. Можно просто быть потребителем и соревноваться в элитности вкусов, наслушанности, начинатанности, количестве просмотренных тайтлов, глубоком анализе деталей такой-то серии такой-то анимы, открывающем абсолютно альтернативную трактовку сюжета, умении видеть 100500 отсылок к творчеству других писателей или мифологии, вкладывать в семиотические структуры такое содержание, которое даже автор открытого текста не мог себе представить, знании поджанров, музыкальной теории, умении сдетектировать ритм, инструменты, эффекты, классифицировать трек как комбинацию таких-то поджанровых тегов и накатать техничную рецензию в духе allmusic и так далее. Искусство и существует ради красоты, глубины, интересности, а вот программирование - оно не для этого. Программирование существует ради того, чтобы решать скучные бытовые инфраструктурные проблемки, являющиеся препятствием на пути к развлечениям и искусству. И чем проще и быстрее это делать, тем больше времени и сил будет оставаться на то, ради чего, собственно, всё и затевалось.
>>487833
Фантазии или так и есть - на самом деле не принципиально. Важно, какие ценности в программировании неуместны, и следующий из этого вывод, что программирование не стоит того, чтобы им вообще так заморачиваться. Можно не программировать - лучше не программировать. Если есть способ решить задачу или заработать деньги проще - лучше так и сделать.
Фантазии или так и есть - на самом деле не принципиально. Важно, какие ценности в программировании неуместны, и следующий из этого вывод, что программирование не стоит того, чтобы им вообще так заморачиваться. Можно не программировать - лучше не программировать. Если есть способ решить задачу или заработать деньги проще - лучше так и сделать.
>>487841
Можно зарабатывать кодингом, а увлекаться чем-то другим, как большинство и делает, но это слишком напряжно и лучше пробовать другие варианты:
- work smarter not harder, всякие экзотические разовые аналитические проекты и консалтинг
- работа, где большую часть рабочего времени можешь заниматься своими делами, типа сисадминства, эникейства, охранников
- фриланс и ситуационные подработки когда нужна лавешка - здесь может быть и быдлокодинг, и консалтинг, и естественноязыковые переводы, и дофига чего
и так далее
Можно зарабатывать кодингом, а увлекаться чем-то другим, как большинство и делает, но это слишком напряжно и лучше пробовать другие варианты:
- work smarter not harder, всякие экзотические разовые аналитические проекты и консалтинг
- работа, где большую часть рабочего времени можешь заниматься своими делами, типа сисадминства, эникейства, охранников
- фриланс и ситуационные подработки когда нужна лавешка - здесь может быть и быдлокодинг, и консалтинг, и естественноязыковые переводы, и дофига чего
и так далее
>>487851
Зато я ебал твою мамашу.
Зато я ебал твою мамашу.
>>487851
Просто все тут конченые шизики, но некоторые начинают что-то подозревать. И кому посчастливилось забраться достаточно высоко на мета-уровень, тот видит, что на той стороне реки люди сходят с ума гораздо веселее. Совсем не быть ёбнутым аутистом здесь у кого-то получится вряд ли, но существенно улучшить качество своей жизни, оказывается, несложно.
Просто все тут конченые шизики, но некоторые начинают что-то подозревать. И кому посчастливилось забраться достаточно высоко на мета-уровень, тот видит, что на той стороне реки люди сходят с ума гораздо веселее. Совсем не быть ёбнутым аутистом здесь у кого-то получится вряд ли, но существенно улучшить качество своей жизни, оказывается, несложно.
На самом деле здесь все просто забыли, что в первую очередь эти языки исследовательские и задачи у них другие.
>>486620
Попробуй нафигачить следующее:
1. Тип Vector, параметризованный длиной – это можназделоть, уже видели.
2. Конкатенация векторов и, допустим, их скалярное произведение – тоже без проблем.
3. В main'е:
3a. Получаем из консоли два числа n и m;
3b. Делаем вектор a длины n и вектор b длины m (чем инициализировать – не важно);
3c. Должно компилироваться: a a, b b, cat(a, b) cat(b, a)
3d. Не должно компилироваться: a b, cat(a, a) cat(a, b)
3e. Самая мякотка: желательно должно компилироваться: if (n == m) {a b;} или какой-то аналог на шаблонах
Эквивалентную идрисню подгоню, если надо.
<i>мимо языкоёб</i>
Попробуй нафигачить следующее:
1. Тип Vector, параметризованный длиной – это можназделоть, уже видели.
2. Конкатенация векторов и, допустим, их скалярное произведение – тоже без проблем.
3. В main'е:
3a. Получаем из консоли два числа n и m;
3b. Делаем вектор a длины n и вектор b длины m (чем инициализировать – не важно);
3c. Должно компилироваться: a a, b b, cat(a, b) cat(b, a)
3d. Не должно компилироваться: a b, cat(a, a) cat(a, b)
3e. Самая мякотка: желательно должно компилироваться: if (n == m) {a b;} или какой-то аналог на шаблонах
Эквивалентную идрисню подгоню, если надо.
<i>мимо языкоёб</i>
>>487901
Макаба разметку съела. Ты имел в виду
?
Макаба разметку съела. Ты имел в виду
> Должно компилироваться: a ∗∗ a, b ∗∗ b, cat(a, b) ∗∗ cat(b, a)
?
>>487897
Да, только вот у idris это исследование на тему практического применения зависимых типов в программировании. Поэтому, к примеру, в языке есть классы типов.
> в первую очередь эти языки исследовательские
Да, только вот у idris это исследование на тему практического применения зависимых типов в программировании. Поэтому, к примеру, в языке есть классы типов.
>>487916
Классы зависимых типов – это охуенчик, кстати. Можно в «интерфейс» помимо собственно методов их инварианты добавлять. Что-то типа:
[code]
class Monoid m where
mempty : m
mappend : m -> m -> m
rightUnit : m -> mappend m mempty = m
leftUnit : m -> mappend mempty m = m
assoc : m1 -> m2 -> m3 -> mappend (mappend m1 m2) m3 = mappend m1 (mappend m2 m3)
[/code]
Классы зависимых типов – это охуенчик, кстати. Можно в «интерфейс» помимо собственно методов их инварианты добавлять. Что-то типа:
[code]
class Monoid m where
mempty : m
mappend : m -> m -> m
rightUnit : m -> mappend m mempty = m
leftUnit : m -> mappend mempty m = m
assoc : m1 -> m2 -> m3 -> mappend (mappend m1 m2) m3 = mappend m1 (mappend m2 m3)
[/code]
>>487822
Напоминаю бедняшам
Ruby on Rails - популярный Ruby фреймворк ........................~200k loc
Yesod - популярный Haskell фреймворк..................................~20k loc
Roslyn - компилятор C#/VB ................................................~2 800k loc
GHC - компилятор Haskell .....................................................~200k loc
git - VCS на C ......................................................................~360k loc
darcs - VCS на Haskell ............................................................~36k loc
Любая программа на любом говноязыке .................................... X loc
Та же программа на хаскеле .................................................... X/10 loc
Напоминаю бедняшам
Ruby on Rails - популярный Ruby фреймворк ........................~200k loc
Yesod - популярный Haskell фреймворк..................................~20k loc
Roslyn - компилятор C#/VB ................................................~2 800k loc
GHC - компилятор Haskell .....................................................~200k loc
git - VCS на C ......................................................................~360k loc
darcs - VCS на Haskell ............................................................~36k loc
Любая программа на любом говноязыке .................................... X loc
Та же программа на хаскеле .................................................... X/10 loc
>>487917
Думаю, поэлементное умножение векторов будет даже нагляднее.
Думаю, поэлементное умножение векторов будет даже нагляднее.
>>487901
Подгони плз. Попробую сделать на крестах.
3е будет не простым if, конечно, а шаблонной магией.
>Эквивалентную идрисню подгоню, если надо.
Подгони плз. Попробую сделать на крестах.
3е будет не простым if, конечно, а шаблонной магией.
>>486746
Если вдруг кому интересны мои приключения, я нашел вроде бы релевантный тред
http://idris-lang.narkive.com/LLtIfcTx/homomorphism-transitivity-proof
Пара релевантных цитат от туда
и
видимо зависимые типы не дают достаточно пощекотать анус, поэтому решили оторваться в тактиках
Я думаю что пока отложу Idris на годик может они за это время допилят ( >>486746 >>486754 ) и лучше с петухом побалуюсь.
Если вдруг кому интересны мои приключения, я нашел вроде бы релевантный тред
http://idris-lang.narkive.com/LLtIfcTx/homomorphism-transitivity-proof
Пара релевантных цитат от туда
> Each invocation of (<+>) has an implicit argument representing the dictionary that will implement the operation. These are not necessarily identical, even for the same type!
и
> Rewrites don't fail in the prover - they just have no effect. Perhaps this should be changed!
видимо зависимые типы не дают достаточно пощекотать анус, поэтому решили оторваться в тактиках
Я думаю что пока отложу Idris на годик может они за это время допилят ( >>486746 >>486754 ) и лучше с петухом побалуюсь.
>>487942
И ни одного issue на гитхабе (хотя, может плохо искал?). Может, стоит создать один?
сам думал поиграться с доказательством сортировки слиянием, но для этого надо ждать https://github.com/idris-lang/Idris-dev/pull/2205
> idris-lang@googlegroups.com
И ни одного issue на гитхабе (хотя, может плохо искал?). Может, стоит создать один?
сам думал поиграться с доказательством сортировки слиянием, но для этого надо ждать https://github.com/idris-lang/Idris-dev/pull/2205
>>487930
http://pastebin.com/XGfF9PYW комментировать было лень, но если что, спрашивай. Вектор в стандартной библиотеке есть, решил завелосипедить для наглядности; Nat не стал. Идея такая, что в общем случае компилятор нихрена не знает, что длины равны, но мы можем ему это доказать – статически, при помощи теорем (например, о коммутативности сложения), или динамически, при помощи вычислимого равенства (DecEq).
http://pastebin.com/XGfF9PYW комментировать было лень, но если что, спрашивай. Вектор в стандартной библиотеке есть, решил завелосипедить для наглядности; Nat не стал. Идея такая, что в общем случае компилятор нихрена не знает, что длины равны, но мы можем ему это доказать – статически, при помощи теорем (например, о коммутативности сложения), или динамически, при помощи вычислимого равенства (DecEq).
>>487997
Замени `print` на `printLn`, чтобы вывод читать можно было.
Замени `print` на `printLn`, чтобы вывод читать можно было.
>>487901
http://dpaste.dzfl.pl/c6859709dc9d
Альфа-версия шаблоно-дрисни, всё чек кроме 3e, 3е так просто не получится, надо вводить какой-то контекст ограничений на n и m. Ну и доказательство теорем надо накодить нормальное, а не ололо-перебором, но это имхо можнозделоть.
МОЖНОЗДЕЛОТЬ нормальный разбор строки выражения (n + m) k тоже.
Потратил часа 3, но я тупой и на D мало кодил.
Интересно, как будет выглядеть подобная хуита на крестах.
http://dpaste.dzfl.pl/c6859709dc9d
Альфа-версия шаблоно-дрисни, всё чек кроме 3e, 3е так просто не получится, надо вводить какой-то контекст ограничений на n и m. Ну и доказательство теорем надо накодить нормальное, а не ололо-перебором, но это имхо можнозделоть.
> Bin!(Bin!(Sym!"n", "+", Sym!"m"), "", Sym!"k")
МОЖНОЗДЕЛОТЬ нормальный разбор строки выражения (n + m) k тоже.
Потратил часа 3, но я тупой и на D мало кодил.
Интересно, как будет выглядеть подобная хуита на крестах.
>>488021
Можнозделоть реализацию Idris на шаблонах. Наверное можно.
> 3е так просто не получится, надо вводить какой-то контекст ограничений на n и m. Ну и доказательство теорем надо накодить нормальное, а не ололо-перебором, но это имхо можнозделоть.
Можнозделоть реализацию Idris на шаблонах. Наверное можно.
>>488022
Я лично уверен, что всё можно. Не будет так удобно, но можно, хоть обкукарекайтесь что нельзя. За 3 часа нахуячил рабочий proof-of-concept, сколько твой Idris пилят?
Я лично уверен, что всё можно. Не будет так удобно, но можно, хоть обкукарекайтесь что нельзя. За 3 часа нахуячил рабочий proof-of-concept, сколько твой Idris пилят?
Жду короч похожую крестодрисню от крестобога. После этого обсуждение того, что на шаблонах что-то ненужное НИЛЬЗЯЗДЕЛОТЬ можно считать закрытым.
Игрушечный язык с зависимыми типами не так уж трудно запилить, кстати:
https://github.com/sweirich/pi-forall/
https://github.com/david-christiansen/tiny-dependent-types
https://github.com/sweirich/pi-forall/
https://github.com/david-christiansen/tiny-dependent-types
>>488031
Смотрел лекции pi-forall и не сказал бы что прям охуеть как просто.
+ там только тайпчекер
+ там несколько версий и есть баги
Смотрел лекции pi-forall и не сказал бы что прям охуеть как просто.
+ там только тайпчекер
+ там несколько версий и есть баги
>>488036
Если завозить, то лучше сразу вот такие: http://www.cs.ru.nl/dtp11/slides/trojahner.pdf
То же, что и в хаскеле — аппликацию.
> Массивов не завезли?
Если завозить, то лучше сразу вот такие: http://www.cs.ru.nl/dtp11/slides/trojahner.pdf
> Знак доллара что обозначает?
То же, что и в хаскеле — аппликацию.
>>488045
`idris --execute foo.idr`
`idris --execute foo.idr`
>>488022
Можно хоть на брэйнфаке, только не нужно
Можно хоть на брэйнфаке, только не нужно
>>488021
Чет на том сайте не работает, что бы я ни вводил в инпут, пишет:
Application error:
std.conv.ConvException@/opt/compilers/dmd2/include/std/conv.d(1684): Unexpected '
' when converting from type string to type uint
Чет на том сайте не работает, что бы я ни вводил в инпут, пишет:
Application error:
std.conv.ConvException@/opt/compilers/dmd2/include/std/conv.d(1684): Unexpected '
' when converting from type string to type uint
>>488025
Зделоть-то на любой полной по Тьюрингу параше можно, а вот сделать пригодным для использования в пределах крестах, не переизобретая поверх них нового языка, никак не выйдет.
Зделоть-то на любой полной по Тьюрингу параше можно, а вот сделать пригодным для использования в пределах крестах, не переизобретая поверх них нового языка, никак не выйдет.
>>488062
Я мудак, извини D тоже, какого хуя надо .strip()?. Починил.
http://dpaste.dzfl.pl/cea917021136
>что бы я ни вводил в инпут
Я мудак, извини D тоже, какого хуя надо .strip()?. Починил.
http://dpaste.dzfl.pl/cea917021136
>>488066
Ну да, кто спорит-то.
Алсо, я тут думал над if(n == m) и более сложными конструкциями, у вас там компилятор прошаривает все такие ограничения в процессе прохода по коду же, и зависимые типы начинают зависеть от них тоже, так? Вот такое хрен сделаешь нормально.
> не переизобретая поверх них нового языка
Ну да, кто спорит-то.
Алсо, я тут думал над if(n == m) и более сложными конструкциями, у вас там компилятор прошаривает все такие ограничения в процессе прохода по коду же, и зависимые типы начинают зависеть от них тоже, так? Вот такое хрен сделаешь нормально.
>>487997
Твоя программа забагована, лал. (a .++ b) . (b .++ a) это не то же самое, что (a .++ b) . (a .++ b), а твой идрис, похоже, считает иначе.
Введи 1 и 2. Получишь
printLn $ (a .++ b) .* (rewrite plusCommutative n m in b .++ a) ==> "1".
Но (a .++ b) = [0 0 1], (b .++ a) = [0 1 0], и их скалярное произведение равно нулю. Сдулась твоя верификация?
Твоя программа забагована, лал. (a .++ b) . (b .++ a) это не то же самое, что (a .++ b) . (a .++ b), а твой идрис, похоже, считает иначе.
Введи 1 и 2. Получишь
printLn $ (a .++ b) .* (rewrite plusCommutative n m in b .++ a) ==> "1".
Но (a .++ b) = [0 0 1], (b .++ a) = [0 1 0], и их скалярное произведение равно нулю. Сдулась твоя верификация?
30 Кб, 1100x668
Вот, наслаждайтесь: https://gist.github.com/sorrge/2d2271e57ad1e91a50ea
Чистейшие кресты, возможностей еще побольше, чем в Идрисе в некоторых местах, к тому же без багов.
Жду исправленного кода на Идрисе. Если такового не будет, то будем считать, что зависимые типы в крестах круче.
Чистейшие кресты, возможностей еще побольше, чем в Идрисе в некоторых местах, к тому же без багов.
Жду исправленного кода на Идрисе. Если такового не будет, то будем считать, что зависимые типы в крестах круче.
>>488167
ну ок))
ну ок))
>>488143
Но там никто и не утверждает, что (a .++ b) .∗ (b .++ a) = (a .++ b) .∗ (a .++ b). Единственное требование, которое есть у .∗ — одинаковые длины у векторов. И действительно, (a .++ b) и (b .++ a) имеют одинаковую длину (что следует из из определения .∗ и коммутативности сложения).
Но там никто и не утверждает, что (a .++ b) .∗ (b .++ a) = (a .++ b) .∗ (a .++ b). Единственное требование, которое есть у .∗ — одинаковые длины у векторов. И действительно, (a .++ b) и (b .++ a) имеют одинаковую длину (что следует из из определения .∗ и коммутативности сложения).
>>488143
Во-первых:
a == [0]
b == [1, 0]
Во-вторых, да, неправильно определена конкатенация (.++):
[0] .++ [1, 0] == [0, 1, 0]
[1, 0] .++ [0] == [0, 1, 0]
То есть вместо:
(.++) {n = S n} {m = m} (x :: xs) y = rewrite plusSuccRightSucc n m in xs .++ (x :: y)
надо просто:
(.++) (x :: xs) y = x :: (xs .++ y)
Во-первых:
a == [0]
b == [1, 0]
Во-вторых, да, неправильно определена конкатенация (.++):
[0] .++ [1, 0] == [0, 1, 0]
[1, 0] .++ [0] == [0, 1, 0]
То есть вместо:
(.++) {n = S n} {m = m} (x :: xs) y = rewrite plusSuccRightSucc n m in xs .++ (x :: y)
надо просто:
(.++) (x :: xs) y = x :: (xs .++ y)
>>488188
Ненене, погоди-погоди. Я хочу зделоть
(a .++ b) .∗ (b .++ a)
А оно мне говорит, мол, не ниче не знаю, n + m это не m + n, и точка. И тут я такой: дык коммутативно же, сложение-то!
(a .++ b) .∗ (rewrite plusCommutative n m in b .++ a)
Я это так понимаю. Не было команды заменять b .++ a на нечто совершенно другое, a .++ b.
А идрис, получается, так рассуждает: нука нука, что это тут у нас? b .++ a не выходит, а может попробовать вместо этого a .++ b? Сработало, ну вот и доказана корректность! Вот и хорошо. Так и запишем.
А в следующий раз он может просто скалярное произведение на 0 заменит? А че там, и то число, и это число. Какая разница-то, итить?
Ненене, погоди-погоди. Я хочу зделоть
(a .++ b) .∗ (b .++ a)
А оно мне говорит, мол, не ниче не знаю, n + m это не m + n, и точка. И тут я такой: дык коммутативно же, сложение-то!
(a .++ b) .∗ (rewrite plusCommutative n m in b .++ a)
Я это так понимаю. Не было команды заменять b .++ a на нечто совершенно другое, a .++ b.
А идрис, получается, так рассуждает: нука нука, что это тут у нас? b .++ a не выходит, а может попробовать вместо этого a .++ b? Сработало, ну вот и доказана корректность! Вот и хорошо. Так и запишем.
А в следующий раз он может просто скалярное произведение на 0 заменит? А че там, и то число, и это число. Какая разница-то, итить?
>>488190
Вот это уже похоже на правду. Протестирую сейчас.
Вот это уже похоже на правду. Протестирую сейчас.
>>488191
Но rewrite не заменяет b .++ a на a .++ b. Он заменяет совсем другое: `m + n` на `n + m` в типе Vec (m + n) _.
Но rewrite не заменяет b .++ a на a .++ b. Он заменяет совсем другое: `m + n` на `n + m` в типе Vec (m + n) _.
>>488193
Да, теперь понятно уже, что конкатенация была забагована. Еще один камень в огород идриса: что же там легко накосячить в элементарной операции
?
А вот такое все равно не работает:
(a .++ b .++ a .++ a .++ b) .∗ (rewrite plusCommutative n m in (b .++ a .++ a .++ a .++ b))
В крестах работает. Для доказательства этого нужна только коммутативность.
Да, теперь понятно уже, что конкатенация была забагована. Еще один камень в огород идриса: что же там легко накосячить в элементарной операции
?
А вот такое все равно не работает:
(a .++ b .++ a .++ a .++ b) .∗ (rewrite plusCommutative n m in (b .++ a .++ a .++ a .++ b))
В крестах работает. Для доказательства этого нужна только коммутативность.
>>488197
Я, вообще говоря, удивился, увидев то определение. Но подумал, что всё равно мы проверяем не это.
Здесь нужно привести `n + m + n + n + m` к `m + n + n + n + m`. Одного `rewrite plusCommutative n m` для этого недостаточно.
Небольшой такой вопрос: а как именно кресты выводят доказательство, полагаясь на одну только коммутативность? Это, конечно, можно доказать, но не за один шаг.
> что же там легко накосячить в элементарной операции
Я, вообще говоря, удивился, увидев то определение. Но подумал, что всё равно мы проверяем не это.
> (a .++ b .++ a .++ a .++ b) .∗ (rewrite plusCommutative n m in (b .++ a .++ a .++ a .++ b))
Здесь нужно привести `n + m + n + n + m` к `m + n + n + n + m`. Одного `rewrite plusCommutative n m` для этого недостаточно.
> В крестах работает. Для доказательства этого нужна только коммутативность.
Небольшой такой вопрос: а как именно кресты выводят доказательство, полагаясь на одну только коммутативность? Это, конечно, можно доказать, но не за один шаг.
>>488205
...и используя не только коммутативность. Без ассоциативности это доказать нельзя.
...и используя не только коммутативность. Без ассоциативности это доказать нельзя.
>>488205
Сопоставлением образцов во время partial template speciation. Вот код, который это делает:
// plusCommutative
template<class TV1, class TV2, class TV3, class TV4, class Context>
struct TypeExprEq<Plus<TV1, TV2>, Plus<TV3, TV4>, Context>
{
\tstatic const bool value = TypeExprEq<TV1, TV3, Context>::value && TypeExprEq<TV2, TV4, Context>::value ||
\t\tTypeExprEq<TV1, TV4, Context>::value && TypeExprEq<TV2, TV3, Context>::value;
};
В переводе на русский, тут утверждается, что для доказательства равенства типов TV1+TV2 == TV3+TV4 нужно сначала попробовать доказать, что TV1 == TV3 && TV2 == TV4, а если это не получилось, то попробовать TV1 == TV4 && TV2 == TV3.
Сопоставлением образцов во время partial template speciation. Вот код, который это делает:
// plusCommutative
template<class TV1, class TV2, class TV3, class TV4, class Context>
struct TypeExprEq<Plus<TV1, TV2>, Plus<TV3, TV4>, Context>
{
\tstatic const bool value = TypeExprEq<TV1, TV3, Context>::value && TypeExprEq<TV2, TV4, Context>::value ||
\t\tTypeExprEq<TV1, TV4, Context>::value && TypeExprEq<TV2, TV3, Context>::value;
};
В переводе на русский, тут утверждается, что для доказательства равенства типов TV1+TV2 == TV3+TV4 нужно сначала попробовать доказать, что TV1 == TV3 && TV2 == TV4, а если это не получилось, то попробовать TV1 == TV4 && TV2 == TV3.
>>488212
Лол. С левой ассоциативностью легко, а вот с правой уже не так просто.
> Ты скобки не так расставил.
Лол. С левой ассоциативностью легко, а вот с правой уже не так просто.
>>488223
В крестах можно добавить правила для проверки ассоциативности. Это будет полным перебором делаться, конечно, что может привести к долгой компиляции длинных выражений. Но сам алгоритм тривиален: пробуй и так, и сяк.
Можно сделать и ручной режим, как в идрисе. Там писанины побольше будет.
В крестах можно добавить правила для проверки ассоциативности. Это будет полным перебором делаться, конечно, что может привести к долгой компиляции длинных выражений. Но сам алгоритм тривиален: пробуй и так, и сяк.
Можно сделать и ручной режим, как в идрисе. Там писанины побольше будет.
>>488197
Idris невиноват в том, что конкатенация неверная, виноват только человек, который ее написал. Idris же не знает, какая конкатенация правильная, а какая нет, для этого нужно формулировать свойства, которые выносятся в типы (или пишутся отдельной функцией), а уже потом доказывается корректность конкатенации.
А оно и не должно. Это же не просто арифметические выражения, это термы. Поэтому уже нужна другая лемма, здесь все строго.
Idris невиноват в том, что конкатенация неверная, виноват только человек, который ее написал. Idris же не знает, какая конкатенация правильная, а какая нет, для этого нужно формулировать свойства, которые выносятся в типы (или пишутся отдельной функцией), а уже потом доказывается корректность конкатенации.
>А вот такое все равно не работает:
А оно и не должно. Это же не просто арифметические выражения, это термы. Поэтому уже нужна другая лемма, здесь все строго.
>>488236
Ясно, что не он не знает. Проблема в том, что запись определения этой функции стала настолько неудобочитаемой, что фактически непонятно (человеку), что она делает. Отсюда и ошибка.
Это плохое оправдание. На крестах вон тоже все строго. Какой это вывод типов, если ему каждое действие нужно прописать? Без автоматизации таких простых цепочек там на каждый чих придется простыни доказательств писать.
Но если там скобки по-другому расставлены, то тогда понятно - там ассоциативность нужна.
Ясно, что не он не знает. Проблема в том, что запись определения этой функции стала настолько неудобочитаемой, что фактически непонятно (человеку), что она делает. Отсюда и ошибка.
>Поэтому уже нужна другая лемма, здесь все строго.
Это плохое оправдание. На крестах вон тоже все строго. Какой это вывод типов, если ему каждое действие нужно прописать? Без автоматизации таких простых цепочек там на каждый чих придется простыни доказательств писать.
Но если там скобки по-другому расставлены, то тогда понятно - там ассоциативность нужна.
>>488241
И какое решение этой проблемы предложено в идрисе?
>Для ad-hoc вещей вроде сложения такой способ пригоден. В общем случае уже нет.
И какое решение этой проблемы предложено в идрисе?
>>488242
Эм. Я совсем не знаю как работает система шаблонов в C++, но в Idris (и в любых языках с зависимыми типами) вывод типов undecidable, не считая контекстов, когда это просто типизированная лямбда.
И да, каждое действие надо прописывать. В этом и проблема, что в данный момент доказательства писать муторно и долго и что нужно переходить к их умной генерации (ну или к тактикам вот переходят).
Эм. Я совсем не знаю как работает система шаблонов в C++, но в Idris (и в любых языках с зависимыми типами) вывод типов undecidable, не считая контекстов, когда это просто типизированная лямбда.
И да, каждое действие надо прописывать. В этом и проблема, что в данный момент доказательства писать муторно и долго и что нужно переходить к их умной генерации (ну или к тактикам вот переходят).
>>488243
Так как сколь-либо общего решения этой проблемы не существует (печально, но факт), остаётся лишь попытаться облегчить сам процесс доказательства. Для этого в Idris есть: разделение кода и доказательств (provisional definitions), тактики, довольно мощное сопоставление с образцом и немного переписывания термов. И само-собой, как всегда, помогает абстракция и готовые библиотеки.
>>488247
С тактиками у Idris пока небогато. Ехал rewrite через rewrite.
Так как сколь-либо общего решения этой проблемы не существует (печально, но факт), остаётся лишь попытаться облегчить сам процесс доказательства. Для этого в Idris есть: разделение кода и доказательств (provisional definitions), тактики, довольно мощное сопоставление с образцом и немного переписывания термов. И само-собой, как всегда, помогает абстракция и готовые библиотеки.
>>488247
> ну или к тактикам вот переходят
С тактиками у Idris пока небогато. Ехал rewrite через rewrite.
>>488251
>>488247
Ну а все-таки, автоматизировать применение правил в идрисе можно? Например, сказать, чтобы коммутативность проверялась всегда, когда в типе используется сложение, а не только по запросу?
Иначе получается, что кресты предоставляют больше возможностей, лал. А на дэ в примере выше вообще можно произвольный код для сопоставления типов писать. Там офигенно можно развернуться: сделать оптимальные процедуры для нормализации выражений, например. Тогда все эти ассоциативности-коммутативности любой сложности будут моментально вычисляться. И многое другое.
>>488247
Ну а все-таки, автоматизировать применение правил в идрисе можно? Например, сказать, чтобы коммутативность проверялась всегда, когда в типе используется сложение, а не только по запросу?
Иначе получается, что кресты предоставляют больше возможностей, лал. А на дэ в примере выше вообще можно произвольный код для сопоставления типов писать. Там офигенно можно развернуться: сделать оптимальные процедуры для нормализации выражений, например. Тогда все эти ассоциативности-коммутативности любой сложности будут моментально вычисляться. И многое другое.
>>488236
Предлагаю сделать это следующим туром нашей специальной зависимотиповой олимпиады. Для конкатенации написать три леммы: про левую и правую единицу и про ассоциативность. Короче, что вектор, пустой вектор и cat образуют моноид.
>для этого нужно формулировать свойства
Предлагаю сделать это следующим туром нашей специальной зависимотиповой олимпиады. Для конкатенации написать три леммы: про левую и правую единицу и про ассоциативность. Короче, что вектор, пустой вектор и cat образуют моноид.
>>488326
Есть неявные аргументы и неявные преобразования. Магии они не делают, впрочем.
> Ну а все-таки, автоматизировать применение правил в идрисе можно?
Есть неявные аргументы и неявные преобразования. Магии они не делают, впрочем.
http://www.linux.org.ru/forum/development/4299185 всё уже обсудили до нас
>>488158
Как это компилировать? На любые попытки выдает ошибки в шаблонах.
>>488326
Я не понимаю почему всем так хочется доказать, что в С++ или D можно сделать то, чего в Idris нельзя.
Ну так получается что вы пишите какие-то куски кода, которые по сути и есть Idris, то есть пишите сами себе прувер на шаблонах, однако важно, чтобы он был согласованным и не позволял строить фальшивые доказательства (undecidable), а бил по рукам. Шаблоны уже по умолчанию undecidable из-за полноты.
>>488330
Неплохое упражнение на самом деле.
Как это компилировать? На любые попытки выдает ошибки в шаблонах.
>>488326
Я не понимаю почему всем так хочется доказать, что в С++ или D можно сделать то, чего в Idris нельзя.
>Кресты предоставляют больше возможностей
Ну так получается что вы пишите какие-то куски кода, которые по сути и есть Idris, то есть пишите сами себе прувер на шаблонах, однако важно, чтобы он был согласованным и не позволял строить фальшивые доказательства (undecidable), а бил по рукам. Шаблоны уже по умолчанию undecidable из-за полноты.
>>488330
Неплохое упражнение на самом деле.
>>488725
Да, только чёт у меня Idris спотыкается на ровном месте.
> Неплохое упражнение на самом деле.
Да, только чёт у меня Idris спотыкается на ровном месте.
>>488740
А вот, собственно, где он спотыкается: http://lpaste.net/1334041297681383424
Причина проста: тупой `rewrite` туп. В мейллисте есть тред https://groups.google.com/forum/#!msg/idris-lang/iNNYoE0k27A/AhiVU_LBFBcJ, где предлагаются костыли-костылики для решения этой проблемы. И ьне как-то лень возиться с этими костылями.
Плохо зделали, тупо, короч.
А вот, собственно, где он спотыкается: http://lpaste.net/1334041297681383424
Причина проста: тупой `rewrite` туп. В мейллисте есть тред https://groups.google.com/forum/#!msg/idris-lang/iNNYoE0k27A/AhiVU_LBFBcJ, где предлагаются костыли-костылики для решения этой проблемы. И ьне как-то лень возиться с этими костылями.
Плохо зделали, тупо, короч.
>>488778
Ну можно и без rewrite (Equational Reasoning), как сделано в стандартной библиотеке: https://github.com/idris-lang/Idris-dev/blob/master/libs/base/Data/VectType.idr#L554
А то что некоторые вещи сделаны плохо или их совсем нет, то это вполне понятно почему.
Ну можно и без rewrite (Equational Reasoning), как сделано в стандартной библиотеке: https://github.com/idris-lang/Idris-dev/blob/master/libs/base/Data/VectType.idr#L554
А то что некоторые вещи сделаны плохо или их совсем нет, то это вполне понятно почему.
>>488718
Это ерунда без выражений и операций.
>>488725
Я только в студии компилировал, под другие надо править ошибки.
Вопрос был в том, изобрели ли зависимые типы в этих языках, или они есть и в крестах. Ответ: нет, не изобрели, на крестах можно делать то же самое. Для сравнения попробуй на С99 сделать ту задачу с вектором. Вот этот язык не поддерживает зависимые типы.
Это ерунда без выражений и операций.
>>488725
>На любые попытки выдает ошибки в шаблонах.
Я только в студии компилировал, под другие надо править ошибки.
>что вы пишите какие-то куски кода, которые по сути и есть Idris
Вопрос был в том, изобрели ли зависимые типы в этих языках, или они есть и в крестах. Ответ: нет, не изобрели, на крестах можно делать то же самое. Для сравнения попробуй на С99 сделать ту задачу с вектором. Вот этот язык не поддерживает зависимые типы.
>>488794
Можно. Просто весьма сбивает с толку, когда то, что должно работать, не работает.
Можно. Просто весьма сбивает с толку, когда то, что должно работать, не работает.
Вопрос к языковедам. Есть ли такой язык, который был бы во всем, как обычный С, со всеми его маллоками, указателями и т.д., но с современной системой типов, с автоматическим выводом типов и тому подобным?
Можно же такое зделоть. Компилировать в тот же С, но после всех проверок, с генерацией кода для разных случаев. Есть же до сих пор любители писать на С, по разным причинам. Из-за скорости, простоты, совместимости с другим кодом. Может быть, им такое понравилось бы.
Можно же такое зделоть. Компилировать в тот же С, но после всех проверок, с генерацией кода для разных случаев. Есть же до сих пор любители писать на С, по разным причинам. Из-за скорости, простоты, совместимости с другим кодом. Может быть, им такое понравилось бы.
>>488801
Да, не изобрели, потому что эти языки опираются на теорию типов 80х, которая была построена на идеях 40-50х годов.
То что в C++ можно делать какие-то вещи как в Idris или Agda, не говорит, что там зависимые типы (в рамках этой простой задачи возможно да, я не читал код на шаблонах). Например в C++ нет супертипа, а это значит, что вот такое написать нельзя:
hey : Int -> Type
hey 5 = Int
hey _ = Float
В обычных языках термы и типы живут в разных мирах, в языках же с зависимыми типами мир термов и типов - один.
>>488832
Если не нужны зависимые типы, то наверное Rust, а если нужны, то http://www.ats-lang.org/
Про генерацию кода для разных случаев - это уже суперкомпиляция какая-то.
Да, не изобрели, потому что эти языки опираются на теорию типов 80х, которая была построена на идеях 40-50х годов.
То что в C++ можно делать какие-то вещи как в Idris или Agda, не говорит, что там зависимые типы (в рамках этой простой задачи возможно да, я не читал код на шаблонах). Например в C++ нет супертипа, а это значит, что вот такое написать нельзя:
hey : Int -> Type
hey 5 = Int
hey _ = Float
В обычных языках термы и типы живут в разных мирах, в языках же с зависимыми типами мир термов и типов - один.
>>488832
Если не нужны зависимые типы, то наверное Rust, а если нужны, то http://www.ats-lang.org/
Про генерацию кода для разных случаев - это уже суперкомпиляция какая-то.
>>488832
О чем ты вообще? Цпп и д компилируются в такой же байткод как и ц, с такой же скоростью и совместимостью. Пиши на цпп в стиле ц и добавь кодогенерации шаблонами - ничто не пострадает. Ним так вообще в исходник на ц компилится.
> Компилировать в тот же С, но после всех проверок, с генерацией кода для разных случаев.
О чем ты вообще? Цпп и д компилируются в такой же байткод как и ц, с такой же скоростью и совместимостью. Пиши на цпп в стиле ц и добавь кодогенерации шаблонами - ничто не пострадает. Ним так вообще в исходник на ц компилится.
>>488837
Это обычное метапрограммирование, которое есть во всех нормальных языках.
>Про генерацию кода для разных случаев - это уже суперкомпиляция какая-то.
Это обычное метапрограммирование, которое есть во всех нормальных языках.
>>488832
Зачем писать как на С, если есть полноценная система типов? А так-то был Cyclone, есть Rust, а если хочется зависимых типов — ATS.
Зачем писать как на С, если есть полноценная система типов? А так-то был Cyclone, есть Rust, а если хочется зависимых типов — ATS.
>>488840
Ну так он спрашивает про то, чтобы компилятор сам генерировал разный код для разных случаев, а не чтобы самому описывать эти самые случаи.
Ну так он спрашивает про то, чтобы компилятор сам генерировал разный код для разных случаев, а не чтобы самому описывать эти самые случаи.
>>488843
Комплюктер САМ ничего не делает, на дворе всё-таки 2015 год.
> компилятор сам генерировал разный код для разных случаев
Комплюктер САМ ничего не делает, на дворе всё-таки 2015 год.
>>488837
Можно, частичной специализацией шаблонов. Но параметер функции должен быть константой времени компиляции.
Тот мой код на крестах выше как раз объединяет термы и типы. Вообще говоря ты прав, но возможности языка огромны, и если сильно надо, можно зделоть все. Особенно в дэ.
http://en.wikipedia.org/wiki/No_true_Scotsman
Мне непонятно, какие принципиально новые возможности открывает идрис? Доказательством теорем меня не удивишь: эта тема древняя, как компьютер сайнс, и тут они ничего нового привнести не могли. Срастили типы и термы? Как именно это помогает при верификации свойств? То, что у а+б длина м+н, можно доказать и без зависимых типов. Они там не нужны. А сколько-нибудь нетривиальная операция точно так же ничего полезного в типах не отразит.
Например, я сначала уберу нули из списка функцией remove_zeros, а потом поделю 5 на первый его элемент. Как доказать, что не будет деления на ноль? Сварганишь специальный тип вектора Vector(length:Nat, elem:Type, contains_0:Boolean), и будешь по всем функциям доказывать, как они влияют на изменения contains_0?
>Например в C++ нет супертипа, а это значит, что вот такое написать нельзя:
Можно, частичной специализацией шаблонов. Но параметер функции должен быть константой времени компиляции.
>термы и типы живут в разных мирах
Тот мой код на крестах выше как раз объединяет термы и типы. Вообще говоря ты прав, но возможности языка огромны, и если сильно надо, можно зделоть все. Особенно в дэ.
>То что в C++ можно делать какие-то вещи как в Idris или Agda, не говорит, что там зависимые типы (в рамках этой простой задачи возможно да, я не читал код на шаблонах).
http://en.wikipedia.org/wiki/No_true_Scotsman
Мне непонятно, какие принципиально новые возможности открывает идрис? Доказательством теорем меня не удивишь: эта тема древняя, как компьютер сайнс, и тут они ничего нового привнести не могли. Срастили типы и термы? Как именно это помогает при верификации свойств? То, что у а+б длина м+н, можно доказать и без зависимых типов. Они там не нужны. А сколько-нибудь нетривиальная операция точно так же ничего полезного в типах не отразит.
Например, я сначала уберу нули из списка функцией remove_zeros, а потом поделю 5 на первый его элемент. Как доказать, что не будет деления на ноль? Сварганишь специальный тип вектора Vector(length:Nat, elem:Type, contains_0:Boolean), и будешь по всем функциям доказывать, как они влияют на изменения contains_0?
Вот вам пример реального использования типов-выражений в крестах: http://eigen.tuxfamily.org/dox/classEigen_1_1GeneralProduct.html
Там это используется для оптимизации действий с матрицами, исключения ненужного копирования промежуточных результатов вычислений в длинных выражениях.
Там это используется для оптимизации действий с матрицами, исключения ненужного копирования промежуточных результатов вычислений в длинных выражениях.
>>488891
Вот, ты сам всё сказал.
То есть, никто не спорит, в C++ можно сварганить подмножество зависимых типов. Как и на скалке, и на хачкеле. Но не всё.
См. изоморфизм Карри-Говарда.
Сделать, чтобы remove_zeros возвращала зависимую пару из вектора и доказательства, что все элементы не нули.
> Но параметер функции должен быть константой времени компиляции.
Вот, ты сам всё сказал.
То есть, никто не спорит, в C++ можно сварганить подмножество зависимых типов. Как и на скалке, и на хачкеле. Но не всё.
> Срастили типы и термы? Как именно это помогает при верификации свойств?
См. изоморфизм Карри-Говарда.
> Как доказать, что не будет деления на ноль?
Сделать, чтобы remove_zeros возвращала зависимую пару из вектора и доказательства, что все элементы не нули.
>>488931
Ну и что, что изоморфизм? Можно доказательства на типах делать? А зачем? Их прекрасно можно делать и без типов. Как это помогает в чем-либо?
Мне это напоминает риторику лиспоидов: смотрите, программа и данные это одно и то же. Ясно.
remove_zeros, допустим, вернет такую пару, хотя это уже притянуто за уши - с чего бы ей морочиться таким частным свойством. Ну допустим. А потом я прицеплю 5 к этому списку, и доказательство протухнет. У тебя весь код должен это доказательство возвращать? А если мне не нули интересны, а простые числа? Строки из трех букв? Может, мне важно, является ли список палиндромом?
Очевидно, что ты не сможешь все доказательства записать в код заранее. Всё равно придется все верифицировать вручную для каждого случая. Какой тогда смысл замусоривать код до нечитаемости?
Ну и что, что изоморфизм? Можно доказательства на типах делать? А зачем? Их прекрасно можно делать и без типов. Как это помогает в чем-либо?
Мне это напоминает риторику лиспоидов: смотрите, программа и данные это одно и то же. Ясно.
remove_zeros, допустим, вернет такую пару, хотя это уже притянуто за уши - с чего бы ей морочиться таким частным свойством. Ну допустим. А потом я прицеплю 5 к этому списку, и доказательство протухнет. У тебя весь код должен это доказательство возвращать? А если мне не нули интересны, а простые числа? Строки из трех букв? Может, мне важно, является ли список палиндромом?
Очевидно, что ты не сможешь все доказательства записать в код заранее. Всё равно придется все верифицировать вручную для каждого случая. Какой тогда смысл замусоривать код до нечитаемости?
>>488941
Делать-то, конечно, можно, а вот с проверкой — беда. Вот, возьми это: http://research.microsoft.com/en-us/um/people/gonthier/4colproof.pdf
> Можно доказательства на типах делать? А зачем? Их прекрасно можно делать и без типов.
Делать-то, конечно, можно, а вот с проверкой — беда. Вот, возьми это: http://research.microsoft.com/en-us/um/people/gonthier/4colproof.pdf
>>488949
По-моему ты совершенно не понимаешь, о чем я говорю. К чему ты это привел?
По-моему ты совершенно не понимаешь, о чем я говорю. К чему ты это привел?
>>488891
Мне кажется ты как-то сильно привязался к Idris и хочешь для себя решить, что он на самом деле и не нужен совсем.
Еще раз: Idris - просто очередная реализация языка с зависимыми типами (немного отличаается от Agda), ну просто решили они попробовать сделать язык с практическим уклоном (на самом деле нового там - другой подход к работе с грязными функциями: библиотека Effects).
Только это и позволяет выражать и доказывать эти самые свойста. Это не просто какой-то язык как C++ или Python. Это язык - типизированная лямбда исчисление (посложнее), в котором некоторые вещи оказались похожи на логику предикатов (Карри-Говард).
Эм, чтобы проверять доказательства на компьютере.
Здесь все конечно смотрят со стороны индустрии и кодеров, однако забыли математиков, которым вообще говоря возможность выражать теоремы конструктивной математики и проверять на компьютере их не помешает.
Есть мнение, что лет через 20 или 50 вся математика и будет проверяться в разных пруверах.
>>488941
Для обычных программистов сейчас это оверхеад и вообще много возни. Но это сейчас, Idris - первый язык с практическим уклоном. Нужно время, чтобы оно доросло до реальных задач. В целом, если спрашивать зачем оно нужно, то такие доказательства дополняют тесты, потому что тесты не могут покрыть все случаи, а док-во может.
Мне кажется ты как-то сильно привязался к Idris и хочешь для себя решить, что он на самом деле и не нужен совсем.
Еще раз: Idris - просто очередная реализация языка с зависимыми типами (немного отличаается от Agda), ну просто решили они попробовать сделать язык с практическим уклоном (на самом деле нового там - другой подход к работе с грязными функциями: библиотека Effects).
>Как именно это помогает при верификации свойств?
Только это и позволяет выражать и доказывать эти самые свойста. Это не просто какой-то язык как C++ или Python. Это язык - типизированная лямбда исчисление (посложнее), в котором некоторые вещи оказались похожи на логику предикатов (Карри-Говард).
>Можно доказательства на типах делать? А зачем?
Эм, чтобы проверять доказательства на компьютере.
>Как это помогает в чем-либо?
Здесь все конечно смотрят со стороны индустрии и кодеров, однако забыли математиков, которым вообще говоря возможность выражать теоремы конструктивной математики и проверять на компьютере их не помешает.
Есть мнение, что лет через 20 или 50 вся математика и будет проверяться в разных пруверах.
>>488941
>Всё равно придется все верифицировать вручную для каждого случая. Какой тогда смысл замусоривать код до нечитаемости?
Для обычных программистов сейчас это оверхеад и вообще много возни. Но это сейчас, Idris - первый язык с практическим уклоном. Нужно время, чтобы оно доросло до реальных задач. В целом, если спрашивать зачем оно нужно, то такие доказательства дополняют тесты, потому что тесты не могут покрыть все случаи, а док-во может.
>>488978
Я хочу понять, нужен он или нет, и если да, то для чего именно.
Да нет, не только это. Программы верифицировали задолго до появления языков с зависимыми типами.
Доказательства можно проверять на компьютере и без всего этого. Совершенно необязательно записывать их как часть самой программы.
Ты что, пытаешься обосновать, что этот механизм записи доказательств внутри самой программы - единственный способ верификации? Это, очевидно, не так. С помощью Coq, например, можно верифицировать программы на С, хаскеле, других языках. Посмотри также Why3. Это state of the art в верификации.
Единственная возможная полезность от возможности представления доказательств в коде программы, это какое-то облегчение процесса верификации. Тут мы и возвращаемся к изначальному вопросу:
Как это помогает в чем-либо?
Пример с вектором не надо приводить. Мы его исследовали и пришли к выводу, что в этом случае идрис не предоставляет значительно более мощные механизмы, чем другие языки с зависимыми типами. Но где тогда потенциал раскрывается? Хоть один пример есть? Чтобы можно было сказать, что не будь тут зависимых типов, это было бы гораздо труднее?
У современных математиков другие заботы. Мало кто из них использует подобные инструменты. Компьютер для них это печатная машинка.
>Мне кажется ты как-то сильно привязался к Idris и хочешь для себя решить, что он на самом деле и не нужен совсем.
Я хочу понять, нужен он или нет, и если да, то для чего именно.
>Только это и позволяет выражать и доказывать эти самые свойста.
Да нет, не только это. Программы верифицировали задолго до появления языков с зависимыми типами.
>Эм, чтобы проверять доказательства на компьютере.
Доказательства можно проверять на компьютере и без всего этого. Совершенно необязательно записывать их как часть самой программы.
Ты что, пытаешься обосновать, что этот механизм записи доказательств внутри самой программы - единственный способ верификации? Это, очевидно, не так. С помощью Coq, например, можно верифицировать программы на С, хаскеле, других языках. Посмотри также Why3. Это state of the art в верификации.
Единственная возможная полезность от возможности представления доказательств в коде программы, это какое-то облегчение процесса верификации. Тут мы и возвращаемся к изначальному вопросу:
Как это помогает в чем-либо?
Пример с вектором не надо приводить. Мы его исследовали и пришли к выводу, что в этом случае идрис не предоставляет значительно более мощные механизмы, чем другие языки с зависимыми типами. Но где тогда потенциал раскрывается? Хоть один пример есть? Чтобы можно было сказать, что не будь тут зависимых типов, это было бы гораздо труднее?
>забыли математиков
У современных математиков другие заботы. Мало кто из них использует подобные инструменты. Компьютер для них это печатная машинка.
>>489014
Например тем, что можно использовать определения и функции, которые уже есть в рабочем коде?
> Как это помогает в чем-либо?
Например тем, что можно использовать определения и функции, которые уже есть в рабочем коде?
>>489035
Кроме того, возможен случай, когда мы не хотим доказывать всю программу (так как это непростая задача), но хотим, чтобы аргументы функции и/или возвращаемое значение подчинились каком-то условию, причём чтобы это проверялось на этапе компиляции.
Кроме того, возможен случай, когда мы не хотим доказывать всю программу (так как это непростая задача), но хотим, чтобы аргументы функции и/или возвращаемое значение подчинились каком-то условию, причём чтобы это проверялось на этапе компиляции.
>>489044
Можно и так. Только зависимые типы позволяют формулировать практически любые утверждения и проверять их во время компиляции. Например, если ты предполагаешь, например, что где-то в коде список не может быть пуст или число не может равняться нулю или что-то ещё, ты можешь это сформулировать и попробовать доказать.
Можно и так. Только зависимые типы позволяют формулировать практически любые утверждения и проверять их во время компиляции. Например, если ты предполагаешь, например, что где-то в коде список не может быть пуст или число не может равняться нулю или что-то ещё, ты можешь это сформулировать и попробовать доказать.
>>489047
Но для этого не нужны зависимые типы. Вот статья про статическую проверку контрактов в дотнете: https://msdn.microsoft.com/en-us/magazine/hh335064.aspx
Суть: пишешь контракт в виде произвольного выражения на шарпе (тоже можешь использовать свой код там, все что хочешь):
public void ProcessOrder(int orderId)
{
Contract.Requires<ArgumentException>(orderId >0);
...
}
И все это проверяется статически, получаешь предупреждение, если контракт не доказан. Зависимых типов в шарпе нет.
Но для этого не нужны зависимые типы. Вот статья про статическую проверку контрактов в дотнете: https://msdn.microsoft.com/en-us/magazine/hh335064.aspx
Суть: пишешь контракт в виде произвольного выражения на шарпе (тоже можешь использовать свой код там, все что хочешь):
public void ProcessOrder(int orderId)
{
Contract.Requires<ArgumentException>(orderId >0);
...
}
И все это проверяется статически, получаешь предупреждение, если контракт не доказан. Зависимых типов в шарпе нет.
>>489053
Очень хуево там проверяется, я пробовал. В основном контракты используют в рантайме как сорт оф обычные ассерты.
> И все это проверяется статически
Очень хуево там проверяется, я пробовал. В основном контракты используют в рантайме как сорт оф обычные ассерты.
>>489058
Это всего лишь слабость прувера. Мы же не пруверы тут сравниваем. Да и можно подумать, в идрисе мегакрутой прувер какой-то.
Попробую потом пример с вектором на контрактах сделать. Посмотрим, осилит ли это верификатор.
Это всего лишь слабость прувера. Мы же не пруверы тут сравниваем. Да и можно подумать, в идрисе мегакрутой прувер какой-то.
Попробую потом пример с вектором на контрактах сделать. Посмотрим, осилит ли это верификатор.
>>489062
Заодно попробуй ту задачу с моноидом.
Заодно попробуй ту задачу с моноидом.
>>489014
Фича идриса в том, что он, в отличие от Coq и агды, стремится стать языком для _разработки_, а не доказательств (но и не байтоёбли, как у ATS). Поэтому он обвешан синтаксическими плюшками и сильно заморачивается на тему компиляции.
> в этом случае идрис не предоставляет значительно более мощные механизмы, чем другие языки с зависимыми типами
Фича идриса в том, что он, в отличие от Coq и агды, стремится стать языком для _разработки_, а не доказательств (но и не байтоёбли, как у ATS). Поэтому он обвешан синтаксическими плюшками и сильно заморачивается на тему компиляции.
>>489062
Прям тут попробуй что-нибудь
http://www.pexforfun.com/default.aspx?language=CSharp&sample=MethodCalls
Прям тут попробуй что-нибудь
http://www.pexforfun.com/default.aspx?language=CSharp&sample=MethodCalls
>>489014
Лол. Похоже ты просто игноришь, что я пишу.
Coq и есть язык с зависимыми типами, он на одном уровне с Agda и Idris (с некоторыми различиями). Просто как написал >>489121 он ориентирован на практику. Ты можешь все тоже самое делать и в Coq (компилировать в ocaml) или в Agda (в Haskell). Просто Idris пытается собрать вместе удобство написания практических программ (как в Haskell) и возможность иметь сложную систему типов. Нет ничего тут особенного.
Why3 имеет внутри rank-1 polymorphism (https://hal.inria.fr/hal-00809651/document), когда Haskell (rank-n) или Scala (rank-2). А это все на уровне System F, а Agda, Coq или Idris далеко дальше (http://en.wikipedia.org/wiki/Lambda_cube)
Лол, да, мало, но использовать то уже можно (что я и пытаюсь делать, да из этого небольшого числа).
Контракты, это вообще совершенно другой подход.
Добавлю, что половины этого треда не было бы, если бы люди просто изучали логику и логические системы, а потом бы просто смотрели на каких логических системах построены пруверы. Если я где-то не прав, то буду рад корректировкам.
Лол. Похоже ты просто игноришь, что я пишу.
Coq и есть язык с зависимыми типами, он на одном уровне с Agda и Idris (с некоторыми различиями). Просто как написал >>489121 он ориентирован на практику. Ты можешь все тоже самое делать и в Coq (компилировать в ocaml) или в Agda (в Haskell). Просто Idris пытается собрать вместе удобство написания практических программ (как в Haskell) и возможность иметь сложную систему типов. Нет ничего тут особенного.
Why3 имеет внутри rank-1 polymorphism (https://hal.inria.fr/hal-00809651/document), когда Haskell (rank-n) или Scala (rank-2). А это все на уровне System F, а Agda, Coq или Idris далеко дальше (http://en.wikipedia.org/wiki/Lambda_cube)
>идрис не предоставляет значительно более мощные механизмы, чем другие языки с зависимыми типами
>(на самом деле нового там - другой подход к работе с грязными функциями: библиотека Effects).
>У современных математиков другие заботы. Мало кто из них использует подобные инструменты. Компьютер для них это печатная машинка.
Лол, да, мало, но использовать то уже можно (что я и пытаюсь делать, да из этого небольшого числа).
Контракты, это вообще совершенно другой подход.
Добавлю, что половины этого треда не было бы, если бы люди просто изучали логику и логические системы, а потом бы просто смотрели на каких логических системах построены пруверы. Если я где-то не прав, то буду рад корректировкам.
>>489189
Ничего я не игнорю. Я пытаюсь добиться какого-то конкретного примера, который бы явно показывал преимущества подхода идриса. Вот ты говоришь, мол, контракты это другой подход. Ок. Чем он хуже?
Я сам всеми руками за формализацию матеметики. Но факт налицо: математики сами в этом не заинтересованы. Занимается этим полтора программиста, а работы там невпроворот.
Нет никакой мотивации это делать у сообщества. Ну формализовал ты доказательство какой-нибудь стопервой теоремы Коши. Кому это надо? Только, возможно, тебе самому при формализации стовторой. А больше никто даже не посмотрит на твою работу, и тем более не оценит. Теорема старая, в ее верности никто и не сомневался.
Про Why3 не понял мысли. Это значит, что на нем нельзя доказывать свойства всех программ на хаскеле и скале? Мне это ок. Если он позволяет нормально рассуждать о программах на С или джаве, например, этого вполне достаточно.
Ничего я не игнорю. Я пытаюсь добиться какого-то конкретного примера, который бы явно показывал преимущества подхода идриса. Вот ты говоришь, мол, контракты это другой подход. Ок. Чем он хуже?
>Лол, да, мало, но использовать то уже можно
Я сам всеми руками за формализацию матеметики. Но факт налицо: математики сами в этом не заинтересованы. Занимается этим полтора программиста, а работы там невпроворот.
Нет никакой мотивации это делать у сообщества. Ну формализовал ты доказательство какой-нибудь стопервой теоремы Коши. Кому это надо? Только, возможно, тебе самому при формализации стовторой. А больше никто даже не посмотрит на твою работу, и тем более не оценит. Теорема старая, в ее верности никто и не сомневался.
Про Why3 не понял мысли. Это значит, что на нем нельзя доказывать свойства всех программ на хаскеле и скале? Мне это ок. Если он позволяет нормально рассуждать о программах на С или джаве, например, этого вполне достаточно.
>>489140
Интересно, спасибо. Но я не знаю, как там ввод-вывод делать. Он, похоже, только функцию Puzzle принимает.
Интересно, спасибо. Но я не знаю, как там ввод-вывод делать. Он, похоже, только функцию Puzzle принимает.
>>489245
Чтобы был конкретный пример преимущества подхода Idris/Agda, нужно как минимум иметь опыт работы с Coq. У меня его нет, слишком мало я пока этим всем занимаюсь. Но скажем так, Coq - это система, которая на вход принимает понятное математикам, а внутри компилируется в что-то похожее на Idris/Agda, то есть в язык программирования. Idris/Agda же сразу предлагают писать на этом языке программирования. Преимущества такого подхода наверное в очевидности происходящего. То есть сразу видно явно и понятно что происходит, потому что приходится руками делать все, что делает Coq.
Возможно я ошибаюсь, но пока пришел к такому пониманию.
Ну блин, Homotopy Type Theory уже на Wired: http://www.wired.com/2015/05/will-computers-redefine-roots-math/
На западных конференциях об этом говорят, да даже в российских вузах. Зачем ты утверждаешь, если знаком только понаслышке?
Никто и не говорит о формализации теорем из матана (хотя на самом деле хорошее занятие и упражнения). Но в данный момент уже возможно и нужно писать доказательства теорем алгебры в подобных система и это уже вполне удобно.
Ну так вот, инструменты разные под разные задачи. Idris еще один инструмент, если тебе например не будет хватать Why3, нужно будет тебе доказать одно свойство, а Why3 не может его выразить, то ты можешь взять Idris (Coq, Agda).
Контракты не позволяют добиться абсолютной истинны так сказать. То есть контракты, это когда мы берем язык и начинаем его ограничивать и вырезать разные плохие случаи. Зависимые же типы - это когда мы строим чистую систему, в которой все корректно изначально. Когда применять одну, а когда другую зависит очевидно от задачи. Но для математики, понятно, нужно использовать формальную систему типов.
Чтобы был конкретный пример преимущества подхода Idris/Agda, нужно как минимум иметь опыт работы с Coq. У меня его нет, слишком мало я пока этим всем занимаюсь. Но скажем так, Coq - это система, которая на вход принимает понятное математикам, а внутри компилируется в что-то похожее на Idris/Agda, то есть в язык программирования. Idris/Agda же сразу предлагают писать на этом языке программирования. Преимущества такого подхода наверное в очевидности происходящего. То есть сразу видно явно и понятно что происходит, потому что приходится руками делать все, что делает Coq.
Возможно я ошибаюсь, но пока пришел к такому пониманию.
> Но факт налицо: математики сами в этом не заинтересованы.
Ну блин, Homotopy Type Theory уже на Wired: http://www.wired.com/2015/05/will-computers-redefine-roots-math/
На западных конференциях об этом говорят, да даже в российских вузах. Зачем ты утверждаешь, если знаком только понаслышке?
Никто и не говорит о формализации теорем из матана (хотя на самом деле хорошее занятие и упражнения). Но в данный момент уже возможно и нужно писать доказательства теорем алгебры в подобных система и это уже вполне удобно.
>Мне это ок.
Ну так вот, инструменты разные под разные задачи. Idris еще один инструмент, если тебе например не будет хватать Why3, нужно будет тебе доказать одно свойство, а Why3 не может его выразить, то ты можешь взять Idris (Coq, Agda).
Контракты не позволяют добиться абсолютной истинны так сказать. То есть контракты, это когда мы берем язык и начинаем его ограничивать и вырезать разные плохие случаи. Зависимые же типы - это когда мы строим чистую систему, в которой все корректно изначально. Когда применять одну, а когда другую зависит очевидно от задачи. Но для математики, понятно, нужно использовать формальную систему типов.
>>489270
Лал, об этом "говорят" как минимум лет 15, а скорее всего и гораздо дольше. Вот про такое ты хоть слышал: http://mizar.uwb.edu.pl/ ? Вон у них целый журнал нечитаемых статей есть: http://mizar.uwb.edu.pl/fm/ . С 1976 года это продолжается. А воз и ныне там.
Не думаю, что НоТТ в корне поменяет ситуацию и все прям кинутся писать доказательства в coq.
>На западных конференциях об этом говорят
Лал, об этом "говорят" как минимум лет 15, а скорее всего и гораздо дольше. Вот про такое ты хоть слышал: http://mizar.uwb.edu.pl/ ? Вон у них целый журнал нечитаемых статей есть: http://mizar.uwb.edu.pl/fm/ . С 1976 года это продолжается. А воз и ныне там.
Не думаю, что НоТТ в корне поменяет ситуацию и все прям кинутся писать доказательства в coq.
>>489293
Да, но только лишь слышал.
Я не знаю причин, может не было движухи и интернета, чтобы ее распространить. Может потому что в основе лежит теория множеств, парадоксы которой ТТ и пытается устранить.
Вроде бы Mizar берут (брали) только когда нужно было формализовать что-то в рамках ZF, а сейчас не берут потому что банально устарело, это же все таки ПО и требования к интерфейсу у пользователей растут.
Да, но только лишь слышал.
Я не знаю причин, может не было движухи и интернета, чтобы ее распространить. Может потому что в основе лежит теория множеств, парадоксы которой ТТ и пытается устранить.
Вроде бы Mizar берут (брали) только когда нужно было формализовать что-то в рамках ZF, а сейчас не берут потому что банально устарело, это же все таки ПО и требования к интерфейсу у пользователей растут.
>>489315
Почему на помойку? Есть база, есть софт в котором эта база работает. Если кому-то нужны эти теоремы, определения и т.д., то он конечно будет писать доказательства на Mizar. Я думаю понятно, почему вопроса о переносе всего этого дела под другую формальную систему не стоит.
Тут уже получается столкновения как раз двух миров: математики и программирования. В одной все фундаментально и имеет значение всегда, когда в другой все быстро устаревает. Ну и я так понимаю Mizar мало используют именно потому что эту базу очень трудно использовать.
Эта проблема на самом деле уже есть у тех же Agda или Idris. Оба языка развиваются и код написанный год или два назад уже не тайпчекается. И здесь придется людям как-то выкручиваться: математикам учиться нормально программировать, а программистам нормально учить математику. Но это если мы говорим о создании какой-то библиотеки, которая будет потом кем-то использоваться, а не только для себя. Просто почти весь код на таких языках пока исследовательский и ни у кого в голове мыслей нет, что кто-то захочет это потом использовать напрямую, а не просто изучить.
Почему на помойку? Есть база, есть софт в котором эта база работает. Если кому-то нужны эти теоремы, определения и т.д., то он конечно будет писать доказательства на Mizar. Я думаю понятно, почему вопроса о переносе всего этого дела под другую формальную систему не стоит.
Тут уже получается столкновения как раз двух миров: математики и программирования. В одной все фундаментально и имеет значение всегда, когда в другой все быстро устаревает. Ну и я так понимаю Mizar мало используют именно потому что эту базу очень трудно использовать.
Эта проблема на самом деле уже есть у тех же Agda или Idris. Оба языка развиваются и код написанный год или два назад уже не тайпчекается. И здесь придется людям как-то выкручиваться: математикам учиться нормально программировать, а программистам нормально учить математику. Но это если мы говорим о создании какой-то библиотеки, которая будет потом кем-то использоваться, а не только для себя. Просто почти весь код на таких языках пока исследовательский и ни у кого в голове мыслей нет, что кто-то захочет это потом использовать напрямую, а не просто изучить.
Протестил это >>487901 с контрактами в шарпе.
Единственный контракт: в скалярном произведении длины должны быть равны. 3е ему слабо сделать, никак не доходит. Все остальное работает, в т.ч. нагромождения конкатенаций, где нужна ассоциативность и коммутативность сложения.
Единственный контракт: в скалярном произведении длины должны быть равны. 3е ему слабо сделать, никак не доходит. Все остальное работает, в т.ч. нагромождения конкатенаций, где нужна ассоциативность и коммутативность сложения.
Бамп.
> зависимые типы на крестах
-> /guro/
>>489503
Та еще задачка.
Та еще задачка.
>>492558
>>492554
Однако. Держите тогда и ATS до кучи: http://www.illtyped.com/projects/patsolve/qsort.html
>>492554
Однако. Держите тогда и ATS до кучи: http://www.illtyped.com/projects/patsolve/qsort.html
>>492589
Вот поэтому в ОП-посте и предлагается доказывать сортировку слиянием, ибо она куда ближе к ФП.
> Квиксорт на списках это просто пушка.
Вот поэтому в ОП-посте и предлагается доказывать сортировку слиянием, ибо она куда ближе к ФП.
>>492589
Там тоже нет анализа сложности, про эффективность это просто вскукарек.
Там тоже нет анализа сложности, про эффективность это просто вскукарек.
>>492589
Анализ сложности проводят при создании алгоритма, а не при его реализации. Впрочем, на зависимых типах и это можно сделать:
http://www.cse.chalmers.se/~nad/publications/danielsson-popl2008.pdf
https://github.com/lives-group/time-complexity-verification
> Алсо, алгоритм без анализа сложности - кусок дрисни
Анализ сложности проводят при создании алгоритма, а не при его реализации. Впрочем, на зависимых типах и это можно сделать:
http://www.cse.chalmers.se/~nad/publications/danielsson-popl2008.pdf
https://github.com/lives-group/time-complexity-verification
Бамп.
Может лучше этот тред сделать в /cs/ или /sci/? Или если доска закрыта, то уже все?
А то видно же, что тут смывает. А много активности здесь не будет из-за сильной специфики, но что-то интересное найти можно.
А то видно же, что тут смывает. А много активности здесь не будет из-за сильной специфики, но что-то интересное найти можно.
>>503910
/cs/ закрыта, а /sci/ немного мимо.
/cs/ закрыта, а /sci/ немного мимо.
Всё это хорошо, но где бы ознакомиться с этим, так, что б было понятно пхп-господину? Совершенно же мистическая штука, не?
Раз уж тред один черт тонет, поясните, что вообще делает тип зависимым и для чего он нужен. Изучав паскаль в школе, предположу, что заголовок функции: function dup(data array len of Integer): array len*2 of Integer; или, например record T: Type;y :T end; могут быть как-то связаны, однако, хотелось бы знать наверняка. Надеюсь на вашу снисходительность.
Раз уж тред один черт тонет, поясните, что вообще делает тип зависимым и для чего он нужен. Изучав паскаль в школе, предположу, что заголовок функции: function dup(data array len of Integer): array len*2 of Integer; или, например record T: Type;y :T end; могут быть как-то связаны, однако, хотелось бы знать наверняка. Надеюсь на вашу снисходительность.
>>516958
Просто в треде на твой вопрос уже ответили и примеры привели.
Просто в треде на твой вопрос уже ответили и примеры привели.
Я как-то тут создавал тред про верификацию своего простого комбинаторного алгоритма с конечным множеством входных вариантов. В итоге выяснилось, что проще ручками доказать. Типа формальная верификация - это не хуяк-хуяк: "Ваша программа верна", а буквально самому по шагам писать доказательство, только формально. Короче, хуйня без задач, не взлетела за десятилетия, не взлетает и не взлетит.
>>517501
Алгоритм? Разумеется, вручную проще. Реализацию? А вот тут уже нет, увы.
> В итоге выяснилось, что проще ручками доказать.
Алгоритм? Разумеется, вручную проще. Реализацию? А вот тут уже нет, увы.
>>489270
Есть и такое.
Мимоконструктивист
Жду, когда агды станут более удобо варимыми
>Никто и не говорит о формализации теорем из матана (хотя на самом деле хорошее занятие и упражнения).
Есть и такое.
Мимоконструктивист
Жду, когда агды станут более удобо варимыми
Раз зашел разговор про надёжность, расскажите, как в той же Агде, где функции "not allowed to crash", обрабатываются всевозможные переполнения: целочисленного, стека, памяти? Тут ведь исключительно от аппаратной составляющей зависит довольно много. Если совсем по-хардкору, следовало бы, пожалуй, компилятору самостоятельно определять системные требования, и соответствие им актуальной системы, что для общего случая и невозможно. В реальном-то мире как борятся с подобным непредсказуемым поведением системы? Есть ли какие-то популярные решения в языках неподдерживающих исключения?
>>517501
Ну дак а как ты думал, что оно все само? С тактиками ещё как-то можно, но все равно муторно.
>>517761
Не надо ждать, надо писать. Ну я пытаюсь в свободное время, но там дофига делать. Там ещё проблема в том, что стандартная библиотека бедновата.
>>517824
Всё зависит от бекенда. Потому что сейчас есть бекенд, который просто компилит в хаскелл, то есть перекладывает на него большинство проблем.
Ну дак а как ты думал, что оно все само? С тактиками ещё как-то можно, но все равно муторно.
>>517761
Не надо ждать, надо писать. Ну я пытаюсь в свободное время, но там дофига делать. Там ещё проблема в том, что стандартная библиотека бедновата.
>>517824
Всё зависит от бекенда. Потому что сейчас есть бекенд, который просто компилит в хаскелл, то есть перекладывает на него большинство проблем.
>>518178
Погугли Formalizing 100 theorems in HOL light.
Погугли Formalizing 100 theorems in HOL light.
Доставлю-ка сюда ещё один прувер.
https://github.com/leanprover/lean
Учебник: http://leanprover.github.io/tutorial/tutorial.pdf или https://leanprover.github.io/tutorial/index.html
https://github.com/leanprover/lean
Учебник: http://leanprover.github.io/tutorial/tutorial.pdf или https://leanprover.github.io/tutorial/index.html
Изучая вопрос часто встречаю утверждение, что функция принимает/возвращает некое доказательство. Что это вообще за материя? Есть ли подобное в бэйсике? С чем-нибудь из императивного програмирования это можно сравнить?
>>519079
Она со списками работает, получает два указателя, из одного списка создаёт другой.
С задачей быстрой сортировки проще всего сравнить.
А если делать на анафорических лямбдах, тах задачка вообще на пять минут.
Она со списками работает, получает два указателя, из одного списка создаёт другой.
С задачей быстрой сортировки проще всего сравнить.
А если делать на анафорических лямбдах, тах задачка вообще на пять минут.
>>519079
В языке с зависимыми типами, тип — то же самое, что предикат, а, соответственно, значение типа — высказывание. В то же время, тип функции соответствует формулировке теоремы, тело функции — доказательству (в смысле самого вывода их начальных положений того, что требуется), а результат функции — итоговому высказыванию. Это итоговое высказывание и называют обычно «доказательством» в смысле итогового результата.
Почитай http://docs.idris-lang.org/en/latest/tutorial/theorems.html, там не очень сложно.
Нет.
В языке с зависимыми типами, тип — то же самое, что предикат, а, соответственно, значение типа — высказывание. В то же время, тип функции соответствует формулировке теоремы, тело функции — доказательству (в смысле самого вывода их начальных положений того, что требуется), а результат функции — итоговому высказыванию. Это итоговое высказывание и называют обычно «доказательством» в смысле итогового результата.
Почитай http://docs.idris-lang.org/en/latest/tutorial/theorems.html, там не очень сложно.
> Есть ли подобное в бэйсике? С чем-нибудь из императивного програмирования это можно сравнить?
Нет.
>>519079
В бэйсике нет, но в любом статическом языке доказывается теорема, что программа не упадет от несовпадения типов. См. изоморфизм Карри — Ховарда.
В бэйсике нет, но в любом статическом языке доказывается теорема, что программа не упадет от несовпадения типов. См. изоморфизм Карри — Ховарда.
>>519088
Это мне ответ был? Прости, я ничего не понял.
>>519092
>>519103
Спасибо огромное, потихоньку проясняется.
Мало знаком с функциональным программированием, поэтому, для зацепки пытаюсь искать какие-то аналогии вещам знакомым.
Вот пример из Ады 2012:
subtype Even is Integer with
Dynamic_Predicate => Even rem 2 = 0;
теперь при попытке ассигнации переменной типа Even будет производиться проверка Dynamic_Predicate. Вопрос: это каким-то боком вообще касается исходной темы, или просто другой механизм повышения надёжности?
Это мне ответ был? Прости, я ничего не понял.
>>519092
>>519103
Спасибо огромное, потихоньку проясняется.
Мало знаком с функциональным программированием, поэтому, для зацепки пытаюсь искать какие-то аналогии вещам знакомым.
>В языке с зависимыми типами, тип — то же самое, что предикат
Вот пример из Ады 2012:
subtype Even is Integer with
Dynamic_Predicate => Even rem 2 = 0;
теперь при попытке ассигнации переменной типа Even будет производиться проверка Dynamic_Predicate. Вопрос: это каким-то боком вообще касается исходной темы, или просто другой механизм повышения надёжности?
>>519172
...во время выполнения, верно?
> при попытке ассигнации переменной типа Even будет производиться проверка Dynamic_Predicate
...во время выполнения, верно?
>>519215
Абсолютно. А принципиальна именно проверка на этапе компиляции?
Кстати, подобный механизм, ведь, в принципе, будет работать при сборке: константу можно проверить сразу, для произвольного значения - принудительно проверять на вхождение в подтип (if Dynamic_Predicate(val) then ev := val) перед присваиванием? Это и имеется ввиду?
>...во время выполнения, верно?
Абсолютно. А принципиальна именно проверка на этапе компиляции?
Кстати, подобный механизм, ведь, в принципе, будет работать при сборке: константу можно проверить сразу, для произвольного значения - принудительно проверять на вхождение в подтип (if Dynamic_Predicate(val) then ev := val) перед присваиванием? Это и имеется ввиду?
Вас не заебало ещё этим изоморфизмом везде тыкать, профаны? Паверсет натуральных чисел тоже изоморфен действительным числам и ни один из этих изоморфизмов не вычислим. Мы говорим о конкретных задачах из практики, а не о овечках в облаках. Пока что доказательства приходится выводить, как мы уже неоднократно убедились, ручками. Вопрос: почему прошло столько времени и нет видимого, признаваемого комьюнити прогресса? Почему даже ФЯП, в конце концов, не в продакшене? Десятилетия прошли, сколько ещё ждать? Ещё несколько десятилетий?
>>519255
Говноеды, вот что такое настоящая математика
правильное объяснение такое: пусть у нас есть мнимое квадратичное поле, порожденное целым x, Q(x), тогда его поле классов - Q(x,j(x)), где j(x) тоже целое, а j - это j-инвариант эллиптической кривой; утверждение называется "теорема Вебера" и является составной частью югендтраума тов. Кронекера, про то, что ежели все абелевы расширения Q порождаются полями деления круга, то расширения мнимых квадратичных полей соответствуют эллиптическим кривым с комплексным умножением и порождаются полями деления лемнискаты, по-научному называемыми целыми значениями эллиптических интегралов; делением лемнискаты занимался ещё Гаусс (кроме построения правильного n-угольника он доказал, что циркулем и линейкой можно разделить лемнискату на n равных частей ровно для тех же n). тот же Гаусс занимался мнимыми квадратичными полями, и высказал гипотезу, что число м.к.п. с числом классов 1 (т.е. у которых целые являются областями главных идеалов, и не возникает проблемы с неоднозначным разложением на множители) конечно, и даже представил список, оканчивающийся как раз на корень из минус 163 (при том, что в явном виде об идеалах и дивизорах у Гаусса, конечно, никакого представления не было, и число классов он определял через классы эквивалентных квадратичных форм). так вот, если применить теорему Вебера к Q(\sqrt{-163}), получим, что все идеалы уже и так главные, и поле классов совпадает с самим полем, т.е. j(x) лежит в Q(x). более того, есть формула для j-инварианта, о которой ниже, из неё следует, что j вещественен, т.е. лежит в Z (последнее до меня дошло только что :). дело в том, что j-инвариант не просто так называется - он действительно инвариант эллиптической кривой; эллиптическая кривая - это точка верхней полуплоскости с точностью до действия PSL_2(Z)-модулярной группы; т.е. точка на модулярной кривой - факторе верхней полуплоскости по действию группы; т.е. j-инвариант - это функция на верхней полуплоскости, инвариантная относительно действия; такие функции называются модулярными. в частности, они инвариантны относительно сдвига z|->z+1, поэтому их можно представить, как ряды Лорана от q=e^{2{\pi}iz}. в этом ряду у j простой полюс в 0 с вычетом 1 (т.е. член 1/q), потом идёт 744, потом члены при q, q^2, etc.
вернёмся к нашему мнимому квадратичному полю с числом классов 1. целые его, конечно, порождаются не sqrt{-163}, а {1+\sqrt{-163}} \over 2. это x. мы знаем, что j(x) - целое, и у нас есть ряд для j(q), q=e^{2{\pi}ix}. ну вот, собственно, и всё - j(q) целое, 1/q=-e^{\sqrt{163}}, 744 целое, а q очень маленькое и его степени - тем более. заодно получается целость, помимо 163, ещё и 67, 43, 19, 11, но они, конечно, похуже, потому что q уже не такое маленькое.
что интересно, оставшиеся коэффициенты при q^n в разложении тоже целые, и являются размерностями градуировок специальной вертексной алгебры, на которой действует группа-монстр, и про сие придумана специальная суперструнная лунатичная теория
Говноеды, вот что такое настоящая математика
правильное объяснение такое: пусть у нас есть мнимое квадратичное поле, порожденное целым x, Q(x), тогда его поле классов - Q(x,j(x)), где j(x) тоже целое, а j - это j-инвариант эллиптической кривой; утверждение называется "теорема Вебера" и является составной частью югендтраума тов. Кронекера, про то, что ежели все абелевы расширения Q порождаются полями деления круга, то расширения мнимых квадратичных полей соответствуют эллиптическим кривым с комплексным умножением и порождаются полями деления лемнискаты, по-научному называемыми целыми значениями эллиптических интегралов; делением лемнискаты занимался ещё Гаусс (кроме построения правильного n-угольника он доказал, что циркулем и линейкой можно разделить лемнискату на n равных частей ровно для тех же n). тот же Гаусс занимался мнимыми квадратичными полями, и высказал гипотезу, что число м.к.п. с числом классов 1 (т.е. у которых целые являются областями главных идеалов, и не возникает проблемы с неоднозначным разложением на множители) конечно, и даже представил список, оканчивающийся как раз на корень из минус 163 (при том, что в явном виде об идеалах и дивизорах у Гаусса, конечно, никакого представления не было, и число классов он определял через классы эквивалентных квадратичных форм). так вот, если применить теорему Вебера к Q(\sqrt{-163}), получим, что все идеалы уже и так главные, и поле классов совпадает с самим полем, т.е. j(x) лежит в Q(x). более того, есть формула для j-инварианта, о которой ниже, из неё следует, что j вещественен, т.е. лежит в Z (последнее до меня дошло только что :). дело в том, что j-инвариант не просто так называется - он действительно инвариант эллиптической кривой; эллиптическая кривая - это точка верхней полуплоскости с точностью до действия PSL_2(Z)-модулярной группы; т.е. точка на модулярной кривой - факторе верхней полуплоскости по действию группы; т.е. j-инвариант - это функция на верхней полуплоскости, инвариантная относительно действия; такие функции называются модулярными. в частности, они инвариантны относительно сдвига z|->z+1, поэтому их можно представить, как ряды Лорана от q=e^{2{\pi}iz}. в этом ряду у j простой полюс в 0 с вычетом 1 (т.е. член 1/q), потом идёт 744, потом члены при q, q^2, etc.
вернёмся к нашему мнимому квадратичному полю с числом классов 1. целые его, конечно, порождаются не sqrt{-163}, а {1+\sqrt{-163}} \over 2. это x. мы знаем, что j(x) - целое, и у нас есть ряд для j(q), q=e^{2{\pi}ix}. ну вот, собственно, и всё - j(q) целое, 1/q=-e^{\sqrt{163}}, 744 целое, а q очень маленькое и его степени - тем более. заодно получается целость, помимо 163, ещё и 67, 43, 19, 11, но они, конечно, похуже, потому что q уже не такое маленькое.
что интересно, оставшиеся коэффициенты при q^n в разложении тоже целые, и являются размерностями градуировок специальной вертексной алгебры, на которой действует группа-монстр, и про сие придумана специальная суперструнная лунатичная теория
>>519255
Говноеды, вот что такое настоящая математика
правильное объяснение такое: пусть у нас есть мнимое квадратичное поле, порожденное целым x, Q(x), тогда его поле классов - Q(x,j(x)), где j(x) тоже целое, а j - это j-инвариант эллиптической кривой; утверждение называется "теорема Вебера" и является составной частью югендтраума тов. Кронекера, про то, что ежели все абелевы расширения Q порождаются полями деления круга, то расширения мнимых квадратичных полей соответствуют эллиптическим кривым с комплексным умножением и порождаются полями деления лемнискаты, по-научному называемыми целыми значениями эллиптических интегралов; делением лемнискаты занимался ещё Гаусс (кроме построения правильного n-угольника он доказал, что циркулем и линейкой можно разделить лемнискату на n равных частей ровно для тех же n). тот же Гаусс занимался мнимыми квадратичными полями, и высказал гипотезу, что число м.к.п. с числом классов 1 (т.е. у которых целые являются областями главных идеалов, и не возникает проблемы с неоднозначным разложением на множители) конечно, и даже представил список, оканчивающийся как раз на корень из минус 163 (при том, что в явном виде об идеалах и дивизорах у Гаусса, конечно, никакого представления не было, и число классов он определял через классы эквивалентных квадратичных форм). так вот, если применить теорему Вебера к Q(\sqrt{-163}), получим, что все идеалы уже и так главные, и поле классов совпадает с самим полем, т.е. j(x) лежит в Q(x). более того, есть формула для j-инварианта, о которой ниже, из неё следует, что j вещественен, т.е. лежит в Z (последнее до меня дошло только что :). дело в том, что j-инвариант не просто так называется - он действительно инвариант эллиптической кривой; эллиптическая кривая - это точка верхней полуплоскости с точностью до действия PSL_2(Z)-модулярной группы; т.е. точка на модулярной кривой - факторе верхней полуплоскости по действию группы; т.е. j-инвариант - это функция на верхней полуплоскости, инвариантная относительно действия; такие функции называются модулярными. в частности, они инвариантны относительно сдвига z|->z+1, поэтому их можно представить, как ряды Лорана от q=e^{2{\pi}iz}. в этом ряду у j простой полюс в 0 с вычетом 1 (т.е. член 1/q), потом идёт 744, потом члены при q, q^2, etc.
вернёмся к нашему мнимому квадратичному полю с числом классов 1. целые его, конечно, порождаются не sqrt{-163}, а {1+\sqrt{-163}} \over 2. это x. мы знаем, что j(x) - целое, и у нас есть ряд для j(q), q=e^{2{\pi}ix}. ну вот, собственно, и всё - j(q) целое, 1/q=-e^{\sqrt{163}}, 744 целое, а q очень маленькое и его степени - тем более. заодно получается целость, помимо 163, ещё и 67, 43, 19, 11, но они, конечно, похуже, потому что q уже не такое маленькое.
что интересно, оставшиеся коэффициенты при q^n в разложении тоже целые, и являются размерностями градуировок специальной вертексной алгебры, на которой действует группа-монстр, и про сие придумана специальная суперструнная лунатичная теория
Говноеды, вот что такое настоящая математика
правильное объяснение такое: пусть у нас есть мнимое квадратичное поле, порожденное целым x, Q(x), тогда его поле классов - Q(x,j(x)), где j(x) тоже целое, а j - это j-инвариант эллиптической кривой; утверждение называется "теорема Вебера" и является составной частью югендтраума тов. Кронекера, про то, что ежели все абелевы расширения Q порождаются полями деления круга, то расширения мнимых квадратичных полей соответствуют эллиптическим кривым с комплексным умножением и порождаются полями деления лемнискаты, по-научному называемыми целыми значениями эллиптических интегралов; делением лемнискаты занимался ещё Гаусс (кроме построения правильного n-угольника он доказал, что циркулем и линейкой можно разделить лемнискату на n равных частей ровно для тех же n). тот же Гаусс занимался мнимыми квадратичными полями, и высказал гипотезу, что число м.к.п. с числом классов 1 (т.е. у которых целые являются областями главных идеалов, и не возникает проблемы с неоднозначным разложением на множители) конечно, и даже представил список, оканчивающийся как раз на корень из минус 163 (при том, что в явном виде об идеалах и дивизорах у Гаусса, конечно, никакого представления не было, и число классов он определял через классы эквивалентных квадратичных форм). так вот, если применить теорему Вебера к Q(\sqrt{-163}), получим, что все идеалы уже и так главные, и поле классов совпадает с самим полем, т.е. j(x) лежит в Q(x). более того, есть формула для j-инварианта, о которой ниже, из неё следует, что j вещественен, т.е. лежит в Z (последнее до меня дошло только что :). дело в том, что j-инвариант не просто так называется - он действительно инвариант эллиптической кривой; эллиптическая кривая - это точка верхней полуплоскости с точностью до действия PSL_2(Z)-модулярной группы; т.е. точка на модулярной кривой - факторе верхней полуплоскости по действию группы; т.е. j-инвариант - это функция на верхней полуплоскости, инвариантная относительно действия; такие функции называются модулярными. в частности, они инвариантны относительно сдвига z|->z+1, поэтому их можно представить, как ряды Лорана от q=e^{2{\pi}iz}. в этом ряду у j простой полюс в 0 с вычетом 1 (т.е. член 1/q), потом идёт 744, потом члены при q, q^2, etc.
вернёмся к нашему мнимому квадратичному полю с числом классов 1. целые его, конечно, порождаются не sqrt{-163}, а {1+\sqrt{-163}} \over 2. это x. мы знаем, что j(x) - целое, и у нас есть ряд для j(q), q=e^{2{\pi}ix}. ну вот, собственно, и всё - j(q) целое, 1/q=-e^{\sqrt{163}}, 744 целое, а q очень маленькое и его степени - тем более. заодно получается целость, помимо 163, ещё и 67, 43, 19, 11, но они, конечно, похуже, потому что q уже не такое маленькое.
что интересно, оставшиеся коэффициенты при q^n в разложении тоже целые, и являются размерностями градуировок специальной вертексной алгебры, на которой действует группа-монстр, и про сие придумана специальная суперструнная лунатичная теория
Хватит уже пастами меряться. Пишите по теме.
>>519239
В этом вся соль. Именно поэтому идёт речь о доказательствах, а не проверках. Основная идея довольно проста: например, пусть есть тип
```
data (=) : a -> b -> Type where
Refl : x = x
```
Хотя `x` может быть чем угодно (хоть термом), значение типа (=) можно создать лишь единственным способом: x = x.
Отсюда можно легко доказать:
```
trans : (a = b) -> (b = c) -> a = c
trans Refl Refl = Refl
```
В самом деле: так как единственный способ построить (=) является Refl (или x = x), то аргументы функции trans не могут быть отличны от, к примеру, (b = b), как и результат функции. Обрати внимание, чтобы это доказать не потребовалось никаких вычислений во время выполнения, на самом деле мы даже не знаем, чему равно b!
> А принципиальна именно проверка на этапе компиляции?
В этом вся соль. Именно поэтому идёт речь о доказательствах, а не проверках. Основная идея довольно проста: например, пусть есть тип
```
data (=) : a -> b -> Type where
Refl : x = x
```
Хотя `x` может быть чем угодно (хоть термом), значение типа (=) можно создать лишь единственным способом: x = x.
Отсюда можно легко доказать:
```
trans : (a = b) -> (b = c) -> a = c
trans Refl Refl = Refl
```
В самом деле: так как единственный способ построить (=) является Refl (или x = x), то аргументы функции trans не могут быть отличны от, к примеру, (b = b), как и результат функции. Обрати внимание, чтобы это доказать не потребовалось никаких вычислений во время выполнения, на самом деле мы даже не знаем, чему равно b!
>>519377
Прости, серьёзно завис над синтаксисом:
Это тип/функция принимающая два аргумента, так? Refl - конструктор принмающий один(x)?
В Refl : x = x знак "=" это, скажем, служебный символ или рекурсивный вызов? Так и не нашёл где бы описывали язык целиком, а не его отличия от хаскеля.
Это и есть тип-доказательство? Боюсь спросить глупость, но как его теперь использовать?
Ещё раз про чётность/нечётность: нашёл определение на idris этих, собственно, понятий, так вот определения компилятору достаточно для того, чтобы установить четность суммы нечетных, или тоже требуется доказательство?
Прости, серьёзно завис над синтаксисом:
>data (=) : a -> b -> Type where
Это тип/функция принимающая два аргумента, так? Refl - конструктор принмающий один(x)?
В Refl : x = x знак "=" это, скажем, служебный символ или рекурсивный вызов? Так и не нашёл где бы описывали язык целиком, а не его отличия от хаскеля.
>```
>trans : (a = b) -> (b = c) -> a = c
>trans Refl Refl = Refl
>```
Это и есть тип-доказательство? Боюсь спросить глупость, но как его теперь использовать?
Ещё раз про чётность/нечётность: нашёл определение на idris этих, собственно, понятий, так вот определения компилятору достаточно для того, чтобы установить четность суммы нечетных, или тоже требуется доказательство?
>>519895
Это конструктор типа, берущий два значения. А Refl -- конструктор значения типа. Гугли "обобщённые алгебраические типы" или GADT.
http://habrahabr.ru/post/207126/ может помочь.
Опять же, конструктор типа. Смысл такой: для некого `x` можно построить единственное значение типа `x = x` с помощью конструктора Refl.
Нужно отметить, что компилятор не может привести произвольные термы к виду `x = x` (эта задача, вообще говоря, неразрешима), так что приходится делать это вручную.
Хаскель стоит знать, тем более что и Agda, и Idris весьма близки к нему.
Если у тебя есть значение типа `a = b` и `b = c`, то с помощью функции trans можно получить значение типа `a = c`. Потому что опять же, автоматически оно у тебя не появится.
Надо доказывать. Но там доказательство совсем простое будет.
> Это тип/функция принимающая два аргумента, так?
Это конструктор типа, берущий два значения. А Refl -- конструктор значения типа. Гугли "обобщённые алгебраические типы" или GADT.
http://habrahabr.ru/post/207126/ может помочь.
> В Refl : x = x знак "=" это, скажем, служебный символ или рекурсивный вызов?
Опять же, конструктор типа. Смысл такой: для некого `x` можно построить единственное значение типа `x = x` с помощью конструктора Refl.
Нужно отметить, что компилятор не может привести произвольные термы к виду `x = x` (эта задача, вообще говоря, неразрешима), так что приходится делать это вручную.
> Так и не нашёл где бы описывали язык целиком, а не его отличия от хаскеля.
Хаскель стоит знать, тем более что и Agda, и Idris весьма близки к нему.
> Это и есть тип-доказательство? Боюсь спросить глупость, но как его теперь использовать?
Если у тебя есть значение типа `a = b` и `b = c`, то с помощью функции trans можно получить значение типа `a = c`. Потому что опять же, автоматически оно у тебя не появится.
> Ещё раз про чётность/нечётность: нашёл определение на idris этих, собственно, понятий, так вот определения компилятору достаточно для того, чтобы установить четность суммы нечетных, или тоже требуется доказательство?
Надо доказывать. Но там доказательство совсем простое будет.
Я тут разбираюсь с Agda и у меня есть вопросы.
Есть ли где-нибудь лаконичное и четкое описание какого-нибудь варианта MLTT?
Я некоторое время назад формализовал совершенно не впечатляющую теорему о том, что произведение натурального на четное четно. В процессе я доказал и лемму о том, что сумма двух нечетных четна. Но это произошло на 126 строке и все что выше было нужно для этой леммы. Правда в учебных целях я ничего не импортировал и если вместо ручного доказательства ассоциативности сложения и т.п. импортировать его из стандартной библиотеки, то все-равно разработка теории четности до этой леммы заняла бы строк 30. Как утверждает >>519909 подобные вещи делаются очень просто. Можно ли показать, как? Или несколько десятков строк - это и есть совсем просто?
Есть ли где-нибудь лаконичное и четкое описание какого-нибудь варианта MLTT?
Я некоторое время назад формализовал совершенно не впечатляющую теорему о том, что произведение натурального на четное четно. В процессе я доказал и лемму о том, что сумма двух нечетных четна. Но это произошло на 126 строке и все что выше было нужно для этой леммы. Правда в учебных целях я ничего не импортировал и если вместо ручного доказательства ассоциативности сложения и т.п. импортировать его из стандартной библиотеки, то все-равно разработка теории четности до этой леммы заняла бы строк 30. Как утверждает >>519909 подобные вещи делаются очень просто. Можно ли показать, как? Или несколько десятков строк - это и есть совсем просто?
17 Кб, 604x439
>
> что произведение натурального на четное четно. В процессе я доказал и лемму о том, что сумма двух нечетных четна. Но это произошло на 126 строке и все что выше было нужно для этой леммы.
Вся суть потуг петушков-формализаторов
>>520983
Конечно гораздо проще немного помахать руками и сказать что утверждение очевидно. Правда, немного неприятно, когда через двадцать лет в утверждении находят небольшую неточность.
Конечно гораздо проще немного помахать руками и сказать что утверждение очевидно. Правда, немного неприятно, когда через двадцать лет в утверждении находят небольшую неточность.
>>521017
Но ведь вывод - тоже махание руками, только на процессоре. А ну как у него в микрокоде баг?
Но ведь вывод - тоже махание руками, только на процессоре. А ну как у него в микрокоде баг?
>>521017
Тащемта, история знает несколько формализаторов, которые доказали, а потом нашлась небольшая неточность. Например, про летательные аппараты тяжелее воздуха, летательные аппараты с вертикальным взлётом, (iirc) подводные лодки и известный каждому быдлану шмель.
Алсо, у тебя нет доказательств, что в твоём доказаторе нет бага. Скормить доказатор доказатору ты, по понятным причинам, не можешь. И это не говоря уже про то, что ты не можешь доказать, что ты доказал именно то, что хотел доказать, а не что-то другое, просто похожее. И такие "нет" и "не можешь" можно ещё продолжать.
Тащемта, история знает несколько формализаторов, которые доказали, а потом нашлась небольшая неточность. Например, про летательные аппараты тяжелее воздуха, летательные аппараты с вертикальным взлётом, (iirc) подводные лодки и известный каждому быдлану шмель.
Алсо, у тебя нет доказательств, что в твоём доказаторе нет бага. Скормить доказатор доказатору ты, по понятным причинам, не можешь. И это не говоря уже про то, что ты не можешь доказать, что ты доказал именно то, что хотел доказать, а не что-то другое, просто похожее. И такие "нет" и "не можешь" можно ещё продолжать.
>>521054
Ты совсем ебанутый? При чем тут математика вообще?
>Например, про летательные аппараты тяжелее воздуха
Ты совсем ебанутый? При чем тут математика вообще?
>>521053
Ну а как ты хотел, обколются своими "доказательствами" тавтологий и тащут на двач.
Ну а как ты хотел, обколются своими "доказательствами" тавтологий и тащут на двач.
>>521054
Если на то пошло, то если в прувере заданы хотя бы элементарные аксиомы арифметики, то окончательного доказательства, что противоречие не возникнет, быть не может.
Если на то пошло, то если в прувере заданы хотя бы элементарные аксиомы арифметики, то окончательного доказательства, что противоречие не возникнет, быть не может.
Я, слыхал было, что Агда и Эпиграмм, кажется, запрещают бесконечную рекурсию. Каким образом это вообще реализуемо? Кто-нибудь интересовался? По каким словам это может гуглиться?
>>523178
Изоморфизм Карри-Говарда в действии. Эти языки являются одновременно языками программирования и конструктивными формальными теориями. Любая программа - это конструктивное доказательство существования чего-то (зависит от типа). Но конструктивное доказательство может соответствовать только обрывающемуся процессу вычислений.
Изоморфизм Карри-Говарда в действии. Эти языки являются одновременно языками программирования и конструктивными формальными теориями. Любая программа - это конструктивное доказательство существования чего-то (зависит от типа). Но конструктивное доказательство может соответствовать только обрывающемуся процессу вычислений.
>>523178
Гугли total functional programming.
> Каким образом это вообще реализуемо? По каким словам это может гуглиться?
Гугли total functional programming.
>>523178
Quantifier free induction. Погугли
Quantifier free induction. Погугли
4 Кб, 208x104
Какой прувер мне выучить и что вообще почитать, чтобы генерировать автоматические решения такого как на пикрелейтед для n. Причём p<q - параметры, которые задано символьно. А то, кажется, ни одна система комп. алгебры не может толком в параметризованные суммы и продукты.
Поиграть принёс: https://www.verigames.com/reg/form
Пообщался с автором вот этого чуда http://www.mathematik.uni-muenchen.de/~logik/minlog/index.php
К таким на сраной козе не подъедешь. Хорошо иметь немецкий PhD и подписываться работником престижного немецкого вуза :) Профессор мне очень интересные вещи рассказал. Надо бы взяться за эту няшу. А то все доказательства делаю ручками уже много лет.
Мимо конструктивист-прикладник
К таким на сраной козе не подъедешь. Хорошо иметь немецкий PhD и подписываться работником престижного немецкого вуза :) Профессор мне очень интересные вещи рассказал. Надо бы взяться за эту няшу. А то все доказательства делаю ручками уже много лет.
Мимо конструктивист-прикладник
Бамп же ёпты, ну.
На правах бампа и вдогонку >>517824 изобилирующее очевидностью рассуждение о достижимости тотальности.
Пусть некая содержащая неоптимизируюемую рекурсию функция корректно исполняется будучи вызванной из корня программы, и рушится с переполнением стека при вызове из процедуры некоторой вложенности. Для определения некоторой абсолютной тотальности алгоритму потребовались бы данные о сложности самих функций, вызывающих их фунциях и их вложенности, доступных ресурсах и самая писечка: подробная, вполоть до количества и разрядности регистров (т.к. это влияет на размер фрейма и не только), информация о самой вычислительной машине. Для задач же критичных ко времени требуется ещё куда более глубокая и детальная проработка анализатора. Задача, на мой взгляд, вполне разрешимая, однако код на языке поддерживающем подобные возможности был бы крайне громоздким. Уж куда многословней тех же исключений.
Собственно вопрос мой в том, насколько подобная абсолютная тотальность выходит за горизонты практического применения обсуждаемых сдесь средств, и насколько их пользователи удовлетворены существующими ныне компромисами.
Пусть некая содержащая неоптимизируюемую рекурсию функция корректно исполняется будучи вызванной из корня программы, и рушится с переполнением стека при вызове из процедуры некоторой вложенности. Для определения некоторой абсолютной тотальности алгоритму потребовались бы данные о сложности самих функций, вызывающих их фунциях и их вложенности, доступных ресурсах и самая писечка: подробная, вполоть до количества и разрядности регистров (т.к. это влияет на размер фрейма и не только), информация о самой вычислительной машине. Для задач же критичных ко времени требуется ещё куда более глубокая и детальная проработка анализатора. Задача, на мой взгляд, вполне разрешимая, однако код на языке поддерживающем подобные возможности был бы крайне громоздким. Уж куда многословней тех же исключений.
Собственно вопрос мой в том, насколько подобная абсолютная тотальность выходит за горизонты практического применения обсуждаемых сдесь средств, и насколько их пользователи удовлетворены существующими ныне компромисами.
>>483770 (OP)
вот взять так и уебать этим псевдоакадемическим петушкам
когда внезапно приходит Vect n+1 a, а у тебя в коде Vect n+2 a и всё идёт по пизде
вообще на практике никто на этой параше писать не будет, потому что неподдерживаемо
вот взять так и уебать этим псевдоакадемическим петушкам
когда внезапно приходит Vect n+1 a, а у тебя в коде Vect n+2 a и всё идёт по пизде
вообще на практике никто на этой параше писать не будет, потому что неподдерживаемо
>>540472
Что ж ты возгорелся-то так? Просто напиши тактику, которая всё за тебя сделает.
Что ж ты возгорелся-то так? Просто напиши тактику, которая всё за тебя сделает.
>>540486
Не boilerplate, у тактик многоразовое применение.
С одной стороны — контроль, с другой — можно делать вещи, которые в обычных статически типизированных языках делать нельзя.
Не boilerplate, у тактик многоразовое применение.
> ради чего?
С одной стороны — контроль, с другой — можно делать вещи, которые в обычных статически типизированных языках делать нельзя.
>>540559
Ну, например, типобезопасный printf без костылей вроде макросов:
http://www.youtube.com/watch?v=fVBck2Zngjo
Или вот реализация бинарного формата:
http://www.youtube.com/watch?v=AWeT_G04a0A (с 24 минуты)
> приведи какой-нибудь пример
Ну, например, типобезопасный printf без костылей вроде макросов:
http://www.youtube.com/watch?v=fVBck2Zngjo
Или вот реализация бинарного формата:
http://www.youtube.com/watch?v=AWeT_G04a0A (с 24 минуты)
Смотрите чо https://www.manning.com/books/type-driven-development-with-idris
Неужели Idris уже такой мейнстрим?
Неужели Idris уже такой мейнстрим?
>Также можно доказать корректность реализации FizzBuzz'а, сортировки слиянием, даже неба, даже аллаха.
На уровне "можнозделать", подозреваю. Есть работающий пример программы на языке с зависимыми типами доказывающей корректность, скажем, алгоритма Крускала?
>>543673
Квадрочую вопрос и добавляю свой.
Вычитал где-то, что Идрис в своей работе производит деконструкцию типа. Как я это понял: можно определить функцию (дальше псевдо с) вида
void quad_matrix_foo(int matrix[L*L]){...};
которая будет принимать исключительно массивы длинной в квадрат целого числа.
Правильно ли я понимаю, что для любого вызова будет произведён разбор аргумента и проверка на принадлежность к квадратам? Оно вообще вычислимо для случая посложнее, например тригонометрии и прочего?
Или же необходимо самостоятельно доказывать корректность аргумента, или создавать новый, уже нужного типа? А как вырвать нужный тип из уже определенного через другие операции числа?
Надеюсь понятно описал, поясните пожалуйста.
Квадрочую вопрос и добавляю свой.
Вычитал где-то, что Идрис в своей работе производит деконструкцию типа. Как я это понял: можно определить функцию (дальше псевдо с) вида
void quad_matrix_foo(int matrix[L*L]){...};
которая будет принимать исключительно массивы длинной в квадрат целого числа.
Правильно ли я понимаю, что для любого вызова будет произведён разбор аргумента и проверка на принадлежность к квадратам? Оно вообще вычислимо для случая посложнее, например тригонометрии и прочего?
Или же необходимо самостоятельно доказывать корректность аргумента, или создавать новый, уже нужного типа? А как вырвать нужный тип из уже определенного через другие операции числа?
Надеюсь понятно описал, поясните пожалуйста.
Тред утонул или удален.
Это копия, сохраненная 15 октября 2015 года.
Скачать тред: только с превью, с превью и прикрепленными файлами.
Второй вариант может долго скачиваться. Файлы будут только в живых или недавно утонувших тредах. Подробнее
Если вам полезен архив М.Двача, пожертвуйте на оплату сервера.
Это копия, сохраненная 15 октября 2015 года.
Скачать тред: только с превью, с превью и прикрепленными файлами.
Второй вариант может долго скачиваться. Файлы будут только в живых или недавно утонувших тредах. Подробнее
Если вам полезен архив М.Двача, пожертвуйте на оплату сервера.