dependent-type - para - meta tags ejemplos

Ejemplos prácticos de Idris

Question

¿Hay algún ejemplo de Idris que pueda usarse para estudiar y quizás aplicarlo para aplicaciones de uso general / "mundo real"?

Soy moderadamente competente en Haskell, de la cual Idris parece pedir prestado de manera significativa, y la documentación / FAQ oficial es bastante buena, pero sería muy útil tener algunos ejemplos más grandes para explorar. El objetivo es intentar usar Idris para el desarrollo de software práctico. TIA.

Answer 1

Edwin Brady tiene un repositorio lleno de demostraciones en https://github.com/edwinb/idris-demos . Entre otras cosas, tiene un juego de invasores del espacio jugables, escrito usando enlaces SDL, Efectos y la sintaxis de efecto! (Básicamente una sintaxis alternativa para hacer-notación / >> =).

Además, intentamos mantener una lista de algunas bibliotecas disponibles en la wiki: https://github.com/idris-lang/Idris-dev/wiki/Libraries

Answer 2

Hay un documento de Edwin Brady, el creador de Idris, que trata cuestiones del mundo real como la eficiencia y la concurrencia: "Concurrencia correcta por construcción: uso de tipos dependientes para verificar las implementaciones de protocolos de uso de recursos efectivos" . No solo explica cómo lidiar con la concurrencia, sino que también crea un lenguaje específico de dominio incrustado (EDSL) en Idris para tratar con la concurrencia.

También se utiliza para la computación científica (que puede o no calificar como aplicación en el mundo real): programación de tipo dependiente en computación científica . El documento contiene ejemplos reales y algunos ejemplos de Agda también.