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

знакомая история

ещё есть какой-то elaborator reflection http://docs.idris-lang.org/en/latest/reference/elaborator-reflection.html

это для метапрограммирования, можно например тактики на нем лепить

А рекламировать можно? http://typetheory.ru Если кто-нибудь знает какие-нибудь другие материалы на русском, то буду рад добавить.

не открывается кстати

> стандартная рекомендация - сливать все новые > структуры напрямую в contrib в главной репе Да мне не критично. Я и сам отчасти виноват, что ввязался в это неправильным способом, поэтому переживать из-за того, что PR отклонили не стоит) Вот это видео прекрасно объяснило правила выживания в OSS: https://www.reddit.com/r/haskell/comments/6lt125/zurihac_2017_neil_mitchell_on_driveby_haskell/ И мне автор и сказал занести изменения в contrib, но я забил. Пакетный менеджер вряд ли появится скоро))

кое какие потуги делаются, вот например из последних https://github.com/Risto-Stevcev/idris-naps

там конечно по сути обертка для боуера :)

Кто нибудь в Haskell делал что-нибудь на подобии generative art, типа как на языке Processing https://www.openprocessing.org/ или как на Openframwork http://openframeworks.cc/ или как в JS https://threejs.org/ ??

была библиотека diagram вроде. у неё был какой-то кривоватый репл, типа как ideone (ну с сохранением результата) и я листал чужие примеры в надежде разобраться как там что делать. не так красиво, конечно, как на ссылках выше

Есть именно "процессинг на хаскеля" от Антона Холомьёва (https://github.com/anton-k/processing-for-haskell)

"REPL, но с сохранением результата", это IHaskell (https://github.com/gibiansky/IHaskell)

И diagrams уже цпомянули. Вот их галерея для привлечения внимания: http://projects.haskell.org/diagrams/gallery.html

еще https://github.com/nteract/hydrogen

я проверял) с хаскеллем работает

ну и еще https://qtconsole.readthedocs.io/en/stable/

Да, точно, Юпитер же умеет в QtConsole

Спасибо, а я нашел пару книг по теме The Haskell School Of Expression - Paul Hudak и The Haskell School of Music того же автора!

Эти книжки больше по теории. Впрочем, School of Music хорошая, помнится

Есть именно "процессинг на хаскеля" от Антона Холомьёва (https://github.com/anton-k/processing-for-haskell)

Реально, напоминает процессинг)

Так Антон специально делал так, чтобы было максимально похоже :)

читаю тут сноймана - https://www.fpcomplete.com/blog/2017/07/the-rio-monad - опять на тему ReaderT IO, полез смотреть код, а там UndecidableInstances - https://github.com/snoyberg/rio/blob/master/src/Control/Monad/RIO.hs#L7

читал где-то, что UndecidableInstances - признак серьёзных проблем

так ли это, или если компилятор предлагает, то можно и согласиться?

Чушь.

UndecidableInstances — это не признак ничего вообще. Можно включать и забыть.

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

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

Это IncoherentInstances, они плохие.

ага, понял, перепутал, значит

❤️

А чо, в голанг уже подвезли system f, type classes и GADT?

Вот чего захотел, нет уж, мы тебе бинарник зато быстро соберем.

А чо, в голанг уже подвезли system f, type classes и GADT?

В 2.0 обещали

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

Там ноют про отсутствие параметрического полиморфизма, а у нас про отсутствие зависимых типов. Везде ноют, а бинарники-то быстрее собираются!

Я тут хотел попробовать написать игрушечный зависимо-типовый ЯП с универсумом махло. Пацан советует, попробую написать на го

Надо быть в авангарде и ныться об отсутствии универсума махло в идрисе

Так что это, для смертных?

Универсум Махло

как говорится "golang - брутально прагматичен"

https://b.thumbs.redditmedia.com/JN-q3H3fPnYVqIfkxaRacYYxU0TpXHKtntS2Gs9N3ow.png

самому стало что это такое, но не тут-то было

http://www.cs.swan.ac.uk/~csetzer/articles/kahleSetzerExtendedPredicativeMahloPohlersFestschrift.pdf

Почему моноид в base не расширяет полугруппу?

Потому же, почему в 7.6 монада не расширяла аппликатив

обратная совместимость

Да, не, просто исторически моноид был в base до полугруппы. Так что остаётся ждать ебилдов, исправляющих эту досадную оплошность.

Вот такое меня немного коробит, но возможно у этого есть какая-то причина, которой я не знаю. Почему нельзя было использовать что-то вроде Nat?

Хотя Nat же тоже 0 может хранить, ок)

но это явно ошибка типовая, которую можно чекать в компайлтайме (как и непонятный head. который должен мейби возвращает, а кидает ошибку)

вас ждет идрис

идрис мне по некоторым необъяснимым причинам показался сырым

вот он и ждет, чтоб вы его приготовили

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

)))

http://docs.idris-lang.org/en/latest/tutorial/index.html#tutorial-index

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

Type driven development with idris

Книга вышла недавно

И не слушайте людей, которые вас в документацию отправляют, они сами ее не читали

http://docs.idris-lang.org/en/latest/tutorial/index.html#tutorial-index

Ну это я смотрел. Думал может более практический курс есть. Типа как по хаскелю на степике.

хей, я читал

до интерфейсов

туториал по идрису вполне ок для людей с бэкграундом

TDD, наверное, пойдёт и совсем нулёвым

книжка аж 50 баксов стоит, жалко сейчас

Госспаде, да идрис тот ещё proof assistant. Несколько лет назад там были проблемы с парсером. А про то, что у них Type : Type я вообще молчу

Вообще-то нет

Type: Type1

А Type1 какой тип имеет?

Type2

И до бесконечности?

Угадай какой тип имеет он

А два года назад было Type : Type и "да ладно, и так сойдёт"

в общем никто его и не позиционирует как proof assistant

Или три. Не помню, когда я в нём ковырялся.

позициониируют как язык общего назначения с зав типами и partiality

туториал по идрису вполне ок для людей с бэкграундом

Ок, тогда может есть хорошие проекты на гитхабе. Просто туториал туториалом, но какие-то стандартные идиомы, как люди на практике пишут не всегда в туториалах хорошо отражены.

Исходный код либ)

Советую читать книгу

и до этого не лезть в доку

Ок, спасибо)

http://compsciclub.ru/courses/idrisprogramming/2017-spring/?tab=classes

и вот в csclub был курс по нему

большинство инфы в книге тоже есть

http://compsciclub.ru/courses/idrisprogramming/2017-spring/?tab=classes

? спасибо

А чем хаскель то не устроил?

А чем хаскель то не устроил?

Я вот хаскель еще не могу осилить а тут люди идрис уже осваивают

А чем хаскель то не устроил?

а почему, чтобы учить что-то новое, старое должно не устраивать?)

в хаскелле завтипов вот пока нет

Мне, например, и без зав.типов норм :) Зато либы есть практически для всего, что я на хаскеле делаю

В Идрисе пока только Идрис, да и тот - сырой пока

А в Идрисе есть типы-отрезки?

Мне, например, и без зав.типов норм :) Зато либы есть практически для всего, что я на хаскеле делаю

ну а прогерам на джаве вот и без лямбд было нормально