М.Двач / Программирование

Этого треда уже нет.
Это копия, сохраненная 15 октября 2015 года.

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

Если вам полезен архив М.Двача, пожертвуйте на оплату сервера.

669 Кб, 479x1417

Зависимых типов тред 24 Май, 11:55 #483770 В конец треда | Веб

ИТТ обсуждают языки с зависимыми типами (Idris, Agda, Coq, ATS и другие).

Что: зависимый тип — тип, который может быть параметризован не только другим типом, но и термом. Простой пример такого типа — Vect n a, где n — натуральное число, а a — тип. Кроме того, в языках с зависимыми типами типы являются объектами первого класса.
Зачем: благодаря изоморфизму Карри — Ховарда, можно не только писать факториалы и числа Фибоначчи, но и доказывать корректность их реализации. Также можно доказать корректность реализации FizzBuzz'а, сортировки слиянием, даже неба, даже аллаха. Кроме того, зависимые типы обладают большей выразительностью, чем, к примеру, система типов в Haskell.

Ответы: >>483774, >>483853, >>484184, >>485133

24 Май, 12:08 #2 #483774

>>483770
Только изоморфизм Карри — Ховарда существует между программами на лямбда исчихлении с типами и мат. логикой. Так как 99% программ - не на лямбда исчислении, а многие из них ещё и без типов, то доказывать остаётся только собственные факториалы на хачкеле. Охуенно.

24 Май, 12:21 #3 #483777

И теперь вопрос, зачем это всё нужно, если есть логика Хоара и Сепарационная логика, с помощью которых можно верифицировать обычные императивные программы с мутабельными структурами, в том числе содержащие указатели?

Ответы: >>483781

24 Май, 12:53 #4 #483781

>>483777
Зависимые типы пригодны не только для ФП. См. ATS (http://www.ats-lang.org/Papers.html) как пример.

24 Май, 14:25 #5 #483853

>>483770
>Простой пример такого типа — Vect n a, где n — натуральное число, а a — тип
Нихуя не понял. Я в крестах могу такое сделать, в чем соль-то?

Ответы: >>483861

sage 24 Май, 14:31 #6 #483861

>>483853
тип вектора зависит от его длины
> Я в крестах могу такое сделать
лол ну сделай

Ответы: >>483873

24 Май, 14:41 #7 #483871

Я так понимаю эта хуйня имеет прикладное применение только в академии? Т.е. обычному быдлу вроде меня кроме как дома за борщом оно нигде не пригодится?

Ответы: >>484116

24 Май, 14:45 #8 #483873

>>483861
> тип вектора зависит от его длины
Что-то вроде
> template<uint n, typename T> Vector
И?

Что за зависимые типы, нахуй? Пиздец.

Ответы: >>483879, >>483961, >>484460

sage 24 Май, 14:52 #9 #483879

>>483873
нет

> Что за зависимые типы, нахуй?
збс отвечаю

Ответы: >>483880

sage 24 Май, 14:54 #10 #483880

>>483879
Что нет? Почему нет? Если ты нормально объяснить не можешь, значит ты нихуя не понимаешь в теме, и нахуй ты тогда тред создал, мудила? У меня бомбит прямо.

Ответы: >>483890

sage 24 Май, 15:02 #11 #483890

>>483880
да

24 Май, 17:19 #12 #483961

>>483873
> template<uint n, typename T> Vector
Малаца. А теперь пусть твой `uint n` неизвестен во время компиляции.

Ответы: >>483973

24 Май, 17:32 #13 #483973

>>483961
> усть твой `uint n` неизвестен во время компиляции
Так у вас сдесь динамикодрисня? Почему сразу не предупреждаете?

Ответы: >>483982

24 Май, 17:37 #14 #483982

>>483973
> Так у вас сдесь динамикодрисня?
Неправильно, попробуй ещё раз.

Ответы: >>483997

24 Май, 17:54 #15 #483997

>>483982
>попробуй ещё раз
Ну, статическая типизация - тип определяется во время объявления, тоесть известен во время компиляции. Динамическая типизация - тип определяется по время присваивания значения, тоесть может не быть известен во время компиляции.
> твой `uint n` неизвестен во время компиляции
Вердикт - динамикодрисня.

Ответы: >>484000

24 Май, 17:57 #16 #484000

Например, пусть есть функция конкатенации двух списков вида:
(++) : Vect n a -> Vect m a -> Vect (n + m) a
Компилятор, вообще говоря, не знает, чему равно n. И чему равно m не знает. Но тем не менее, он способен статически проверить, что функция (++) действительно для любых двух векторов с длинами n и m вернёт вектор с длиной (n + m).

>>483997
> Вердикт - динамикодрисня.
Неправильно, попробуй ещё раз.

Ответы: >>484007, >>484056

24 Май, 18:02 #17 #484006

а разгадка проста: терм это не совсем значение

Ответы: >>484014

24 Май, 18:03 #18 #484007

>>484000
> ко ко ко ко
> попробуй ещё раз
Чтобы еще раз услышать вскукареки динамикопитушка? Я лучше скрою тред.

sage 24 Май, 18:10 #19 #484014

>>484006
Окай, но что мешает заебашить твои термы на типах в тех же крестах и проверять себе что хочешь на этапе компиляции, м?

Ответы: >>484018

sage 24 Май, 18:16 #20 #484018

>>484014
Лол, ну заебашь.

41 Кб, 373x457

sage 24 Май, 18:23 #21 #484023

обиженный байтуx пытается устроить срач итт
oкрoпил yриной мaнькин рoтeшник
брызги урины алсо задели рнр тредик

Ответы: >>484047

sage 24 Май, 18:51 #22 #484047

>>484023
Такие-то проекции. Иди кушать, борщ стынет.

24 Май, 18:59 #23 #484056

>>484000
http://ideone.com/MeKYz1
Вот так нужно сделать или что?
Вообще я считал что плюсы единственный мейнстримный язык с зависимыми типами. Конечно корявыми, но вроде утверждение верное. Да даже если бы и нельзя было складывать эти инты - всё равно анон должен был почуять что обосрался когда один тип начал зависеть от некоторой величины.
_другой анон_

Ответы: >>484058, >>484093, >>484104

24 Май, 19:02 #24 #484058

>>484056
ха лол может звездочками сработает

24 Май, 19:38 #25 #484093

>>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

Изобрази мне пример подобной проверки типов на С++.

Ответы: >>484130

24 Май, 19:47 #26 #484104

>>484056
А можешь сделать так, чтобы дефолтный конструктор возвращал вектор нужной длины в зависимости от типа?

Ответы: >>484137

24 Май, 20:03 #27 #484116

>>483871
Даже в академических кругах эту хуйню считают слишком академической, там что копай глубже.

73 Кб, 315x332

24 Май, 20:14 #28 #484125

dotty anyone?

24 Май, 20:26 #29 #484130

>>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
Разумеется я не знаю как это выглядит

Ответы: >>484143, >>484153, >>484196

24 Май, 20:39 #30 #484137

>>484104
Странная просьба не находишь?
Вот если бы ты попросил ограничить тип в темплейте то да я бы сказал что тут плюсы сосут (хотя есть костыли со специализацией). Хотя я их вроде и не защищал здесь.

А так вроде конструктор создаётся при вызове пользователем vec<T,N> v; где T и N любые.
Можно сделать внешнюю функцию с типом T и специализировать под несколько типов
template<>
vec<int> vec_constructor<int>{
return vec<int, 4>();
}

24 Май, 20:58 #31 #484143

>>484130
> А если допустим ты пишешь функции с этим вектором стандартным а потом понимаешь что нужно будет определить длину вектора в рантайме то ты такой типа списочек хуйнёшь?
Хитрость в том, что все эти `n` существуют только во время компиляции, во время выполнения это самый что ни на есть обычный список. Так что если тебе нужна длина вектора в рантайме, то придётся таки вычислить его длину, и потратить O(n) времени.
Правда если потом ты хочешь передать этот в функцию вроде `Vect 5 a -> ...`, то нужно, чтобы функция, вычисляющая длину, возвращала зависимую пару (n Vect n a). Тогда ты сможешь вручную проверить, что n действительно равно пяти, и если так, передать уже вектор в функцию.
С другой стороны, можно и доказывать, что данные обладают требуемым функцией свойствами. Список, к которому добавили элемент не может быть пустым, остаток от деления меньше делителя, моноидальная операция чего-либо с нейтральным элементом вернёт то самое «чего-либо» и так далее.
> вычитать их можно? а если 0 - 1
В принципе, вычитание могло бы требовать доказательства, что первое число не меньше второго, но в Idris сделали всё довольно топорно.

Ответы: >>484144

24 Май, 20:59 #32 #484144

>>484143
> (n ★★ Vect n a)
Макаба звёздочки съела.

24 Май, 21:02 #33 #484147

Я слышал, что в agde охуенно удобно строить edsl'и.
Хотелось бы увидеть пример такого на какой-нибудь приближенной к реальности задаче, а не факториалах.

Ответы: >>484166

24 Май, 21:12 #34 #484153

>>484130
У кого что, а у плюсоеба вечное "можнозделоть". Вы, ей-богу, хуже лисперов.

Ответы: >>484156

24 Май, 21:20 #35 #484156

>>484153
По-твоему лучше бы тред шёл в своём прежнем рейдж-русле? Все же началось с того что int в темпейте это совсем не то что нужно.

Но да сравнение забавное.

Ответы: >>484169

24 Май, 21:40 #36 #484166

>>484147
Idris больше направлен в сторону DSL. Но приближённый к реальной задаче пример доставить не могу.

Ответы: >>484172

24 Май, 21:46 #37 #484169

>>484156
Я не про содержание треда, просто интересно в очередной раз наблюдать типичное поведение крестовика/лиспера при обсуждении какой-то фичи: статическая типизация — ой, да можно на макросах сделать; сопоставление с образцом — да хуйня, за пару деньков на шаблонах/макросах можно накидать; зависимые типы — я в крестах могу такое сделать.
И иногда это "можнозделоть" даже выливается в полурабочую горстку костылей, отдаленно напоминающую предмет разговора. Но даже при всей очевидности их неприменимости на практике, фанатичная убежденность лишпера/крестоблядка во всемогуществе, всепременимости и безальтернативности его предмета обожания остается непробиваемой.

Ответы: >>486488

24 Май, 21:50 #38 #484172

>>484166
Что-то типа такого можешь показать? http://swizard.info/articles/solitaire/article.html

24 Май, 22:19 #39 #484184

>>483770
>можно доказать корректность реализации FizzBuzz'а
Приступай.

Ответы: >>484188

24 Май, 22:22 #40 #484188

>>484184
Кто-то и без меня уже начал: https://gist.github.com/david-christiansen/3660d5d45e9287c25a5e

Ответы: >>484192

24 Май, 22:28 #41 #484192

>>484188
Ну это чушь какая-то. Где доказательство того, что она корректную последовательность на экране напечатает? Его нет. Есть доказательство тривиальных фактов из арифметики.

Ответы: >>484193

24 Май, 22:31 #42 #484193

>>484192
> Где доказательство того, что она корректную последовательность на экране напечатает?
Для этого нужно как минимум переписать компилятор idris на idris и полностью покрыть доказательствами.

Ответы: >>484195

24 Май, 22:36 #43 #484195

>>484193
Дык. Не надо тогда нам лапшу на уши вешать. Физбаз он верифицировать может. Эта задача находится далеко за пределами возможностей таких систем.
А то доказательство про тупую реализацию остатка от деления можно было написать и на системах двадцатилетней давности. Собственно с тех пор ничего не изменилось. Толкут воду в ступе с умным видом.

Ответы: >>484394

sage 24 Май, 22:40 #44 #484196

>>484130
> кроме зависмости типа он ещё предоставляет некоторые проверки
Ну так запилят же вроде скоро. Алсо, D.

24 Май, 23:00 #45 #484207

Увы, подобные треды вредны для человечества. Они по факту являются необоснованным и ничем не подкреплённым разогревом интереса к профессии. Но вот беда: на практике это всё нахуй не нужно, а наличие зависимых типов на дваче никоим образом не делает программирование более интересной и интеллектуальной работой.

Ответы: >>484505

25 Май, 11:00 #46 #484394

>>484195
> Эта задача находится далеко за пределами возможностей таких систем.
А вот это тебе следует обосновать.

Ответы: >>484425

25 Май, 12:12 #47 #484425

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

Ответы: >>484434

2014 Кб, 2776x2464

25 Май, 12:43 #48 #484434

>>484425
> Понятие печати текста в консоль нигде не формализовано.
Можно эмулировать оборудование вроде пикрелейта и на самом деле юникс-подобные ОС это и делают, у него спецификации должны быть.
а вообще, просто предполагается, что среда, в которой запускается программа, идеальна, проверяется, что программа корректно взаимодействует со средой, и на этом, вообще говоря, задача верификации завершена

25 Май, 14:00 #49 #484460

>>483873
Тред не читал, сразу отвечал. Не слушай петухов, в крестах есть зависимые типы, полиморфные (или шаблонные, как принято называть их в крестах) функции - один из примеров. Другое дело, что в С++ типы могут зависеть только от других типов (или констант времени компиляции, которые по сути эквивалентны типам), а в языках с полноценной поддержкой - от любого выражения. И да, не от значения а от выражения, это важно, потому что рантайм-значение на момент компиляции не известно.

Ответы: >>484473, >>484528

25 Май, 14:27 #50 #484473

>>484460
В чем принципиальная разница между выражением и типом?

Ответы: >>484534

25 Май, 14:56 #51 #484486

>но и доказывать корректность их реализации
Ну докажи мне корректность гостевухи или цмски, например.

25 Май, 15:30 #52 #484505

>>484207
Лисп, хаскель, алгоритмы, олимпиадки, архитектурка - это всё этакое самопорождённое и самоподдерживающееся ассоциативное чёрное SMM от быдлокодинга.
Вот вам красивый аналог попроще: http://vk.com/anime_onlineparty
Хаскешиз? Гоу нырять в энтерпрайз-парашу на скале, ведь у нас есть scalaz, а теперь и cats!
Схемофаз? Гоу пилить круды на рельсах, ведь в раби есть callcc и вообще дух метапетушения выдержан!

Ответы: >>484515

25 Май, 15:43 #53 #484515

>>484505
Нашел таки тусовку?

25 Май, 15:58 #54 #484528

>>484460
> Другое дело, что в С++ типы могут зависеть только от других типов
Это называется параметрическим полиморфизмом. Хотя он формально и относится к некоторому подмножеству зависимых типов, к языкам с зависимыми типами относят именно те, что позволяют зависеть от выражения.

Ответы: >>484534

25 Май, 16:13 #55 #484534

>>484473
>В чем принципиальная разница между выражением и типом?
Ты, наверное, хотел спросить в чем принципиальная разница между языками, в которых типы как-то ограничены, и теми, в которых тип может быть представлен произвольным выражением. В сложности алгоритма проверки типов главным образом (и как следствие - в геморе использования такого языка). Если типы - простые значения, их можно просто сравнивать, например Int не равен String. Если там выражения, то их надо как-то унифицировать, чтобы понять эквивалентны они или нет, в некоторых случаях это вообще неразрешимая задача.
>>484528
Что значит "зависеть от выражения"? Тащем-то тип полиморфной функции зависит от типов аргументов.

Ответы: >>484540, >>486420

25 Май, 16:37 #56 #484540

>>484534
> Тащем-то тип полиморфной функции зависит от типов аргументов
Да, только вот в большинстве языков тип не может быть представлен произвольным выражением, пусть даже гарантируемо вычислимым.

sage 25 Май, 16:59 #57 #484553

Сьебите в /sci/, больные ублюдки.

26 Май, 14:52 #58 #485092

Бамп.

26 Май, 16:14 #59 #485133

>>483770
А в скале такое можно сделать?

Ответы: >>485164

26 Май, 16:55 #60 #485164

>>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'е всё это проще и естественнее.

26 Май, 18:27 #61 #485206

50 постов, а я так и не понял. Зачем мне доказывать корректность моих программ?

Ответы: >>485214

26 Май, 18:54 #62 #485214

>>485206
Ну например, чтобы избежать http://www.envisage-project.eu/proving-android-java-and-python-sorting-algorithm-is-broken-and-how-to-fix-it/

28 Май, 09:10 #63 #486383

Бамп.

28 Май, 10:09 #64 #486408

Я так и не понял зачем все это петушение нужно.
Кто-нибудь покажите рабочий production код, где эти ваши типы реально используются, и для сравнения тот же код без их использования.

28 Май, 10:34 #65 #486420

>>484534
Все равно не очень понял. Вернемся к тому примеру с массивом, там было выражение n. Первый крестобог попытался это выразить в виде template<int n, class a>, что неверно. Но можно же сделать, скажем, template<class Expression, class a> где в качестве Expression можно задавать, например, Variable<"N"> или Plus<Variable<"N">, Constant<1>>. Т.е. сделать на шаблонах систему выражений. Чем это будет отличаться тогда от настоящих зависимых типов?

Ответы: >>486488, >>486503

28 Май, 13:24 #66 #486488

>>486420
>Первый крестобог попытался это выразить в виде template<int n, class a>, что неверно
>Но можно же сделать
>МОЖНОЗДЕЛОТЬ
-> >>484169

28 Май, 13:44 #67 #486503

>>486420
>сделать на шаблонах систему выражений.
Попробуй, лол. Не забывай, что тебе по этим выражениям ещё корректность доказывать. И всё это писать на ебанутом языке шаблонов.
>Чем это будет отличаться тогда от настоящих зависимых типов?
Тем, что это будет кривая и неюзабельная хуита, головной и жопной боли от которой в разы больше, чем пользы
>Plus<Variable<"N">, Constant<1>>
хотя плюсоёбам не привыкать.
Алсо, страшно представить, какими простынями будет плеваться компилятор при ошибках.

Ответы: >>486620

28 Май, 17:07 #68 #486620

>>486503
>Попробуй, лол.
Что там пробовать? Ты сомневаешься, что можно нафигачить шаблонных классов для всех действий и т.д.?
>Не забывай, что тебе по этим выражениям ещё корректность доказывать.
Вот тут бы поподробнее. Какие именно манипуляции в твоих языках возможны? Как их применять?
На шаблонах можно много чего сделать.

>Тем, что это будет кривая и неюзабельная хуита, головной и жопной боли от которой в разы больше, чем пользы
Слабовато. У тебя есть два пути.
1)
>Вот вам язык. Его основная фича - сахарок для одной эзотерической операции. Эту операцию вообще-то можно реализовать и стандартными средствами крестов, но этого никто не делает, потому что это никому не нужно.
Ясно.

