研究に使用され、おそらくそれを汎用/「実世界」アプリケーションに適用できるイドリスの例はありますか?
私は Haskell にある程度精通しており、Idris はそこからかなり借用しているようです。公式の FAQ/ドキュメントはかなり優れていますが、調査するためのより大きな例がいくつかあると非常に役立ちます。目標は、実用的なソフトウェア開発に Idris を使用することです。ティア。
研究に使用され、おそらくそれを汎用/「実世界」アプリケーションに適用できるイドリスの例はありますか?
私は Haskell にある程度精通しており、Idris はそこからかなり借用しているようです。公式の FAQ/ドキュメントはかなり優れていますが、調査するためのより大きな例がいくつかあると非常に役立ちます。目標は、実用的なソフトウェア開発に Idris を使用することです。ティア。
Edwin Brady には、https://github.com/edwinb/idris-demosにデモが満載のリポジトリがあります。とりわけ、SDL バインディング、エフェクト、および !-effect 構文 (基本的に do 記法 / >>= の代替構文) を使用して記述された、プレイ可能なスペース インベーダー ゲームがあります。
また、ウィキで利用可能ないくつかのライブラリのリストを維持しようとしています: https://github.com/idris-lang/Idris-dev/wiki/Libraries