Idris (язык программирования)
Idris — функциональный язык программирования общего назначения с зависимыми типами. Использует строгую стратегию вычислений и Haskell-подобный синтаксис. Разрабатывается c 2009 года Эдвином Брэди в университете города Сент-Эндрюс.
Для компиляции программ на Idris используется стек промежуточных представлений, нисходящих по уровню абстракции. Подходящее представление затем транслируется отдельным модулем в код на другом языке. В официальную поставку включены модули для компиляции в C и JavaScript, существуют сторонние модули для компиляции в JVM, Erlang, СIL и другие языки и платформы.
Также в язык встроена мощная система метапрограммирования, использующую рефлексию так называемого элаборатора, то есть, доступ из программы к части компилятора, занимающейся преобразованием в промежуточное представление. Данный механизм позволяет, к примеру, гибко реализовывать Coq-подобные тактики, упрощающие построение доказательств.
Ссылки[править]
- Официальный сайт языка
- Сайт с документацией
- Сайт книги Brady, (2017) «Type-Driven Development with Idris»