Vladislav

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

Евгений

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

Евгений

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

Vladislav

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

Vladislav

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

Leonid 🦇

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

Leonid 🦇

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

Нурлан

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

Alex

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

кана

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

Anonymous

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

Aleksei (astynax)

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

Anonymous

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

кана

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

кана

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

кана

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

Alex

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

кана

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

Alex

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

odbc

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

odbc

)))

кана

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

Viacheslav

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

Type driven development with idris

Viacheslav

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

Viacheslav

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

odbc

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

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

кана

хей, я читал

кана

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

Vasiliy

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

Vasiliy

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

кана

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

Anonymous

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

Viacheslav

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

Viacheslav

Type: Type1

Anonymous

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

Viacheslav

Type2

Anonymous

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

Viacheslav

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

Anonymous

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

Viacheslav

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

Anonymous

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

Viacheslav

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

odbc

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

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

Viacheslav

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

Viacheslav

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

Viacheslav

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

odbc

Ок, спасибо)

Viacheslav

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

Viacheslav

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