Esistono esempi di Idris che potrebbero essere utilizzati per lo studio e forse per l'applicazione generalizzata/"mondo reale"?Esempi pratici di Idris
Sono moderatamente esperto in Haskell, di cui Idris sembra prendere in prestito in modo significativo, e le FAQ/documentazione ufficiali sono piuttosto carine, ma sarebbe molto utile avere alcuni esempi più ampi da esplorare. L'obiettivo è tentare di utilizzare Idris per lo sviluppo di software pratico. TIA.
Edwin Brady ha un repo pieno di demo al https://github.com/edwinb/idris-demos. Tra le altre cose, ha un gioco di invaders dello spazio giocabile, scritto usando i collegamenti SDL, effetti e la sintassi! -effect (fondamentalmente una sintassi alternativa a do-notation/>> =).
Inoltre, cerchiamo di mantenere un elenco di alcune librerie disponibili sul wiki: https://github.com/idris-lang/Idris-dev/wiki/Libraries
Forse "bang-binding" è un nome migliore per il! sintassi: bang dal!, binding perché diventa >> = (spiegazione da David Christiansen nel canale #idris). – pdxleif
C'è un documento di Edwin Brady, il creatore di Idris, che si occupa di domande del mondo reale come l'efficienza e la concorrenza: "Correct-by-Construction Concurrency: using Dependent Types to Verify Implementations of Effectful Resource Usage Protocols". Non solo spiega come gestire la concorrenza, ma crea anche un linguaggio specifico di dominio incorporato (EDSL) in Idris per gestire la concorrenza.
Viene anche utilizzato per il calcolo scientifico (che può o meno essere qualificato come applicazione del mondo reale): Dependently-typed programming in scientific computing. Il documento contiene esempi reali e alcuni esempi di Agda.
Sono anche in una posizione simile, relativamente esperto in Haskell (capire GADT di, tipo Famiglie, ecc ...) e cercando di esplorare tutti i tipi di dipendenti in Idris. Sarebbe bello aggiungere altri esempi. – MFlamer
Solo per riferimento, ecco una domanda relativa a [programmi agda real-world] (http://stackoverflow.com/questions/10931316/real-programs-written-in-agda) (purtroppo chiuso). –