Idris（プログラミング言語）
イドリス
パラダイム機能的
デザイン：エドウィン・ブレイディ
初登場2007年[ 1 ] （2007年）
安定版リリース
Idris2 v0.8.0 [ 2 ] / 2025年10月31日 ( 2025-10-31 )
タイピングの規律依存
OSクロスプラットフォーム
ライセンスBSD
ファイル名拡張子.idr、.lidr
Webサイトwww.idris-lang.org​​
影響を受けた
Agda、Clean、[ 3 ] Rocq（旧称Coq）、[ 4 ] Epigram、F#、Haskell、[ 4 ] ML、[ 4 ] Rust [ 3 ]

Idrisは、依存型、量注釈、オプションの遅延評価、そして全体性チェッカーなどの機能を備えた純粋関数型プログラミング言語です。IdrisはHaskellに似た汎用プログラミング言語として設計されていますが、証明支援系としても使用できます。

Idrisの型システムはAgdaの型システムに似ています。Agdaと比較して、Idrisは副作用の管理と組み込みドメイン固有言語のサポートを重視しています。Idrisは、コード生成とランタイムシステムを提供するモジュール式バックエンドによってコンパイルされます。[ 5 ] Idrisコンパイラには、 Chez Scheme、Racket、JavaScript （ブラウザベースとNode.jsベースの両方）、C言語用のバックエンドが含まれています。他のプラットフォーム向けには、サードパーティ製のバックエンドも利用可能です。[ 6 ]

イドリスは、1970年代のイギリスの子供向けテレビ番組「アイヴァー・ザ・エンジン」に登場する歌うドラゴンにちなんで名付けられました。[ 7 ]

特徴

Idris は、比較的主流の関数型プログラミング言語のいくつかの機能と、証明支援システムから借用した機能を組み合わせています。

関数型プログラミング

Idrisの構文はHaskellの構文と多くの類似点があります。IdrisでHello Worldプログラムを書くと、次のようになります。 

モジュールメインmain : IO () main = putStrLn "Hello, World!"

このプログラムとHaskellの同等のプログラムとの唯一の違いは、メイン関数の型シグネチャにコロンが2つではなく1つあることと、モジュールwhere宣言で「 」という単語が省略されていることです。[ 8 ]

帰納的およびパラメトリックなデータ型

Idrisは、帰納的に定義されたデータ型とパラメトリック多態性をサポートしています。これらの型は、従来のHaskell 98のような構文で定義できます。 

データツリーa =ノード(ツリーa ) (ツリーa ) |リーフa

あるいは、より一般的な一般化代数データ型（GADT）のような構文では次のようになります。 

データツリー:タイプ->タイプwhereノード:ツリーa ->ツリーa ->ツリーa リーフ: a ->ツリーa

依存型

依存型では、型に値が出現する可能性があります。つまり、型チェック中に値レベルの計算を実行できることになります。以下は、プログラム実行前に長さがわかっているリストの型を定義しています。これは伝統的にベクターと呼ばれます。 

データVect : Nat -> Type -> Type where Nil : Vect 0 a (::) : ( x : a ) -> ( xs : Vect n a ) -> Vect ( n + 1 ) a

このタイプは次のように使用できます。 

合計追加: Vect n a -> Vect m a -> Vect ( n + m ) aNil ys = ys を追加 追加( x :: xs ) ys = x ::追加xs ys

この関数は、 型の要素appendのベクトルを型の要素のベクトルに追加します。入力ベクトルの正確な型は値に依存するため、コンパイル時に、結果のベクトルが 型の要素を ( + ) 個だけ持つことを確実にすることができます。単語 " " は全体性チェッカーを呼び出します。このチェッカーは、関数がすべての可能なケースをカバーしていない場合、または無限ループに陥らないことが（自動的に）証明できない場合にエラーを報告します。 mananmatotal

もう 1 つの一般的な例は、長さに基づいてパラメータ化された 2 つのベクトルのペアワイズ加算です。 

合計ペア追加: Num a => Vect n a -> Vect n a -> Vect n a pairAdd Nil Nil = Nil pairAdd ( x :: xs ) ( y :: ys ) = x + y :: pairAdd xs ys

Numa は、型 a が型クラスNumに属することを意味します。片方のベクトルには大文字小文字の一致がなくNil、もう片方には数値が含まれているにもかかわらず、この関数は total として型チェックに成功していることに注意してください。型システムはベクトルの長さが同じであることを証明できるため、コンパイル時に大文字小文字の一致が発生しないことが保証され、関数の定義に大文字小文字の一致を含める必要はありません。

証明アシスタント機能

依存型はプログラムのほとんどの特性を符号化するのに十分な強力さを持ち、Idrisプログラムはコンパイル時に不変条件を証明できます。これにより、Idrisは証明支援系として機能します。

証明支援系との対話には、2つの標準的な方法があります。1つは、一連のタクティック呼び出しを記述する方法（Rocqスタイル）で、もう1つは、対話的に証明項を詳細化する方法（Epigram -Agdaスタイル）です。Idrisは両方の対話モードをサポートしていますが、利用可能なタクティックのセットはまだRocqほど有用ではありません。

コード生成

Idrisには証明支援系が含まれているため、Idrisプログラムは証明を渡すように記述できます。しかし、単純に扱うと、そのような証明は実行時に残ってしまいます。Idrisは、使用されていない項を積極的に削除することで、この落とし穴を回避することを目指しています。[ 9 ] [ 10 ]

デフォルトでは、Idris はCを介してネイティブコードを生成します。公式にサポートされている他のバックエンドはJavaScriptを生成します。

イドリス2

Idris 2は、量的型理論に基づく線形型システムを深く統合した、この言語の新しいセルフホストバージョンです。現在はSchemeとCにコンパイルできます。[ 11 ]

参照

参考文献

  1. ^ Brady, Edwin (2007年12月12日). 「Index of /~eb/darcs/Idris」 .セントアンドリュース大学コンピュータサイエンス学部. 2008年3月20日時点のオリジナルよりアーカイブ。
  2. ^ 「リリース [v0.8.0] 2025 ハロウィーンリリース」 GitHub . 2025年8月31日閲覧。
  3. ^ a b「一意性タイプ」 . Idris 1.3.1 ドキュメント. 2019年9月26日閲覧。
  4. ^ a b c「Idris、依存型を持つ言語」 。 2014年10月26日閲覧。
  5. ^ 「実行可能ファイルへのコンパイル」 . Idris 2言語のドキュメント . 2025年11月1日閲覧。
  6. ^ 「外部バックエンド」 . Idris2 Wiki . 2025年11月1日閲覧。
  7. ^ 「よくある質問」 . 2015年7月19日閲覧。
  8. ^ 「構文ガイド – Idris 1.3.2ドキュメント」 。 2020年4月27日閲覧。
  9. ^ 「使用状況分析による消去 - Idris 最新ドキュメント」 . idris.readthedocs.org .
  10. ^ 「ベンチマーク結果」 . ziman.functor.sk .
  11. ^ "idris-lang/Idris2" . GitHub . 2021年4月11日閲覧。
「 https://en.wikipedia.org/w/index.php?title=Idris_(programming_language)&oldid=1322566448」から取得