Idrisの実際の例

Idrisの例がありますが、これは一般的な「現実の」アプリケーションに適用されていますか？Idrisの実際の例

私はハスケルに適度に熟練していますが、そのうちのIdrisはかなり借りているようですが、公式のFAQ /ドキュメントは素晴らしいですが、いくつかの大きな例があれば役に立ちます。目標は実用的なソフトウェア開発のためにIdrisを使用しようとしています。 TIA。

出典

2013-06-11 Arets Paeglis

私はHaskellの中で比較的堪能、同様の位置にもいます（...など、GADTの、タイプの家族を理解する）と、 Idrisで完全な依存型を探求しようとしています。いくつかの例をもっとうまく使ってみればいいと思う。 – MFlamer

ちょうど参照のために、ここに[実世界のagdaプログラム]（残念ながら閉じた）についての関連する質問があります（http://stackoverflow.com/questions/10931316/real-programs-written-in-agda）。 –

エドウィン・ブラディにはhttps://github.com/edwinb/idris-demosというデモが満載のレポがあります。とりわけ、SDLバインディング、エフェクト、！効果の構文（基本的にdo-notation/>> =の代替構文）を使って書かれた、再生可能なスペース侵略者のゲームを持っています。

また、我々はwikiにいくつかの使用可能なライブラリのリストを維持しよう： https://github.com/idris-lang/Idris-dev/wiki/Libraries

出典

2014-03-01 00:17:19 pdxleif

"bang-binding"はもっと良い名前です！シンタックス：！からバインドされているので、バインディングは>> =（#idrisチャネルのDavid Christiansenの説明）になります。 – pdxleif

効率性と並行性などの現実的な問題を扱うIdrisの創始者、Edwin Bradyの論文があります："Correct-by-Construction Concurrency: using Dependent Types to Verify Implementations of Effectful Resource Usage Protocols"。並行性を処理する方法だけでなく、同時実行性を扱うためにIdrisに埋め込みドメイン固有言語（EDSL）を作成します。

これは科学的コンピューティング（現実世界のアプリケーションと見なされるかもしれません）：Dependently-typed programming in scientific computingです。この論文には実際の例とAgdaの例がいくつか含まれています。

出典

2013-06-16 16:01:13 scravy

答えて

関連する問題