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

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

Зачем?)

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

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

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

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

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

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 то мы не можем ничего с элементами делать

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

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

наверное

только сортировки на swap`ах

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

т.е. это другой класс

что не удивительно, т.к. там ты требуешь новую операции над элементами

Optparse applicative

А что, в хачкеле есть ограничения на переносы и отступы, как в пайтоне? Объявляю strOption, ставлю закрывающую скобку отдельной строкой — parse error. Сливаю с предыдущей строкой — компилится. Треш какой-то

Отступы играют роль, да

Если переносишь на другую строку, то отступ должен быть увеличен

Впрочем, можно писать с {, } и ; :)

И execParser возвращает кортеж, получается? Из него можно достать конкретный аргумент по имени?

fst / snd

или через паттерн матчинг

let (foo, bar) = execParser ...

execParser возвращает то, что конструирует аппликатив - потому и -applicative в имени пакета

Если пасер вернет record, то и доступ к опциям будет по имени (по имени поля рекорда)

Прямо в README у optparse-applicative есть пример

execParser тащемта IO возвращает

Хм, что-то System.Random теперь отвалился

execParser тащемта IO возвращает

Ну не IO, а IO smth, положим :)

но a внутре IO a - тот, что конструируется аппликативом

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

Мде, и после отката не компилится, по ходу, cabal пакет потерял, это как вообще?

Отступы играют роль, да

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

вроде же не такая сложная штука?

т.е. where не в конце, а где-нибудь в середине, по месту надобности

ну про let я знаю, если что

то есть let есть, а where нет, как-то странно

Ну лет - выражение же

where же - захардкоренный синтаксический стейтмент

да, я понимаю:) что трудно придумать рассахаренную версию такого локального where

но почему вообще это должно быть решающим фактором

возможность развернуть любую do-нотацию в >>= и >>

foo = do bar baz where baz = .... qux doox where doox = ... where doox = ... ?

такое что-то?

foo = do bar baz where baz = .... qux doox where doox = ... where doox = ... ?

отступы ужасно скачут

я пытаюсь понять этого ли хочет @Masteroid

или это про то, что у меня 2 первые where на разном уровне?

foo = do bar baz where baz = .... qux doox where doox = ... where doox = ... ?

так работает main = do x <- f print x where f = readLn :: IO Int а так нет main = do x <- f where f = readLn :: IO Int print x

то, что я напсал не поддерживается

я спрашиваю, такое ли хочется

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

так работает main = do x <- f print x where f = readLn :: IO Int а так нет main = do x <- f where f = readLn :: IO Int print x

Я правильно понимаю, что все, что в where, будет видно всему коду выше ?

у меня да

в первом варианте

do f a f b where a = 1 f c where f x = ...

не надо такого, это попахивает жаваскриптом!

Не очень понимаю, зачем это нужно, если есть лет, который субъективно лучше читается

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

let в do понятно рассахаривается - слева-направо сверху-вниз

where нормально смотрится вне тела функции, т.к. не является выражением

@Masteroid как должен рассахариваться where в середине do при условии, что where не может быть частью выражения?

да, я понимаю:) что трудно придумать рассахаренную версию такого локального where

но почему вообще это должно быть решающим фактором

возможность развернуть любую do-нотацию в >>= и >>

Потому что это говорит об отсутствии магии.

Есть чуть другая форма записи, но то что является выражением (do - является) - им и остаётся.

Если хочется where в do, то почему бы тогда let не убрать вообще? И data разрешить внутри do

И классы с инстансами и импорты!

И получим s/говно/питон/

И получим s/говно/питон/

как будто это что-то плохое ?

f :: D -> D f = do data D = Foo | Bar g :: D -> D g Foo = Bar g Bar = Foo export D g . g

не хочу такое