2)
>Вот вам язык. Его основная фича, Х, позволяет делать У, что невозможно на других языках. Вот простой абстрактный пример: ... А вот пример того, как этим можно воспользоваться в реальном проекте: ... На других языках полный аналог этих примеров написать нельзя.
Вот теперь тебя люблю я!

Пока что я вижу скорее 1).

Ответы: >>486686, >>487901

28 Май, 17:45 #69 #486640

Хули ДРИСНЯ ебаная модули нихуя не загружает
ШINDOШS
Кто-нибудь сталкивался?

Ответы: >>486642, >>486693

147 Кб, 1263x776

28 Май, 17:50 #70 #486642

>>486640 пик вдогонку

Ответы: >>486649, >>486696

224 Кб, 552x830

28 Май, 17:59 #71 #486649

>>486642
Спермопроблемы.

28 Май, 19:28 #72 #486686

>>486620
>Ты сомневаешься, что можно нафигачить шаблонных классов для всех действий и т.д.?
>можно нафигачить
>На шаблонах можно много чего сделать.
Можносделать зашкаливает! Ну и нафигачь, давай. Но мы-то знаем, что ничего, что можно было бы назвать зависимыми типами, у тебя не получится.

>>Тем, что это будет кривая и неюзабельная хуита, головной и жопной боли от которой в разы больше, чем пользы
>Слабовато. У тебя есть два пути.
Слабовато. У тебя есть один путь: можносделать, но никто не делает и не будет делать из-за, ВНЕЗАПНО, уёбищности крестов, усложняющих и без того сложную задачу, из-за уёбищности результата, который в и без того уёбищных крестах никто в здравом уме использовать не будет.

Ответы: >>486695

28 Май, 19:52 #73 #486693

>>486640
Contrib-то подгрузи. `idris -p contrib`

