Idris (プログラミング言語)

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

Idris の型システムはAgdaのものと似ており、証明はCoqのものと似ており、エラボレータ リフレクションによるタクティクス (定理証明関数/手順) も含まれています。 ^[6] Agda や Coq と比較すると、Idris は副作用の管理と組み込みドメイン固有言語のサポートを重視しています。Idris はC ( Cheney のアルゴリズムを使用したカスタム コピーガベージ コレクターを使用) とJavaScript (ブラウザーベースとNode.jsベースの両方) にコンパイルされます。Java仮想マシン(JVM)、共通中間言語(CIL)、LLVMなど、他のプラットフォーム用のサードパーティ コード ジェネレーターもあります。^[7]

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

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

Idris の構文は Haskell の構文と多くの類似点があります。Idrisのhello world プログラムは次のようになります。

モジュールメイン 

main : IO () 
main = putStrLn "Hello, World!"      

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

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 ) a              Nil 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に属していることを示します。1 つのベクトルに大文字小文字の一致がなくNil、もう 1 つのベクトルに数値がある場合でも、この関数は total として正常に型チェックされることに注意してください。型システムはベクトルの長さが同じであることを証明できるため、コンパイル時に大文字小文字の一致が発生しないことが保証され、関数の定義にその大文字小文字を含める必要はありません。

依存型はプログラムのほとんどのプロパティをエンコードできるほど強力であり、Idris プログラムはコンパイル時に不変条件を証明できます。これにより、Idris は証明アシスタントになります。

証明支援システムと対話する標準的な方法は 2 つあります。一連のタクティック呼び出しを記述する方法 (Coq スタイル) と、対話的に証明項を詳述する方法 ( Epigram –Agda スタイル) です。Idris は両方の対話モードをサポートしていますが、利用可能なタクティックのセットはまだ Coq ほど便利ではありません。^{[あいまい]}

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

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

Idris 2は、定量的型理論に基づいた線形型システムを深く統合した、新しい自己ホスト型言語バージョンです。現在はSchemeとCにコンパイルされます。^[12]

• 証明補助者のリスト
• トータル関数型プログラミング

• 公式ウェブサイト、ドキュメント、よくある質問、例
• HackageリポジトリのIdris
• Idris 言語のドキュメント (チュートリアル、言語リファレンスなど)