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

ты имеешь ввиду, типа число > n и < m?

Типа того, да.

Да

В стандартно либе есть тип Fin n, который говорит что от 0 до n не включительно

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

Если ко мне вопрос, то просто для общего развития. Вглубь развиваюсь туда, куда надо, а вширь туда, где интересно)

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

Вступишь в чат по идрису, а там все про php говорят :3

Вступишь в чат по идрису, а там все про php говорят :3

ппц зашквар

А есть чат по идрису?))

https://t.me/joinchat/AAAAAD9SWO_tLd7rJ9S7Ig

Спасибо, рискнул вступить))

только не офтопьте

Спасибо, рискнул вступить))

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

только не офтопьте

Я не из тех)

насчет курса рекомендую книгу TDDwI (уже упоминали) и https://www.lektorium.tv/course/29862

если интересуют именно доказательства, попробуйте порешать упражнения из https://github.com/idris-hackers/software-foundations

насчет курса рекомендую книгу TDDwI (уже упоминали) и https://www.lektorium.tv/course/29862

я собственно курс и книгу скинул)

а, не заметил курс

я правильно понимаю, что реальный хак - это даже не IO, а именно ST и некий RealWorld

а RealWorld - некий интерфейс к системе

а IO - довольно чистая обертка над ST

Мне кажется, что разговоры про теорию типов в чатике по идрису вытесняют разговоры про идрис сюда :)

@kana_sama, в смысле ST это хак? ST это конструктор конечных автоматов, вот уж чище и тотальней не бывает. Единственный костыль это prim_WorldType, насколько я понимаю: https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/IO.idr

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

то есть это что-то вроде мутабельных переменных

речь про haskell, не idris

а вы точно про один и тот же ST говрите?

а господи

нет, вы про разные ST

я про Control.Monad.ST, ессно

а @elemir90 видимо про https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Control/ST.idr

в идрисе и хаскеле очень разные st?

ну в идрисе это совсем другая штука

в идрисе ST - что то типа трансформера индексированных монад

вообще да, обсуждения идриса в тематическом чате приветствуются :)

Бананы и линзы обратно что ли умер :(

там отпуска наложились у ведущих

Окей, а то я беспокоюсь

а RealWorld - некий интерфейс к системе

Что за RealWorld? Понятие вообще не гуглится

Что за RealWorld? Понятие вообще не гуглится

http://hackage.haskell.org/package/base-4.10.0.0/docs/Control-Monad-ST.html#t:RealWorld

Бананы и линзы обратно что ли умер :(

будем надеятся, что нет

привет всем

может кто посоветовать хорошие блоги про haskell

привет всем

здорОво!

я только этот знаю

https://joyofhaskell.com/blog.html

https://www.fpcomplete.com

Гонзалес же http://www.haskellforall.com/

Well-typed ещё https://www.well-typed.com/blog/ Пипони http://blog.sigfpe.com/

А вот такой вопрос: есть ли вакансии на Haskell. Или учить для общего развития полезно.

Если ты крутой, то есть

А вот такой вопрос: есть ли вакансии на Haskell. Или учить для общего развития полезно.

Очень широкий вопрос. Во-первых, где. Во-вторых, да, надо быть senior (не спрашивай, как им стать без вакансий для juniors)

А вот такой вопрос: есть ли вакансии на Haskell. Или учить для общего развития полезно.

Заходи на gitter и там проскакивают вакансии

Тут тоже

Не надо быть senior, но понимать конечно надо, напиши пару проектов и выложи на гитхаб

Какой-то Todo лист

Может игру какую

Это очень поможет

Да даже для слегка миддлов есть работа уже

Я java junior. Просто заметил, что некоторые фунциональные фичи. Типа монад и функторов здорово упрощают жизнь и убирают костыли из кода.

Ты ещё много заметишь ?

Пиши, задавай вопросы в этом чате или в гиттере, всегда помогут

Я java junior. Просто заметил, что некоторые фунциональные фичи. Типа монад и функторов здорово упрощают жизнь и убирают костыли из кода.

Есть дорога через скалку)

folks, писал ли кто-нибудь бэкенд на хаскеле?)

т.н. haskallator

folks, писал ли кто-нибудь бэкенд на хаскеле?)

писали

нужно написать один микросервис, хочу на хаскеле попробовать, благо он очень небольшой (5 эндпоинтов). Какой стек использовать?

servant

Скилл какой?

Хаскеля :)

знаю идрис

но опыта нет вообще

Смело

тогда servant не напугает :) (после идриса)

откуда все знают идрис?

что вы с ним делаете?

То же, что и с хаскелем

ничего

чисто для изучения

никто не знает, только хвастаются :)

Там еще есть данные, по возможности хотелось бы хранить их без базы. Дает ли этот сервант хранить данные между запросами?

даёт

окей, спасибо

Не хранить данные это великое зло. Сразу все становится в разы сложнее.

а если хранить в файле/базе, то все окей?

Тоесть если их между запросами в приложении сохранять.

Ну лучше в базе. Должны быть типа in memory баз данных.

Можно типа redis заюзать. Но реляционная база удобней на порядок. Правда в десятки раз медленнее работает

зачем городить базу, если надо немного данных сохранить между запросами?

в чем проблема держать их в IORef или TVar ?

страннота какая-то в канале

Да, восемнадцать миллионов сообщений про монаду