Ответы: >>486736

28 Май, 19:53 #74 #486695

>>486686
Ясно.

Ответы: >>486760

sage 28 Май, 19:55 #75 #486696

>>486642
> запускает юзер-левел приложения от админа

Ответы: >>486736

28 Май, 20:28 #76 #486736

>>486693
Спасибо, братишка.

>>486696
> set username
> USERNAME=user
ну хуй знает

Я правильно понимаю, что они решили переименовать refl в Refl?

Ответы: >>486776, >>486792

140 Кб, 1263x776

28 Май, 20:39 #77 #486746

Почему rewrite не срабатывает?
И еще интереснее, почему нет никаких сообщений по этому поводу?

Ответы: >>487942

1 Кб, 330x19

28 Май, 20:49 #78 #486754

И еще. WTF? Зависимые типы ебут мое корыто, даже во время простоя (просто запущен repl, никаких операций не выполняется). Очень хотелось бы их угомонить.

Ответы: >>487942

28 Май, 20:52 #79 #486760

>>486695
Сколько ошибок в слове "неприятно".

Ответы: >>486790

28 Май, 21:00 #80 #486776

>>486736
> Я правильно понимаю, что они решили переименовать refl в Refl?
Да, переименовали (что вполне естественно, так как типы и конструкторы везде с большой буквы).

sage 28 Май, 21:07 #81 #486790

>>486760
Да ты целых пять слов написал вместо нужного.

Ответы: >>486797

28 Май, 21:09 #82 #486792

>>486736
Хм, смутила надпись (Admin) в заголовке и значок UAC в табе.

28 Май, 21:12 #83 #486797

>>486790
А ты вообще восемь.

Ответы: >>486801

sage 28 Май, 21:14 #84 #486801

>>486797
> ты дурак
> нет, ты дурак!
> нет, ты!
> маам, ну скажи ему!

Ответы: >>486811

28 Май, 21:19 #85 #486811

>>486801
Чего, сынуля? Снова тебя обижают?
мимо-мама

29 Май, 11:31 #86 #487168

Бамп.

29 Май, 12:05 #87 #487189

Я понял!!! Андрюше нужно писать на PHP! Ведь как учит языки нормальный человек: лисп (аморфная красота) -> хаскель (строгая красота) -> агда (математически строгая красота). А история Андрюши очень трагичная, братюни. Сначала все начиналось хорошо: общелисп -> хаскель -> скала + агда. Помню даже писал Андрюша пасты про то, что хотел бы соседа лиспера на дачу, потому что лисперы слишком практичные.
Но потом что-то пошло не так: -> хаскель -> кресты -> джаваскрипт -> питон.
И я все ломал голову, как человек может так ненавидеть красивое и сложное, так хотеть деградации, что пишет на питоне? Но для Андрюши практичное уродство и есть красота. А дальше PHP, Verilog, соцреализм, диктатура пролетариата и экономическое чудо по китайскому образцу. Скай из зе лимит!

Ответы: >>487201, >>487822

sage 29 Май, 12:20 #88 #487201

>>487189
>Андрюше нужно писать на PHP
cпс разъяснил

мимо-андрюша

30 Май, 01:02 #89 #487807

на ваших зависимых типах можно зделать так:

data Img = Img {
width :: Nat,
height :: Nat,
pixels :: Vec (width * height) Pixel
}

чтоб width и height не были известны на этапе компиляции?

Ответы: >>487816

sage 30 Май, 02:09 #90 #487816

>>487807
да

30 Май, 05:04 #91 #487821

1

30 Май, 05:04 #92 #487822

>>487189
Всё хорошо до тех пор, пока игнорируешь цели программирования. Как только включаешь ЦЕЛЕСООБРАЗНОСТЬ, так сразу вдруг обнаруживаются удивительные вещи: что на ноджс и петоне все программы пишутся в 100 раз быстрее, работают производительнее, код гораздо чище, проще, и поддерживаемее, библиотеки для всего уже написаны, и так далее.
> уродство и есть красота
Нет, суть не в том, что это красиво, а в том, что попытки искать в программировании красоту - глупые и обречены на провал. Сколько такой хуйнёй не страдай, тебе потом ноджсник или питонщик за вечер по губам проведёт, решив ту же задачу гораздо проще и компактнее. И твоя красота сливается по полной, потому что сил в неё вбухано намного больше, а для других программистов она сложнее и трудноподдерживаемее. Не все настолько изощрены в искусстве отрицания и самообмана, чтобы упорно продолжать в том же духе даже после многочисленных подобных отсосов.
Любителям красоты могу только посочувствовать и посоветовать перекат в области, где искусство ради искусства, где композиция выразительных элементов - сама цель деятельности, а критерии её качества - "красиво", "интересно", "прикольно", и так далее. Причём не обязательно в качестве производителя. Можно просто быть потребителем и соревноваться в элитности вкусов, наслушанности, начинатанности, количестве просмотренных тайтлов, глубоком анализе деталей такой-то серии такой-то анимы, открывающем абсолютно альтернативную трактовку сюжета, умении видеть 100500 отсылок к творчеству других писателей или мифологии, вкладывать в семиотические структуры такое содержание, которое даже автор открытого текста не мог себе представить, знании поджанров, музыкальной теории, умении сдетектировать ритм, инструменты, эффекты, классифицировать трек как комбинацию таких-то поджанровых тегов и накатать техничную рецензию в духе allmusic и так далее. Искусство и существует ради красоты, глубины, интересности, а вот программирование - оно не для этого. Программирование существует ради того, чтобы решать скучные бытовые инфраструктурные проблемки, являющиеся препятствием на пути к развлечениям и искусству. И чем проще и быстрее это делать, тем больше времени и сил будет оставаться на то, ради чего, собственно, всё и затевалось.

Ответы: >>487833, >>487841, >>487851, >>487925

30 Май, 07:02 #93 #487833

>>487822
>эти фантазии
>эти оправдания
>эти оправдания
>эти оправдания
Чет вголосяндру.

Ответы: >>487837

30 Май, 08:12 #94 #487837

>>487833
Фантазии или так и есть - на самом деле не принципиально. Важно, какие ценности в программировании неуместны, и следующий из этого вывод, что программирование не стоит того, чтобы им вообще так заморачиваться. Можно не программировать - лучше не программировать. Если есть способ решить задачу или заработать деньги проще - лучше так и сделать.

Ответы: >>487838

30 Май, 08:17 #95 #487838

>>487837
>это оправдывающееся быдло
As expected.

30 Май, 08:20 #96 #487841

>>487822
Так за эту хуйню денег никто не платит.

Ответы: >>487842

30 Май, 08:34 #97 #487842

>>487841
Можно зарабатывать кодингом, а увлекаться чем-то другим, как большинство и делает, но это слишком напряжно и лучше пробовать другие варианты:
- work smarter not harder, всякие экзотические разовые аналитические проекты и консалтинг
- работа, где большую часть рабочего времени можешь заниматься своими делами, типа сисадминства, эникейства, охранников
- фриланс и ситуационные подработки когда нужна лавешка - здесь может быть и быдлокодинг, и консалтинг, и естественноязыковые переводы, и дофига чего
и так далее

30 Май, 09:47 #98 #487851

>>487822
Ты, Андрюш, просто сдался.
А сдался ты потому, что слаб.

Ответы: >>487853, >>487854

30 Май, 09:48 #99 #487853

>>487851
Зато я ебал твою мамашу.

30 Май, 09:58 #100 #487854

>>487851
Просто все тут конченые шизики, но некоторые начинают что-то подозревать. И кому посчастливилось забраться достаточно высоко на мета-уровень, тот видит, что на той стороне реки люди сходят с ума гораздо веселее. Совсем не быть ёбнутым аутистом здесь у кого-то получится вряд ли, но существенно улучшить качество своей жизни, оказывается, несложно.

Ответы: >>487873

30 Май, 11:07 #101 #487873

>>487854
>этот проецирующий шизофреник
Ну что же ты, Андрюша.
Как был дурачком - так и остался.

30 Май, 11:58 #102 #487897

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

Ответы: >>487916

30 Май, 12:07 #103 #487901

>>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>

Ответы: >>487911, >>487926, >>487930, >>488021, >>489411

30 Май, 12:34 #104 #487911

>>487901
Макаба разметку съела. Ты имел в виду
> Должно компилироваться: a ∗∗ a, b ∗∗ b, cat(a, b) ∗∗ cat(b, a)
?

Ответы: >>487917

30 Май, 12:42 #105 #487916

>>487897
> в первую очередь эти языки исследовательские
Да, только вот у idris это исследование на тему практического применения зависимых типов в программировании. Поэтому, к примеру, в языке есть классы типов.

Ответы: >>487922

30 Май, 12:43 #106 #487917

>>487911
Так точно. Никак не привыкну к разметке.

Ответы: >>487927

30 Май, 12:48 #107 #487922

>>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]

30 Май, 12:59 #108 #487925

>>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

Ответы: >>487928

30 Май, 13:03 #109 #487926

>>487901
на Хаскеле такое делается?

Ответы: >>487928

30 Май, 13:03 #110 #487927

>>487917
Думаю, поэлементное умножение векторов будет даже нагляднее.

30 Май, 13:05 #111 #487928

>>487925
> darcs - VCS на Haskell
Лучше бы ты о darcs не вспоминал.

>>487926
Нет.

30 Май, 13:10 #112 #487930

>>487901
>Эквивалентную идрисню подгоню, если надо.
Подгони плз. Попробую сделать на крестах.
3е будет не простым if, конечно, а шаблонной магией.

Ответы: >>487997

30 Май, 13:40 #113 #487942

>>486746
Если вдруг кому интересны мои приключения, я нашел вроде бы релевантный тред
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 ) и лучше с петухом побалуюсь.

Ответы: >>487945

30 Май, 13:47 #114 #487945

>>487942
> [email-masked]
И ни одного issue на гитхабе (хотя, может плохо искал?). Может, стоит создать один?

сам думал поиграться с доказательством сортировки слиянием, но для этого надо ждать https://github.com/idris-lang/Idris-dev/pull/2205

30 Май, 15:09 #115 #487997

