чтобы проникнуться духом -- http://thedeemon.livejournal.com/tag/idris

@gds да там факторлиалы какие-то.

@4da значит, духом ты уже проникся, ок.

@polecat ну, вообще, зависимые типы кое-где полезны. А дроч -- да, та же хуйня, какая была с функциональщиной в целом и с х-ем в частности лет 7..10 назад. Но функциональщина таки пробивается в бузинесс, очередь за зависимыми типами.

тутор почитай

@polecat функциональщина не везде применима. А зависимые типы -- считай, та же функциональщина, только на порядок выше. ФП++ лол.

@polecat по первому пункту топикстартор тебе расскажет про 3д-графику и гейдев, а я расскажу про миллипиздрические системы с 256 байтами ram, и отдельно про реалтайм-гарантии. по второму пункту -- кажется, ты не представляешь себе, что такое зависимые типы. Если представляешь таки -- прошу, опиши их в паре слов, чтобы было понятно, откуда начинать объяснять, где ты не прав.