История изменений

В целом конечно идрис очень интересен. Но скажем, если Хаскель можно без страха использовать, то с идрис такой фокус не прокатит пока что на сколько я понимаю. Версия 0.99 имела пометку вроде «ну как готов к продакшену: готов то готов, но у нас пол человека им не занимается на фултайм, а улучшать ещё есть чего». Не знаю висит ли чейчас (лениво смотреть).

Ещё один аргумент - все эти монады, комонады, функторы, аппликативы - они сохраняются. А все туториалы по этим штукам - они как правило хаскель-ориентированы. Туториалы по агде/идрису часто прямо говорят: обязательное требование - знание хаскеля. Иногда говорят «ну типа если вы программировали то должно получится», но это по моему смотря что «должно получится». Если писать реальные приложения в итоге, то эту машинерию надо знать.

Итого: если чисто поиграться именно с зависимыми типами - то замечательный выбор.

Правда если не знаком с техническими моментами (опять, функторы, аппликативные функторы, монады), то их придётся осваивать по ходу и туториалы всё на том же хаскеле.

В целом конечно идрис очень интересен. Но скажем, если Хаскель можно без страха использовать, то с идрис такой фокус не прокатит пока что на сколько я понимаю. Версия 0.99 имела пометку вроде «ну как готов к продакшену: готов то готов, но у нас пол человека им не занимается на фултайм, а улучшать ещё есть чего». Не знаю висит ли чейчас (лениво смотреть).

Ещё один аргумент - все эти монады, комонады, функторы, аппликативы - они сохраняются. А все туториалы по этим штукам - они как правило хаскель-ориентированы. Туториалы по агде/идрису часто прямо говорят: обязательное требование - знание хаскеля. Иногда говорят «ну типа если вы программировали то должно получится», но это по моему смотря что «должно получится». Если писать реальные приложения в итоге, то эту машинерию надо знать.

Итого: если чисто поиграться именно с зависимыми типами - то замечательный выбор.

Правда если не знаком с техническими моментами (опять, функторы, аппликативные функторы, монады), то их придётся осваивать по ходу и туториалы на том же хаскеле.

В целом конечно идрис очень интересен. Но скажем, если Хаскель можно без страха использовать, то с идрис такой фокус не прокатит пока что на сколько я понимаю. Версия 0.99 имела пометку вроде «ну как готов к продакшену: готов то готов, но у нас пол человека им не занимается на фултайм, а улучшать ещё есть чего». Не знаю висит ли чейчас (лениво смотреть).

Ещё один аргумент - все эти монады, комонады, функторы, аппликативы - они сохраняются. А все туториалы по этим штукам - они как правило хаскель-ориентированы. Туториалы по агде/идрису часто прямо говорят: обязательное требование - знание хаскеля. Иногда говорят «ну типа если вы программировали то должно получится», но это по моему смотря что «должно получится». Если писать реальные приложения в итоге, то эту машинерию надо знать.

Итого: если чисто поиграться именно с зависимыми - то замечательный выбор.

Правда если не знаком с техническими моментами (опять, функторы, аппликативные функторы, монады), то их придётся осваивать по ходу и туториалы на том же хаскеле.