>>487930
http://pastebin.com/XGfF9PYW комментировать было лень, но если что, спрашивай. Вектор в стандартной библиотеке есть, решил завелосипедить для наглядности; Nat не стал. Идея такая, что в общем случае компилятор нихрена не знает, что длины равны, но мы можем ему это доказать – статически, при помощи теорем (например, о коммутативности сложения), или динамически, при помощи вычислимого равенства (DecEq).

Ответы: >>488002, >>488036, >>488143

30 Май, 15:26 #116 #488002

>>487997
Замени `print` на `printLn`, чтобы вывод читать можно было.

30 Май, 16:21 #117 #488021

>>487901
http://dpaste.dzfl.pl/c6859709dc9d

Альфа-версия шаблоно-дрисни, всё чек кроме 3e, 3е так просто не получится, надо вводить какой-то контекст ограничений на n и m. Ну и доказательство теорем надо накодить нормальное, а не ололо-перебором, но это имхо можнозделоть.

> Bin!(Bin!(Sym!"n", "+", Sym!"m"), "", Sym!"k")
МОЖНОЗДЕЛОТЬ нормальный разбор строки выражения (n + m) k тоже.

Потратил часа 3, но я тупой и на D мало кодил.

Интересно, как будет выглядеть подобная хуита на крестах.

Ответы: >>488022, >>488062

30 Май, 16:27 #118 #488022

>>488021
> 3е так просто не получится, надо вводить какой-то контекст ограничений на n и m. Ну и доказательство теорем надо накодить нормальное, а не ололо-перебором, но это имхо можнозделоть.
Можнозделоть реализацию Idris на шаблонах. Наверное можно.

Ответы: >>488023, >>488054

30 Май, 16:28 #119 #488023

>>488022
Я лично уверен, что всё можно. Не будет так удобно, но можно, хоть обкукарекайтесь что нельзя. За 3 часа нахуячил рабочий proof-of-concept, сколько твой Idris пилят?

30 Май, 16:35 #120 #488025

Жду короч похожую крестодрисню от крестобога. После этого обсуждение того, что на шаблонах что-то ненужное НИЛЬЗЯЗДЕЛОТЬ можно считать закрытым.

Ответы: >>488066

30 Май, 16:59 #121 #488031

Игрушечный язык с зависимыми типами не так уж трудно запилить, кстати:
https://github.com/sweirich/pi-forall/
https://github.com/david-christiansen/tiny-dependent-types

Ответы: >>488040

30 Май, 17:19 #122 #488036

>>487997
У тебя там связанный список? Массивов не завезли?
Знак доллара что обозначает?

Ответы: >>488042

30 Май, 17:27 #123 #488040

>>488031
Смотрел лекции pi-forall и не сказал бы что прям охуеть как просто.
+ там только тайпчекер
+ там несколько версий и есть баги

30 Май, 17:28 #124 #488042

>>488036
> Массивов не завезли?
Если завозить, то лучше сразу вот такие: http://www.cs.ru.nl/dtp11/slides/trojahner.pdf
> Знак доллара что обозначает?
То же, что и в хаскеле — аппликацию.

Ответы: >>488045

30 Май, 17:39 #125 #488045

>>488042
Как запустить эту программу?

Ответы: >>488050

30 Май, 17:41 #126 #488050

>>488045
`idris --execute foo.idr`

30 Май, 17:43 #127 #488054

>>488022
Можно хоть на брэйнфаке, только не нужно

30 Май, 17:48 #128 #488062

>>488021
Чет на том сайте не работает, что бы я ни вводил в инпут, пишет:
Application error:

std.conv.ConvException@/opt/compilers/dmd2/include/std/conv.d(1684): Unexpected '
' when converting from type string to type uint

Ответы: >>488118

30 Май, 17:58 #129 #488066

>>488025
Зделоть-то на любой полной по Тьюрингу параше можно, а вот сделать пригодным для использования в пределах крестах, не переизобретая поверх них нового языка, никак не выйдет.

Ответы: >>488119

30 Май, 19:52 #130 #488118

>>488062
>что бы я ни вводил в инпут
Я мудак, извини D тоже, какого хуя надо .strip()?. Починил.
http://dpaste.dzfl.pl/cea917021136

30 Май, 19:55 #131 #488119

>>488066
> не переизобретая поверх них нового языка
Ну да, кто спорит-то.

Алсо, я тут думал над if(n == m) и более сложными конструкциями, у вас там компилятор прошаривает все такие ограничения в процессе прохода по коду же, и зависимые типы начинают зависеть от них тоже, так? Вот такое хрен сделаешь нормально.

30 Май, 20:44 #132 #488143

>>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], и их скалярное произведение равно нулю. Сдулась твоя верификация?

Ответы: >>488188, >>488190

30 Кб, 1100x668

30 Май, 21:13 #133 #488158

Вот, наслаждайтесь: https://gist.github.com/sorrge/2d2271e57ad1e91a50ea
Чистейшие кресты, возможностей еще побольше, чем в Идрисе в некоторых местах, к тому же без багов.
Жду исправленного кода на Идрисе. Если такового не будет, то будем считать, что зависимые типы в крестах круче.

Ответы: >>488165, >>488725

30 Май, 21:43 #134 #488165

>>488158
давай типы зависимые от строк накодь

Ответы: >>488167

30 Май, 21:49 #135 #488167

>>488165
Замени int на string в строке 12.

Ответы: >>488171

30 Май, 22:09 #136 #488171

>>488167
ну ок))

30 Май, 23:24 #137 #488188

>>488143
Но там никто и не утверждает, что (a .++ b) .∗ (b .++ a) = (a .++ b) .∗ (a .++ b). Единственное требование, которое есть у .∗ — одинаковые длины у векторов. И действительно, (a .++ b) и (b .++ a) имеют одинаковую длину (что следует из из определения .∗ и коммутативности сложения).

Ответы: >>488189, >>488191

30 Май, 23:26 #138 #488189

>>488188
> из определения .++
ffix

30 Май, 23:28 #139 #488190

>>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)

Ответы: >>488192

30 Май, 23:32 #140 #488191

>>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 заменит? А че там, и то число, и это число. Какая разница-то, итить?

Ответы: >>488193

30 Май, 23:34 #141 #488192

>>488190
Вот это уже похоже на правду. Протестирую сейчас.

30 Май, 23:36 #142 #488193

>>488191
Но rewrite не заменяет b .++ a на a .++ b. Он заменяет совсем другое: `m + n` на `n + m` в типе Vec (m + n) _.

Ответы: >>488197

30 Май, 23:42 #143 #488197

>>488193
Да, теперь понятно уже, что конкатенация была забагована. Еще один камень в огород идриса: что же там легко накосячить в элементарной операции
?

А вот такое все равно не работает:
(a .++ b .++ a .++ a .++ b) .∗ (rewrite plusCommutative n m in (b .++ a .++ a .++ a .++ b))
В крестах работает. Для доказательства этого нужна только коммутативность.

Ответы: >>488205, >>488236

30 Май, 23:56 #144 #488205

