или третий

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

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

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

Они 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

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

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

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

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

Ну тайпчекеру этот пруф мало что скажет ведь. А самому в рантайме проверять валидность перестановки - не то

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

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

Зачем?)

Существование такой перестановки уже говорит нам, что массивы из одних и тех же эл-ов

Любой алгоритм сортировки должен уметь её выдавать. Некоторые по сути так и работают даже. Но не всё.

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

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

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

https://hackage.haskell.org/package/Raincat же

в твитерке все так восторжено к ней отнеслись

Хотя хз собираются ли сейчас дождекоты

Home page http://raincat.bysusanlin.com/

Правильный -> http://bysusanlin.com/raincat/

Спасибо. Но там вроде бы 2008 год.

Помню была какая-то библиотека, крутецкая.

Ну она клёвая

ещё про танки было что-то

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

Если функция сортировки записана как sort :: Vec n a -> Vec n a то нам нужно гарантировать, что а) элементы нового вектора = элементы старого вектора б) новый вектор отсортирован Теперь, если функция сортировки записана как sort :: Vec n a -> AscVec n a где AscVec n a - вектор с возрастающими элементами длины n то нам достаточно гарантировать только а), б) уже следует автоматом А другой подход может быть в том, чтобы записать сортировку как sort :: Vec n a -> Perm n a где Perm n a - перестановка длины n теперь нам надо проверять б), а а) уже есть

я не знаю, какой подход лучше. с идрисом не знаком

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

собственно вот "другой подход"

ну я это и написал:)

с unqiue types есть халяву (неформальная)

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

т.к. мы не можем ни дублировать, ни брать элементы из ниоткуда, ни забывать

это верно если метод полиморфный по элементу только

доказать не просите =)

т.к. мы не можем ни дублировать, ни брать элементы из ниоткуда, ни забывать

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

насчёт дублирования непонятно как следует из полиморфности

еще на сортировку иногда навешивают пруф complexity

уникальность/линейность требует

в смысле что дублировать нельзя

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

т.е. если есть Unique a то мы не можем создать, a

а если это Unqiue Int мы можем сделать Unique 0

если у нас a то мы не можем ничего с элементами делать

т.к. мы не можем ни дублировать, ни брать элементы из ниоткуда, ни забывать

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

наверное