для unqiue или линейных типов оно автоматом будет

наверное только достаточно чтобы длина совпадала

но это надо доказывать

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

А, ну да, можно и только длину, уникальные же

автоматически её вывести из такого плохого описания нельзя

из List a -> List a или UniqueList a -> AscendingUniqueList a — да но потому мне и интересно можно ли заложить в типы саму реализацию, но так чтобы она закладывалась не ручками, а на основе реализации

ну _я думаю_ что в типы можно заложить реализацию

поскольну ничего формально не запрещает поднять реализацию на уровень типов

Написать дсл, который будет дублировать стейтменты идриса)

будет у тебя там IF a < b 'THEN ....

Чтобы реализация и тип совпадали

i.e. у тебя будет реализация на уровне типов, только непонятен толк от этого

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

Написать дсл, который будет дублировать стейтменты идриса)

слишком плохо если просто дублировать стейтменты идриса, то доказывать равенство типов будет нетривиально совсем, разве нет?

скорее всего

вообще идея инетересная в смысле оптимизаций, ведь если "поднять" формальный код на уровень типов, а потом написать оптимальный и можно будет доказать что они эквивалентны

меня можно не слушать, я в зависимых типах и т.п. понимаю не достаточно

Ну так ты же хотел биекцию. Может ошибаюсь, но если две вещи эквивалентны, то уже биекция невозможна

Ну так ты же хотел биекцию. Может ошибаюсь, но если две вещи эквивалентны, то уже биекция невозможна

я же говорил, что вопрос плохо сформуирован видимо в таком случае нужна биекция не между конкретной реализацией и типами, а между классом эквивалентности реализаций и классом эквивалентности типов

но это же то, что система типов принципиально и дает

компилятор проверяет совпадение заявленного типа, и программы?

но это же то, что система типов принципиально и дает

она не всегда достаточно точна :с хотелось бы сузить эти классы

и желательно более автоматически

а не ручками писать ~200 строк, чтобы доказать, что сортировка работает

ну типы для этого и есть, мы выражаем те свойста, которые хотим иметь

Было бы все так легко, все бы писали верифицированный код)

а сортировка это достаточно сложная и подлая штука

Было бы все так легко, все бы писали верифицированный код)

мечта!

особенно если не халявить с линейными типами

да, ладно

просто бы сложности программирования перенеслись бы на создание правильных спецификаций

возможно

сейчас то, сложность спецификаций (типов) много меньше, чем сложность программ

Индуктивные доказательства бы как-нибудь автоматизировать, а то f A = Refl f (B A) = rewrite f A in Refl Такого много

стратегии в coq не для этого?

Со стратегиями еще не знаком, с доказальствами знаком один день)

ладно наверное соседний чятик больше подойдет, так и людей больше кто с хорошим образованием по теме

а в идрисе можно писать доказательства как в коке?

А как их в коке пишут? По моему так декларативно нельзя, все через костыли изоморфизма

"Монады являются моноидами, ведь как известно, монада — это всего лишь моноид в категории эндофункторов, а монадические законы — не более чем определение моноида в контексте продолжений" Всего лишь. Как известно. С очевидностью следует. Пиздить вас кочергой.

ну тактиками

Слова "тактики и стратегии" в идрисе точно есть, видел в доке

Ну на самом деле это со временем действительно становится очевидным)

ну просто редко учат монады по определению которое интуитивно является моноидом

"Монады являются моноидами, ведь как известно, монада — это всего лишь моноид в категории эндофункторов, а монадические законы — не более чем определение моноида в контексте продолжений" Всего лишь. Как известно. С очевидностью следует. Пиздить вас кочергой.

я думаю, что если почитать книжки по теоркату, то станет проще и это действительно может оказаться простым фактом

но зря

Слова "тактики и стратегии" в идрисе точно есть, видел в доке

Они deprecated

я думаю, что если почитать книжки по теоркату, то станет проще и это действительно может оказаться простым фактом

ага, особенно политологу это полезно (кем ортега типа является)

Я пост как раз про моноиды и монады пишу. Заочка началась просто

И идрис в целом не очень для доказательств подходит

ага, особенно политологу это полезно (кем ортега типа является)

ну если тебе не интересно то зачем ты изучаешь?

ага, особенно политологу это полезно (кем ортега типа является)

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

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

хбз

ну если тебе не интересно то зачем ты изучаешь?

он возможно где-то напоролся на это

уже второй раз псит на программистов и всяких айтишников

или третий

аа это канал какого-то политолога

ну пусть дальше изучает с таким отношением

Почему-то канал его не открывается

Они deprecated

в coq

в idris

а не на моё сообщение было, ок

Так, вернёмся к другой околохаскелевой теме - определение монады как моноида на эндофункторах. Я понимаю, почему это моноид: (F : C -> C, Indentity : F, Compose : (F, F) -> F), где C - какая-то категория, но не понимаю, как из этого определения следуют join и bind

join это _3, так?

просто по определению

что за _3?

третий элемент тройки

Ну да

Стоп, нет

все же да

Там Compose, не джоин

Compose дает нам возможность работать с композиций функторов как функтором, но не заменяет функтор. Или это одно и то же?

А, ну в принципе да, одно и то же)

щас, должно переписываться одно через другое

Окей, а unit?

Definition 1.1 A monad over a category C is a triple (T, η,µ), where T: C → C is a functor, η: IdC T and µ:T2 . →T are natural transformations and the following equations hold: • µTA; µA = T(µA);µA • ηTA;µA = idTA = T(ηA);µA A

я к этому определеню больше привык

There is an alternative description of a monad (see [7]), which is easier to justify computationally. Definition 1.2 A Kleisli triple over C is a triple (T, η, ∗), where T:Obj(C) → Obj(C), ηA:A → TA, f∗:TA→ TB for f:A→TB and the following equa- tions hold: • η∗ A = idTA • ηA; f∗ = f • f∗; g∗ = (f; g∗)∗ Every

инетерсно здеть картинку можно пихать или копировлся бы латех сразу :/

тут какое-то третье определение..

Они deprecated

почему, pruviloj работает

я даже пару тактик туда контрибутнул

http://docs.idris-lang.org/en/latest/reference/tactics.html

другое дело что дебажить их еще сложнее чем обычный идрис

теперь там элаборатор

это старые, новые через elab да, pruviloj называются

а в идрисе можно писать доказательства как в коке?

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

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

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

вроде в блодвене имплициты как-то поудобнее в ядро будут вшиты

Блодвен?

кодовое название для идриса на идрисе

О, нашел

точнее пока только чекера для tt

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

можно возвращать перестановку, например

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

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