>>488197
> что же там легко накосячить в элементарной операции
Я, вообще говоря, удивился, увидев то определение. Но подумал, что всё равно мы проверяем не это.
> (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` для этого недостаточно.
> В крестах работает. Для доказательства этого нужна только коммутативность.
Небольшой такой вопрос: а как именно кресты выводят доказательство, полагаясь на одну только коммутативность? Это, конечно, можно доказать, но не за один шаг.

Ответы: >>488207, >>488211

30 Май, 23:59 #145 #488207

>>488205
...и используя не только коммутативность. Без ассоциативности это доказать нельзя.

Ответы: >>488212

31 Май, 00:02 #146 #488211

>>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.

31 Май, 00:03 #147 #488212

>>488207
Можно. Ты скобки не так расставил.

Ответы: >>488223

31 Май, 00:31 #148 #488223

>>488212
> Ты скобки не так расставил.
Лол. С левой ассоциативностью легко, а вот с правой уже не так просто.

Ответы: >>488227

31 Май, 00:40 #149 #488227

>>488223
В крестах можно добавить правила для проверки ассоциативности. Это будет полным перебором делаться, конечно, что может привести к долгой компиляции длинных выражений. Но сам алгоритм тривиален: пробуй и так, и сяк.
Можно сделать и ручной режим, как в идрисе. Там писанины побольше будет.

Ответы: >>488241

31 Май, 00:59 #150 #488236

>>488197
Idris невиноват в том, что конкатенация неверная, виноват только человек, который ее написал. Idris же не знает, какая конкатенация правильная, а какая нет, для этого нужно формулировать свойства, которые выносятся в типы (или пишутся отдельной функцией), а уже потом доказывается корректность конкатенации.

>А вот такое все равно не работает:
А оно и не должно. Это же не просто арифметические выражения, это термы. Поэтому уже нужна другая лемма, здесь все строго.

Ответы: >>488241, >>488242, >>488330

31 Май, 01:03 #151 #488241

>>488227
> Но сам алгоритм тривиален: пробуй и так, и сяк.
Для ad-hoc вещей вроде сложения такой способ пригоден. В общем случае уже нет.

>>488236
При левой ассоциативности, `rewrite plusCommutative m n` могло бы сработать. Однако, ассоциативность у `.++` правая.

Ответы: >>488243

31 Май, 01:10 #152 #488242

>>488236
Ясно, что не он не знает. Проблема в том, что запись определения этой функции стала настолько неудобочитаемой, что фактически непонятно (человеку), что она делает. Отсюда и ошибка.

>Поэтому уже нужна другая лемма, здесь все строго.
Это плохое оправдание. На крестах вон тоже все строго. Какой это вывод типов, если ему каждое действие нужно прописать? Без автоматизации таких простых цепочек там на каждый чих придется простыни доказательств писать.
Но если там скобки по-другому расставлены, то тогда понятно - там ассоциативность нужна.

Ответы: >>488247

31 Май, 01:12 #153 #488243

>>488241
>Для ad-hoc вещей вроде сложения такой способ пригоден. В общем случае уже нет.
И какое решение этой проблемы предложено в идрисе?

Ответы: >>488251

31 Май, 01:21 #154 #488247

>>488242
Эм. Я совсем не знаю как работает система шаблонов в C++, но в Idris (и в любых языках с зависимыми типами) вывод типов undecidable, не считая контекстов, когда это просто типизированная лямбда.

И да, каждое действие надо прописывать. В этом и проблема, что в данный момент доказательства писать муторно и долго и что нужно переходить к их умной генерации (ну или к тактикам вот переходят).

Ответы: >>488251, >>488326

31 Май, 01:29 #155 #488251

>>488243
Так как сколь-либо общего решения этой проблемы не существует (печально, но факт), остаётся лишь попытаться облегчить сам процесс доказательства. Для этого в Idris есть: разделение кода и доказательств (provisional definitions), тактики, довольно мощное сопоставление с образцом и немного переписывания термов. И само-собой, как всегда, помогает абстракция и готовые библиотеки.

>>488247
> ну или к тактикам вот переходят
С тактиками у Idris пока небогато. Ехал rewrite через rewrite.

Ответы: >>488326

31 Май, 13:11 #156 #488326

>>488251
>>488247
Ну а все-таки, автоматизировать применение правил в идрисе можно? Например, сказать, чтобы коммутативность проверялась всегда, когда в типе используется сложение, а не только по запросу?

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

Ответы: >>488373, >>488725

31 Май, 13:15 #157 #488330

>>488236
>для этого нужно формулировать свойства
Предлагаю сделать это следующим туром нашей специальной зависимотиповой олимпиады. Для конкатенации написать три леммы: про левую и правую единицу и про ассоциативность. Короче, что вектор, пустой вектор и cat образуют моноид.

Ответы: >>488725

31 Май, 14:20 #158 #488373

>>488326
> Ну а все-таки, автоматизировать применение правил в идрисе можно?
Есть неявные аргументы и неявные преобразования. Магии они не делают, впрочем.

31 Май, 22:36 #159 #488718

http://www.linux.org.ru/forum/development/4299185 всё уже обсудили до нас

Ответы: >>488801

31 Май, 22:43 #160 #488725

>>488158
Как это компилировать? На любые попытки выдает ошибки в шаблонах.

>>488326
Я не понимаю почему всем так хочется доказать, что в С++ или D можно сделать то, чего в Idris нельзя.

>Кресты предоставляют больше возможностей
Ну так получается что вы пишите какие-то куски кода, которые по сути и есть Idris, то есть пишите сами себе прувер на шаблонах, однако важно, чтобы он был согласованным и не позволял строить фальшивые доказательства (undecidable), а бил по рукам. Шаблоны уже по умолчанию undecidable из-за полноты.

>>488330
Неплохое упражнение на самом деле.

Ответы: >>488740, >>488801

31 Май, 22:54 #161 #488740

>>488725
> Неплохое упражнение на самом деле.
Да, только чёт у меня Idris спотыкается на ровном месте.

Ответы: >>488778

31 Май, 23:20 #162 #488778

>>488740
А вот, собственно, где он спотыкается: http://lpaste.net/1334041297681383424
Причина проста: тупой `rewrite` туп. В мейллисте есть тред https://groups.google.com/forum/#!msg/idris-lang/iNNYoE0k27A/AhiVU_LBFBcJ, где предлагаются костыли-костылики для решения этой проблемы. И ьне как-то лень возиться с этими костылями.
Плохо зделали, тупо, короч.

Ответы: >>488794

31 Май, 23:33 #163 #488794

>>488778
Ну можно и без rewrite (Equational Reasoning), как сделано в стандартной библиотеке: https://github.com/idris-lang/Idris-dev/blob/master/libs/base/Data/VectType.idr#L554

А то что некоторые вещи сделаны плохо или их совсем нет, то это вполне понятно почему.

Ответы: >>488803

31 Май, 23:42 #164 #488801

>>488718
Это ерунда без выражений и операций.
>>488725
>На любые попытки выдает ошибки в шаблонах.
Я только в студии компилировал, под другие надо править ошибки.
>что вы пишите какие-то куски кода, которые по сути и есть Idris
Вопрос был в том, изобрели ли зависимые типы в этих языках, или они есть и в крестах. Ответ: нет, не изобрели, на крестах можно делать то же самое. Для сравнения попробуй на С99 сделать ту задачу с вектором. Вот этот язык не поддерживает зависимые типы.

Ответы: >>488837

31 Май, 23:44 #165 #488803

>>488794
Можно. Просто весьма сбивает с толку, когда то, что должно работать, не работает.

01 Июн, 00:09 #166 #488832

Вопрос к языковедам. Есть ли такой язык, который был бы во всем, как обычный С, со всеми его маллоками, указателями и т.д., но с современной системой типов, с автоматическим выводом типов и тому подобным?
Можно же такое зделоть. Компилировать в тот же С, но после всех проверок, с генерацией кода для разных случаев. Есть же до сих пор любители писать на С, по разным причинам. Из-за скорости, простоты, совместимости с другим кодом. Может быть, им такое понравилось бы.

Ответы: >>488837, >>488838, >>488842

01 Июн, 00:14 #167 #488837

>>488801
Да, не изобрели, потому что эти языки опираются на теорию типов 80х, которая была построена на идеях 40-50х годов.

То что в C++ можно делать какие-то вещи как в Idris или Agda, не говорит, что там зависимые типы (в рамках этой простой задачи возможно да, я не читал код на шаблонах). Например в C++ нет супертипа, а это значит, что вот такое написать нельзя:

hey : Int -> Type
hey 5 = Int
hey _ = Float

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

>>488832
Если не нужны зависимые типы, то наверное Rust, а если нужны, то http://www.ats-lang.org/

Про генерацию кода для разных случаев - это уже суперкомпиляция какая-то.

Ответы: >>488840, >>488891, >>488894

01 Июн, 00:14 #168 #488838

>>488832
> Компилировать в тот же С, но после всех проверок, с генерацией кода для разных случаев.
О чем ты вообще? Цпп и д компилируются в такой же байткод как и ц, с такой же скоростью и совместимостью. Пиши на цпп в стиле ц и добавь кодогенерации шаблонами - ничто не пострадает. Ним так вообще в исходник на ц компилится.

01 Июн, 00:15 #169 #488840

>>488837
>Про генерацию кода для разных случаев - это уже суперкомпиляция какая-то.
Это обычное метапрограммирование, которое есть во всех нормальных языках.

Ответы: >>488843

01 Июн, 00:16 #170 #488842

>>488832
Зачем писать как на С, если есть полноценная система типов? А так-то был Cyclone, есть Rust, а если хочется зависимых типов — ATS.

Ответы: >>488894

01 Июн, 00:17 #171 #488843

>>488840
Ну так он спрашивает про то, чтобы компилятор сам генерировал разный код для разных случаев, а не чтобы самому описывать эти самые случаи.

Ответы: >>488854

01 Июн, 00:24 #172 #488854

>>488843
> компилятор сам генерировал разный код для разных случаев
Комплюктер САМ ничего не делает, на дворе всё-таки 2015 год.

01 Июн, 00:51 #173 #488891

>>488837
>Например в 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?

Ответы: >>488931, >>488978

01 Июн, 00:52 #174 #488894

>>488842
>>488837
Да, Rust, пожалуй, это то, о чем я говорил. Спасибо.

01 Июн, 01:10 #175 #488924

Вот вам пример реального использования типов-выражений в крестах: http://eigen.tuxfamily.org/dox/classEigen_1_1GeneralProduct.html
Там это используется для оптимизации действий с матрицами, исключения ненужного копирования промежуточных результатов вычислений в длинных выражениях.

01 Июн, 01:18 #176 #488931

>>488891
> Но параметер функции должен быть константой времени компиляции.
Вот, ты сам всё сказал.
То есть, никто не спорит, в C++ можно сварганить подмножество зависимых типов. Как и на скалке, и на хачкеле. Но не всё.
> Срастили типы и термы? Как именно это помогает при верификации свойств?
См. изоморфизм Карри-Говарда.
> Как доказать, что не будет деления на ноль?
Сделать, чтобы remove_zeros возвращала зависимую пару из вектора и доказательства, что все элементы не нули.

Ответы: >>488941

01 Июн, 01:40 #177 #488941

>>488931
Ну и что, что изоморфизм? Можно доказательства на типах делать? А зачем? Их прекрасно можно делать и без типов. Как это помогает в чем-либо?
Мне это напоминает риторику лиспоидов: смотрите, программа и данные это одно и то же. Ясно.

remove_zeros, допустим, вернет такую пару, хотя это уже притянуто за уши - с чего бы ей морочиться таким частным свойством. Ну допустим. А потом я прицеплю 5 к этому списку, и доказательство протухнет. У тебя весь код должен это доказательство возвращать? А если мне не нули интересны, а простые числа? Строки из трех букв? Может, мне важно, является ли список палиндромом?
Очевидно, что ты не сможешь все доказательства записать в код заранее. Всё равно придется все верифицировать вручную для каждого случая. Какой тогда смысл замусоривать код до нечитаемости?

Ответы: >>488949, >>488978

01 Июн, 01:53 #178 #488949

>>488941
> Можно доказательства на типах делать? А зачем? Их прекрасно можно делать и без типов.
Делать-то, конечно, можно, а вот с проверкой — беда. Вот, возьми это: http://research.microsoft.com/en-us/um/people/gonthier/4colproof.pdf

Ответы: >>488950

01 Июн, 02:02 #179 #488950

>>488949
По-моему ты совершенно не понимаешь, о чем я говорю. К чему ты это привел?

01 Июн, 06:58 #180 #488978

>>488891
Мне кажется ты как-то сильно привязался к Idris и хочешь для себя решить, что он на самом деле и не нужен совсем.

Еще раз: Idris - просто очередная реализация языка с зависимыми типами (немного отличаается от Agda), ну просто решили они попробовать сделать язык с практическим уклоном (на самом деле нового там - другой подход к работе с грязными функциями: библиотека Effects).

>Как именно это помогает при верификации свойств?
Только это и позволяет выражать и доказывать эти самые свойста. Это не просто какой-то язык как C++ или Python. Это язык - типизированная лямбда исчисление (посложнее), в котором некоторые вещи оказались похожи на логику предикатов (Карри-Говард).

>Можно доказательства на типах делать? А зачем?

Эм, чтобы проверять доказательства на компьютере.

>Как это помогает в чем-либо?
Здесь все конечно смотрят со стороны индустрии и кодеров, однако забыли математиков, которым вообще говоря возможность выражать теоремы конструктивной математики и проверять на компьютере их не помешает.

Есть мнение, что лет через 20 или 50 вся математика и будет проверяться в разных пруверах.

>>488941

>Всё равно придется все верифицировать вручную для каждого случая. Какой тогда смысл замусоривать код до нечитаемости?
Для обычных программистов сейчас это оверхеад и вообще много возни. Но это сейчас, Idris - первый язык с практическим уклоном. Нужно время, чтобы оно доросло до реальных задач. В целом, если спрашивать зачем оно нужно, то такие доказательства дополняют тесты, потому что тесты не могут покрыть все случаи, а док-во может.

Ответы: >>489014

01 Июн, 11:00 #181 #489014

>>488978
>Мне кажется ты как-то сильно привязался к Idris и хочешь для себя решить, что он на самом деле и не нужен совсем.
Я хочу понять, нужен он или нет, и если да, то для чего именно.

>Только это и позволяет выражать и доказывать эти самые свойста.
Да нет, не только это. Программы верифицировали задолго до появления языков с зависимыми типами.

>Эм, чтобы проверять доказательства на компьютере.
Доказательства можно проверять на компьютере и без всего этого. Совершенно необязательно записывать их как часть самой программы.

Ты что, пытаешься обосновать, что этот механизм записи доказательств внутри самой программы - единственный способ верификации? Это, очевидно, не так. С помощью Coq, например, можно верифицировать программы на С, хаскеле, других языках. Посмотри также Why3. Это state of the art в верификации.
Единственная возможная полезность от возможности представления доказательств в коде программы, это какое-то облегчение процесса верификации. Тут мы и возвращаемся к изначальному вопросу:
Как это помогает в чем-либо?

Пример с вектором не надо приводить. Мы его исследовали и пришли к выводу, что в этом случае идрис не предоставляет значительно более мощные механизмы, чем другие языки с зависимыми типами. Но где тогда потенциал раскрывается? Хоть один пример есть? Чтобы можно было сказать, что не будь тут зависимых типов, это было бы гораздо труднее?

>забыли математиков
У современных математиков другие заботы. Мало кто из них использует подобные инструменты. Компьютер для них это печатная машинка.

Ответы: >>489035, >>489121, >>489189

01 Июн, 12:00 #182 #489035

>>489014
> Как это помогает в чем-либо?
Например тем, что можно использовать определения и функции, которые уже есть в рабочем коде?

Ответы: >>489037

01 Июн, 12:13 #183 #489037

>>489035
Кроме того, возможен случай, когда мы не хотим доказывать всю программу (так как это непростая задача), но хотим, чтобы аргументы функции и/или возвращаемое значение подчинились каком-то условию, причём чтобы это проверялось на этапе компиляции.

Ответы: >>489044

01 Июн, 12:35 #184 #489044

>>489037
Ты про контракты что ль?
http://en.wikipedia.org/wiki/Design_by_contract

Ответы: >>489047

01 Июн, 12:50 #185 #489047

>>489044
Можно и так. Только зависимые типы позволяют формулировать практически любые утверждения и проверять их во время компиляции. Например, если ты предполагаешь, например, что где-то в коде список не может быть пуст или число не может равняться нулю или что-то ещё, ты можешь это сформулировать и попробовать доказать.

Ответы: >>489053

01 Июн, 13:00 #186 #489053

>>489047
Но для этого не нужны зависимые типы. Вот статья про статическую проверку контрактов в дотнете: https://msdn.microsoft.com/en-us/magazine/hh335064.aspx
Суть: пишешь контракт в виде произвольного выражения на шарпе (тоже можешь использовать свой код там, все что хочешь):
public void ProcessOrder(int orderId)
{
Contract.Requires<ArgumentException>(orderId >0);
...
}

И все это проверяется статически, получаешь предупреждение, если контракт не доказан. Зависимых типов в шарпе нет.

Ответы: >>489058

01 Июн, 13:09 #187 #489058

>>489053
> И все это проверяется статически
Очень хуево там проверяется, я пробовал. В основном контракты используют в рантайме как сорт оф обычные ассерты.

Ответы: >>489062

01 Июн, 13:16 #188 #489062

>>489058
Это всего лишь слабость прувера. Мы же не пруверы тут сравниваем. Да и можно подумать, в идрисе мегакрутой прувер какой-то.

Попробую потом пример с вектором на контрактах сделать. Посмотрим, осилит ли это верификатор.

Ответы: >>489080, >>489140

01 Июн, 13:51 #189 #489080

>>489062
Заодно попробуй ту задачу с моноидом.

01 Июн, 14:42 #190 #489121

>>489014
> в этом случае идрис не предоставляет значительно более мощные механизмы, чем другие языки с зависимыми типами
Фича идриса в том, что он, в отличие от Coq и агды, стремится стать языком для _разработки_, а не доказательств (но и не байтоёбли, как у ATS). Поэтому он обвешан синтаксическими плюшками и сильно заморачивается на тему компиляции.

Ответы: >>489189

01 Июн, 15:12 #191 #489140

>>489062
Прям тут попробуй что-нибудь
http://www.pexforfun.com/default.aspx?language=CSharp&sample=MethodCalls

Ответы: >>489252

01 Июн, 16:06 #192 #489189

>>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)

>идрис не предоставляет значительно более мощные механизмы, чем другие языки с зависимыми типами

>(на самом деле нового там - другой подход к работе с грязными функциями: библиотека Effects).

>У современных математиков другие заботы. Мало кто из них использует подобные инструменты. Компьютер для них это печатная машинка.
Лол, да, мало, но использовать то уже можно (что я и пытаюсь делать, да из этого небольшого числа).

Контракты, это вообще совершенно другой подход.

Добавлю, что половины этого треда не было бы, если бы люди просто изучали логику и логические системы, а потом бы просто смотрели на каких логических системах построены пруверы. Если я где-то не прав, то буду рад корректировкам.

Ответы: >>489245

01 Июн, 17:45 #193 #489245

>>489189
Ничего я не игнорю. Я пытаюсь добиться какого-то конкретного примера, который бы явно показывал преимущества подхода идриса. Вот ты говоришь, мол, контракты это другой подход. Ок. Чем он хуже?

>Лол, да, мало, но использовать то уже можно
Я сам всеми руками за формализацию матеметики. Но факт налицо: математики сами в этом не заинтересованы. Занимается этим полтора программиста, а работы там невпроворот.
Нет никакой мотивации это делать у сообщества. Ну формализовал ты доказательство какой-нибудь стопервой теоремы Коши. Кому это надо? Только, возможно, тебе самому при формализации стовторой. А больше никто даже не посмотрит на твою работу, и тем более не оценит. Теорема старая, в ее верности никто и не сомневался.

Про Why3 не понял мысли. Это значит, что на нем нельзя доказывать свойства всех программ на хаскеле и скале? Мне это ок. Если он позволяет нормально рассуждать о программах на С или джаве, например, этого вполне достаточно.

Ответы: >>489270

01 Июн, 17:49 #194 #489252

>>489140
Интересно, спасибо. Но я не знаю, как там ввод-вывод делать. Он, похоже, только функцию Puzzle принимает.

01 Июн, 18:11 #195 #489270

>>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).

Контракты не позволяют добиться абсолютной истинны так сказать. То есть контракты, это когда мы берем язык и начинаем его ограничивать и вырезать разные плохие случаи. Зависимые же типы - это когда мы строим чистую систему, в которой все корректно изначально. Когда применять одну, а когда другую зависит очевидно от задачи. Но для математики, понятно, нужно использовать формальную систему типов.

Ответы: >>489293, >>517761

01 Июн, 18:38 #196 #489293

>>489270
>На западных конференциях об этом говорят
Лал, об этом "говорят" как минимум лет 15, а скорее всего и гораздо дольше. Вот про такое ты хоть слышал: http://mizar.uwb.edu.pl/ ? Вон у них целый журнал нечитаемых статей есть: http://mizar.uwb.edu.pl/fm/ . С 1976 года это продолжается. А воз и ныне там.
Не думаю, что НоТТ в корне поменяет ситуацию и все прям кинутся писать доказательства в coq.

Ответы: >>489303, >>489306

01 Июн, 18:54 #197 #489303

>>489293
Да, но только лишь слышал.

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

Вроде бы Mizar берут (брали) только когда нужно было формализовать что-то в рамках ZF, а сейчас не берут потому что банально устарело, это же все таки ПО и требования к интерфейсу у пользователей растут.

Ответы: >>489315

01 Июн, 18:58 #198 #489306

>>489293
На чём он вообще основан? Тот же CoC появился только в 1986.

Ответы: >>489315

01 Июн, 19:23 #199 #489315

>>489306
Проприетарная система.
>>489303
Ну а как быть с их базой? Они утверждают, что это самая большая библиотека формализованной математики. На помоечку?
Глядя на это, у людей не прибавляется энтузиазма вкладываться в другие системы.

Ответы: >>489324

01 Июн, 19:35 #200 #489324

>>489315
Почему на помойку? Есть база, есть софт в котором эта база работает. Если кому-то нужны эти теоремы, определения и т.д., то он конечно будет писать доказательства на Mizar. Я думаю понятно, почему вопроса о переносе всего этого дела под другую формальную систему не стоит.

Тут уже получается столкновения как раз двух миров: математики и программирования. В одной все фундаментально и имеет значение всегда, когда в другой все быстро устаревает. Ну и я так понимаю Mizar мало используют именно потому что эту базу очень трудно использовать.

Эта проблема на самом деле уже есть у тех же Agda или Idris. Оба языка развиваются и код написанный год или два назад уже не тайпчекается. И здесь придется людям как-то выкручиваться: математикам учиться нормально программировать, а программистам нормально учить математику. Но это если мы говорим о создании какой-то библиотеки, которая будет потом кем-то использоваться, а не только для себя. Просто почти весь код на таких языках пока исследовательский и ни у кого в голове мыслей нет, что кто-то захочет это потом использовать напрямую, а не просто изучить.

01 Июн, 21:41 #201 #489411

Протестил это >>487901 с контрактами в шарпе.
Единственный контракт: в скалярном произведении длины должны быть равны. 3е ему слабо сделать, никак не доходит. Все остальное работает, в т.ч. нагромождения конкатенаций, где нужна ассоциативность и коммутативность сложения.

02 Июн, 01:28 #202 #489503

Что же вы, крестоносцы? Доказали уже корректность квиксорта на шаблонах?

Ответы: >>490390, >>492513

02 Июн, 17:42 #203 #489975

Бамп.

sage 02 Июн, 23:08 #204 #490164

> зависимые типы на крестах
-> /guro/

03 Июн, 11:56 #205 #490390

>>489503
Та еще задачка.

06 Июн, 21:14 #206 #492513

>>489503
Что-то скукожились все крестоносцы, эх.

Ответы: >>492525

06 Июн, 21:24 #207 #492525

>>492513
Доказательство сортировки на Idris тоже никто пока не доставил.

Ответы: >>492554, >>492558

06 Июн, 22:21 #208 #492554

>>492525
Держи на агде https://github.com/bitonic/agdastuff/blob/master/Quicksort.agda

Ответы: >>492560, >>492589

06 Июн, 22:28 #209 #492558

>>492525
https://github.com/bmsherman/blog/wiki/Quicksort-in-Idris

Ответы: >>492560, >>492589

06 Июн, 22:40 #210 #492560

>>492558
>>492554
Однако. Держите тогда и ATS до кучи: http://www.illtyped.com/projects/patsolve/qsort.html

Ответы: >>492589

07 Июн, 00:22 #211 #492589

>>492554>>492558
Квиксорт на списках это просто пушка.
Алсо, алгоритм без анализа сложности - кусок дрисни, а не алгоритм. Хотя, функциональщики же не могут в анализ сложности, я совсем забыл.
>>492560 Вот вроде хорошо зделали, но не осилил пока

Ответы: >>492719, >>493333, >>493425

07 Июн, 12:29 #212 #492719

>>492589
> Квиксорт на списках это просто пушка.
Вот поэтому в ОП-посте и предлагается доказывать сортировку слиянием, ибо она куда ближе к ФП.

08 Июн, 15:53 #213 #493333

>>492589
Там тоже нет анализа сложности, про эффективность это просто вскукарек.

08 Июн, 18:32 #214 #493425

>>492589
> Алсо, алгоритм без анализа сложности - кусок дрисни
Анализ сложности проводят при создании алгоритма, а не при его реализации. Впрочем, на зависимых типах и это можно сделать:
http://www.cse.chalmers.se/~nad/publications/danielsson-popl2008.pdf
https://github.com/lives-group/time-complexity-verification

21 Июн, 05:30 #215 #500670

Бамп.

25 Июн, 19:25 #216 #503910

Может лучше этот тред сделать в /cs/ или /sci/? Или если доска закрыта, то уже все?

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

Ответы: >>503976

25 Июн, 21:04 #217 #503976

>>503910
/cs/ закрыта, а /sci/ немного мимо.

17 Июл, 01:09 #218 #515867

Всё это хорошо, но где бы ознакомиться с этим, так, что б было понятно пхп-господину? Совершенно же мистическая штука, не?
Раз уж тред один черт тонет, поясните, что вообще делает тип зависимым и для чего он нужен. Изучав паскаль в школе, предположу, что заголовок функции: function dup(data array len of Integer): array len*2 of Integer; или, например record T: Type;y :T end; могут быть как-то связаны, однако, хотелось бы знать наверняка. Надеюсь на вашу снисходительность.

Ответы: >>515936

17 Июл, 04:44 #219 #515936

>>515867
Прочитай сначала тред целиком.

Ответы: >>516958

19 Июл, 04:15 #220 #516958

>>515936
А потом ты мне сразу расскажешь? Или блиц тест проведешь?

Ответы: >>516965

19 Июл, 07:01 #221 #516965

>>516958
Просто в треде на твой вопрос уже ответили и примеры привели.

20 Июл, 07:47 #222 #517501

Я как-то тут создавал тред про верификацию своего простого комбинаторного алгоритма с конечным множеством входных вариантов. В итоге выяснилось, что проще ручками доказать. Типа формальная верификация - это не хуяк-хуяк: "Ваша программа верна", а буквально самому по шагам писать доказательство, только формально. Короче, хуйня без задач, не взлетела за десятилетия, не взлетает и не взлетит.

Ответы: >>517511, >>518178

20 Июл, 08:52 #223 #517511

>>517501
> В итоге выяснилось, что проще ручками доказать.
Алгоритм? Разумеется, вручную проще. Реализацию? А вот тут уже нет, увы.

20 Июл, 17:31 #224 #517761

>>489270
>Никто и не говорит о формализации теорем из матана (хотя на самом деле хорошее занятие и упражнения).
Есть и такое.

Мимоконструктивист

Жду, когда агды станут более удобо варимыми

Ответы: >>518178

20 Июл, 19:12 #225 #517824

Раз зашел разговор про надёжность, расскажите, как в той же Агде, где функции "not allowed to crash", обрабатываются всевозможные переполнения: целочисленного, стека, памяти? Тут ведь исключительно от аппаратной составляющей зависит довольно много. Если совсем по-хардкору, следовало бы, пожалуй, компилятору самостоятельно определять системные требования, и соответствие им актуальной системы, что для общего случая и невозможно. В реальном-то мире как борятся с подобным непредсказуемым поведением системы? Есть ли какие-то популярные решения в языках неподдерживающих исключения?

Ответы: >>518178, >>540273

21 Июл, 10:22 #226 #518178

>>517501
Ну дак а как ты думал, что оно все само? С тактиками ещё как-то можно, но все равно муторно.

>>517761
Не надо ждать, надо писать. Ну я пытаюсь в свободное время, но там дофига делать. Там ещё проблема в том, что стандартная библиотека бедновата.

>>517824
Всё зависит от бекенда. Потому что сейчас есть бекенд, который просто компилит в хаскелл, то есть перекладывает на него большинство проблем.

Ответы: >>518757

21 Июл, 22:14 #227 #518757

>>518178
Погугли Formalizing 100 theorems in HOL light.

22 Июл, 10:59 #228 #519012

Доставлю-ка сюда ещё один прувер.

https://github.com/leanprover/lean
Учебник: http://leanprover.github.io/tutorial/tutorial.pdf или https://leanprover.github.io/tutorial/index.html

22 Июл, 14:48 #229 #519079

Изучая вопрос часто встречаю утверждение, что функция принимает/возвращает некое доказательство. Что это вообще за материя? Есть ли подобное в бэйсике? С чем-нибудь из императивного програмирования это можно сравнить?

Ответы: >>519088, >>519092, >>519103

22 Июл, 15:08 #230 #519088

>>519079
Она со списками работает, получает два указателя, из одного списка создаёт другой.
С задачей быстрой сортировки проще всего сравнить.
А если делать на анафорических лямбдах, тах задачка вообще на пять минут.

Ответы: >>519172

22 Июл, 15:26 #231 #519092

>>519079
В языке с зависимыми типами, тип — то же самое, что предикат, а, соответственно, значение типа — высказывание. В то же время, тип функции соответствует формулировке теоремы, тело функции — доказательству (в смысле самого вывода их начальных положений того, что требуется), а результат функции — итоговому высказыванию. Это итоговое высказывание и называют обычно «доказательством» в смысле итогового результата.
Почитай http://docs.idris-lang.org/en/latest/tutorial/theorems.html, там не очень сложно.
> Есть ли подобное в бэйсике? С чем-нибудь из императивного програмирования это можно сравнить?
Нет.

Ответы: >>519172

22 Июл, 15:39 #232 #519103

>>519079
В бэйсике нет, но в любом статическом языке доказывается теорема, что программа не упадет от несовпадения типов. См. изоморфизм Карри — Ховарда.

Ответы: >>519172

22 Июл, 18:07 #233 #519172

>>519088
Это мне ответ был? Прости, я ничего не понял.
>>519092
>>519103
Спасибо огромное, потихоньку проясняется.
Мало знаком с функциональным программированием, поэтому, для зацепки пытаюсь искать какие-то аналогии вещам знакомым.
>В языке с зависимыми типами, тип — то же самое, что предикат
Вот пример из Ады 2012:
subtype Even is Integer with
Dynamic_Predicate => Even rem 2 = 0;
теперь при попытке ассигнации переменной типа Even будет производиться проверка Dynamic_Predicate. Вопрос: это каким-то боком вообще касается исходной темы, или просто другой механизм повышения надёжности?

Ответы: >>519215, >>519495

22 Июл, 19:32 #234 #519215

>>519172
> при попытке ассигнации переменной типа Even будет производиться проверка Dynamic_Predicate
...во время выполнения, верно?

Ответы: >>519239

22 Июл, 20:29 #235 #519239

>>519215
>...во время выполнения, верно?
Абсолютно. А принципиальна именно проверка на этапе компиляции?
Кстати, подобный механизм, ведь, в принципе, будет работать при сборке: константу можно проверить сразу, для произвольного значения - принудительно проверять на вхождение в подтип (if Dynamic_Predicate(val) then ev := val) перед присваиванием? Это и имеется ввиду?

Ответы: >>519377

22 Июл, 21:19 #236 #519255

Вас не заебало ещё этим изоморфизмом везде тыкать, профаны? Паверсет натуральных чисел тоже изоморфен действительным числам и ни один из этих изоморфизмов не вычислим. Мы говорим о конкретных задачах из практики, а не о овечках в облаках. Пока что доказательства приходится выводить, как мы уже неоднократно убедились, ручками. Вопрос: почему прошло столько времени и нет видимого, признаваемого комьюнити прогресса? Почему даже ФЯП, в конце концов, не в продакшене? Десятилетия прошли, сколько ещё ждать? Ещё несколько десятилетий?

Ответы: >>519313

23 Июл, 00:06 #237 #519313

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

Ответы: >>519495

sage 23 Июл, 00:21 #238 #519323

Хватит уже пастами меряться. Пишите по теме.

23 Июл, 06:42 #239 #519377

>>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!

Ответы: >>519895

23 Июл, 13:01 #240 #519495

>>519172
>Это мне ответ был? Прости, я ничего не понял.
Я имел в виду, что на вход подаётся список:
(' x y)
А на выходе выползает:
(меньше x y)
и это тоже список. Ну и >>519313-чародей всё правильно сказал.

24 Июл, 07:04 #241 #519895

>>519377
Прости, серьёзно завис над синтаксисом:
>data (=) : a -> b -> Type where
Это тип/функция принимающая два аргумента, так? Refl - конструктор принмающий один(x)?
В Refl : x = x знак "=" это, скажем, служебный символ или рекурсивный вызов? Так и не нашёл где бы описывали язык целиком, а не его отличия от хаскеля.
>```
>trans : (a = b) -> (b = c) -> a = c
>trans Refl Refl = Refl
>```
Это и есть тип-доказательство? Боюсь спросить глупость, но как его теперь использовать?

Ещё раз про чётность/нечётность: нашёл определение на idris этих, собственно, понятий, так вот определения компилятору достаточно для того, чтобы установить четность суммы нечетных, или тоже требуется доказательство?

Ответы: >>519909

24 Июл, 09:22 #242 #519909

>>519895
> Это тип/функция принимающая два аргумента, так?
Это конструктор типа, берущий два значения. А 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 этих, собственно, понятий, так вот определения компилятору достаточно для того, чтобы установить четность суммы нечетных, или тоже требуется доказательство?
Надо доказывать. Но там доказательство совсем простое будет.

Ответы: >>520948

26 Июл, 12:01 #243 #520948

Я тут разбираюсь с Agda и у меня есть вопросы.
Есть ли где-нибудь лаконичное и четкое описание какого-нибудь варианта MLTT?
Я некоторое время назад формализовал совершенно не впечатляющую теорему о том, что произведение натурального на четное четно. В процессе я доказал и лемму о том, что сумма двух нечетных четна. Но это произошло на 126 строке и все что выше было нужно для этой леммы. Правда в учебных целях я ничего не импортировал и если вместо ручного доказательства ассоциативности сложения и т.п. импортировать его из стандартной библиотеки, то все-равно разработка теории четности до этой леммы заняла бы строк 30. Как утверждает >>519909 подобные вещи делаются очень просто. Можно ли показать, как? Или несколько десятков строк - это и есть совсем просто?

17 Кб, 604x439

26 Июл, 13:55 #244 #520983

>
> что произведение натурального на четное четно. В процессе я доказал и лемму о том, что сумма двух нечетных четна. Но это произошло на 126 строке и все что выше было нужно для этой леммы.

Вся суть потуг петушков-формализаторов

Ответы: >>521017

26 Июл, 15:06 #245 #521017

>>520983
Конечно гораздо проще немного помахать руками и сказать что утверждение очевидно. Правда, немного неприятно, когда через двадцать лет в утверждении находят небольшую неточность.

Ответы: >>521035, >>521054

26 Июл, 16:12 #246 #521035

>>521017
Но ведь вывод - тоже махание руками, только на процессоре. А ну как у него в микрокоде баг?

Ответы: >>521053

9 Кб, 256x192

26 Июл, 16:44 #247 #521053

>>521035
> А ну как у него в микрокоде баг?
Как же вы заебали.

Ответы: >>521065

26 Июл, 16:45 #248 #521054

>>521017
Тащемта, история знает несколько формализаторов, которые доказали, а потом нашлась небольшая неточность. Например, про летательные аппараты тяжелее воздуха, летательные аппараты с вертикальным взлётом, (iirc) подводные лодки и известный каждому быдлану шмель.
Алсо, у тебя нет доказательств, что в твоём доказаторе нет бага. Скормить доказатор доказатору ты, по понятным причинам, не можешь. И это не говоря уже про то, что ты не можешь доказать, что ты доказал именно то, что хотел доказать, а не что-то другое, просто похожее. И такие "нет" и "не можешь" можно ещё продолжать.

Ответы: >>521063, >>521886

26 Июл, 16:55 #249 #521063

>>521054
>Например, про летательные аппараты тяжелее воздуха
Ты совсем ебанутый? При чем тут математика вообще?

sage 26 Июл, 16:59 #250 #521065

>>521053
Ну а как ты хотел, обколются своими "доказательствами" тавтологий и тащут на двач.

28 Июл, 09:09 #251 #521886

>>521054
Если на то пошло, то если в прувере заданы хотя бы элементарные аксиомы арифметики, то окончательного доказательства, что противоречие не возникнет, быть не может.

30 Июл, 03:38 #252 #523178

Я, слыхал было, что Агда и Эпиграмм, кажется, запрещают бесконечную рекурсию. Каким образом это вообще реализуемо? Кто-нибудь интересовался? По каким словам это может гуглиться?

Ответы: >>523191, >>523236, >>523480

30 Июл, 07:36 #253 #523191

>>523178
Изоморфизм Карри-Говарда в действии. Эти языки являются одновременно языками программирования и конструктивными формальными теориями. Любая программа - это конструктивное доказательство существования чего-то (зависит от типа). Но конструктивное доказательство может соответствовать только обрывающемуся процессу вычислений.

30 Июл, 11:50 #254 #523236

>>523178
> Каким образом это вообще реализуемо? По каким словам это может гуглиться?
Гугли total functional programming.

30 Июл, 19:50 #255 #523480

>>523178
Quantifier free induction. Погугли

4 Кб, 208x104

30 Июл, 20:40 #256 #523516

Какой прувер мне выучить и что вообще почитать, чтобы генерировать автоматические решения такого как на пикрелейтед для n. Причём p<q - параметры, которые задано символьно. А то, кажется, ни одна система комп. алгебры не может толком в параметризованные суммы и продукты.

31 Июл, 02:00 #257 #523642

Поиграть принёс: https://www.verigames.com/reg/form

31 Июл, 19:00 #258 #523885

Пообщался с автором вот этого чуда http://www.mathematik.uni-muenchen.de/~logik/minlog/index.php

К таким на сраной козе не подъедешь. Хорошо иметь немецкий PhD и подписываться работником престижного немецкого вуза :) Профессор мне очень интересные вещи рассказал. Надо бы взяться за эту няшу. А то все доказательства делаю ручками уже много лет.

Мимо конструктивист-прикладник

26 Авг, 00:16 #259 #535067

Бамп же ёпты, ну.

08 Сен, 18:31 #260 #540273

На правах бампа и вдогонку >>517824 изобилирующее очевидностью рассуждение о достижимости тотальности.

Пусть некая содержащая неоптимизируюемую рекурсию функция корректно исполняется будучи вызванной из корня программы, и рушится с переполнением стека при вызове из процедуры некоторой вложенности. Для определения некоторой абсолютной тотальности алгоритму потребовались бы данные о сложности самих функций, вызывающих их фунциях и их вложенности, доступных ресурсах и самая писечка: подробная, вполоть до количества и разрядности регистров (т.к. это влияет на размер фрейма и не только), информация о самой вычислительной машине. Для задач же критичных ко времени требуется ещё куда более глубокая и детальная проработка анализатора. Задача, на мой взгляд, вполне разрешимая, однако код на языке поддерживающем подобные возможности был бы крайне громоздким. Уж куда многословней тех же исключений.

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

08 Сен, 22:44 #261 #540472

>>483770 (OP)
вот взять так и уебать этим псевдоакадемическим петушкам
когда внезапно приходит Vect n+1 a, а у тебя в коде Vect n+2 a и всё идёт по пизде
вообще на практике никто на этой параше писать не будет, потому что неподдерживаемо

Ответы: >>540484

08 Сен, 22:57 #262 #540484

>>540472
Что ж ты возгорелся-то так? Просто напиши тактику, которая всё за тебя сделает.

Ответы: >>540486

08 Сен, 23:01 #263 #540486

>>540484
то бишь boilerplate
ради чего?

Ответы: >>540529

09 Сен, 00:04 #264 #540529

>>540486
Не boilerplate, у тактик многоразовое применение.
> ради чего?
С одной стороны — контроль, с другой — можно делать вещи, которые в обычных статически типизированных языках делать нельзя.

Ответы: >>540559

09 Сен, 00:54 #265 #540559

>>540529
плиииз
приведи какой-нибудь пример
желательно - не вычисление факториала

Ответы: >>540621

09 Сен, 09:26 #266 #540621

>>540559
> приведи какой-нибудь пример
Ну, например, типобезопасный printf без костылей вроде макросов:
http://www.youtube.com/watch?v=fVBck2Zngjo
Или вот реализация бинарного формата:
http://www.youtube.com/watch?v=AWeT_G04a0A (с 24 минуты)

11 Сен, 02:27 #267 #541557

Смотрите чо https://www.manning.com/books/type-driven-development-with-idris
Неужели Idris уже такой мейнстрим?

11 Сен, 08:55 #268 #541582

Поясните для тупого, что такое тактики.

Ответы: >>542490

11 Сен, 10:45 #269 #541592

>Также можно доказать корректность реализации FizzBuzz'а, сортировки слиянием, даже неба, даже аллаха.
На уровне "можнозделать", подозреваю. Есть работающий пример программы на языке с зависимыми типами доказывающей корректность, скажем, алгоритма Крускала?

13 Сен, 15:01 #270 #542490

>>541582
Присоединяюсь к вопросу.

Ответы: >>543673

16 Сен, 03:03 #271 #543673

>>542490
Триждую вопрос.

Ответы: >>547155

22 Сен, 01:28 #272 #547155

>>543673
Квадрочую вопрос и добавляю свой.

Вычитал где-то, что Идрис в своей работе производит деконструкцию типа. Как я это понял: можно определить функцию (дальше псевдо с) вида
void quad_matrix_foo(int matrix[L*L]){...};
которая будет принимать исключительно массивы длинной в квадрат целого числа.
Правильно ли я понимаю, что для любого вызова будет произведён разбор аргумента и проверка на принадлежность к квадратам? Оно вообще вычислимо для случая посложнее, например тригонометрии и прочего?
Или же необходимо самостоятельно доказывать корректность аргумента, или создавать новый, уже нужного типа? А как вырвать нужный тип из уже определенного через другие операции числа?
Надеюсь понятно описал, поясните пожалуйста.

Тред утонул или удален.
Это копия, сохраненная 15 октября 2015 года.

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

Если вам полезен архив М.Двача, пожертвуйте на оплату сервера.

« /pr/В начало тредаВеб-версияНастройки

/a//b//mu//s//vg/Все доски

Пользуетесь скринридером — пишите, что можно улучшить.
Host-Food.ru — надёжный хостинг от 12 руб/мес | Free DNS
Зеркала М.Двача: m2ch.hk, m2ch.gq, m2ch.cf, m2ch.fapp.in, m2ch.lib, m2chfapiswfw2wcakptqp4o6ltgchvjuxfab7urxlduraomtlnhw5xad.onion