Есть ли примеры Idris, которые могут быть использованы для изучения и, возможно, применения для применения в обычном/реальном мире?Практические примеры Idris
Я уверенно владею Haskell, из которых Идрис, кажется, значительно заимствует, а официальные FAQ/документация довольно приятные, но было бы очень полезно иметь более крупные примеры для изучения. Целью является попытка использовать Idris для практической разработки программного обеспечения. ТИА.
У Эдвина Брэди есть репо, полное демо на https://github.com/edwinb/idris-demos. Помимо всего прочего, в нем есть игра для захваченных космических захватчиков, написанная с использованием привязок SDL, эффектов и синтаксиса! -effect (в основном альтернативный синтаксис для do-notation/>> =).
Кроме того, мы пытаемся сохранить список некоторых доступных библиотек на вики: https://github.com/idris-lang/Idris-dev/wiki/Libraries
Может быть, «перехват привязки» - лучшее имя для! синтаксис: bang from!, binding, потому что он становится >> = (объяснение Дэвида Кристиансена в канале #idris). – pdxleif
Существует статья Эдвина Брэди, создателя Идриса, в которой рассматриваются вопросы реального мира, такие как эффективность и параллелизм: "Correct-by-Construction Concurrency: using Dependent Types to Verify Implementations of Effectful Resource Usage Protocols". Он не только объясняет, как бороться с параллелизмом, но также создает встроенный доменный язык (EDSL) в Идрисе для решения проблемы параллелизма.
Он также используется для научных вычислений (которые могут или не могут квалифицироваться как приложение реального мира): Dependently-typed programming in scientific computing. Бумага содержит фактические примеры и несколько примеров Агды.
я и в таком же положении, относительно опытный в Haskell (понимать GADT, тип семьи, и т.д ...) и глядя на изучение зависимых типов в Идрисе. Приятно было бы еще несколько примеров. – MFlamer
Только для справки, вот связанный с этим вопрос о [реальных программах agda] (http://stackoverflow.com/questions/10931316/real-programs-written-in-agda) (к сожалению, закрыт). –