Оглавление
Idris (язык программирования)
-
Обзор языка программирования Idris
- Idris – функциональный язык программирования с зависимыми типами и отложенным вычислением.
- Разработан как универсальный язык, похожий на Haskell, но с акцентом на управление побочными эффектами и поддержку встроенных DSL.
- Компилируется на C и JavaScript, с поддержкой других платформ через сторонние генераторы кода.
-
Особенности и синтаксис
- Синтаксис Idris похож на Haskell, с некоторыми отличиями в сигнатуре типа и объявлении модуля.
- Поддерживает индуктивные и параметрические типы данных, а также зависимые типы, которые позволяют выполнять вычисления на уровне значений.
- Функция “total” обеспечивает проверку полноты программы, а система типов может доказать инвариантность программ.
-
Генерация кода и интеграция с помощниками по проверке
- Idris генерирует машинный код на C по умолчанию, а также поддерживает генерацию JavaScript.
- Idris 2 представляет новую версию языка с интеграцией системы линейных типов и компиляцией в Scheme и C.
-
Дополнительные ресурсы
- Ссылки на официальный сайт, документацию, примеры и список помощников по проверке.