エピグラム（プログラミング言語）

警句
警句
パラダイム	機能的
デザイン：	コナー・マクブライド; ジェームズ・マッキナ
開発者	メンテナンスされていない
初登場	2004年; 21年前
安定版リリース	1 / 2006年10月11日; 19年前
タイピングの規律	強い、静的、依存的
OS	クロスプラットフォーム: Linux、Windows、macOS
ライセンス	マサチューセッツ工科大学
Webサイト	web.archive.org/web/20120717070845/http://www.e-pig.org/darcs/Pig09/web/
影響を受けた
	アルフ
影響を受けた
	アグダ、イドリス

Epigramは依存型を持つ関数型プログラミング言語であり、統合開発環境（IDE）は通常この言語に同梱されています。Epigramの型システムは、プログラム仕様を表現できるほど強力です。その目的は、通常のプログラミングから統合プログラムへのスムーズな移行と、コンパイラによって正当性が検証・証明される証明をサポートすることです。Epigramは、命題を型として扱う原理とも呼ばれるカリー・ハワード対応を利用し、直観主義型理論に基づいています。

Epigramのプロトタイプは、Conor McBrideとJames McKinnaの共同研究に基づいて実装されました。開発は、英国（UK）のノッティンガム、ダラム、セントアンドリュース、そしてロンドン大学ロイヤル・ホロウェイ校のEpigramグループによって継続されています。Epigramシステムの現在の実験的実装は、ユーザーマニュアル、チュートリアル、および背景資料とともに無料で利用可能です。このシステムは、 Linux、Windows、macOSで利用されています。

現在はメンテナンスされておらず、観測型理論を実装することを目的としたバージョン 2 は正式にリリースされたことはありませんが、GitHubに存在しています。

構文

Epigramは2次元の自然演繹スタイルの構文を採用しており、LaTeX版とASCII版が用意されています。Epigramチュートリアルからの例をいくつか示します。

例

自然数

次の宣言は自然数を定義します。

 ( ! ( ! ( n : Nat !データ!---------!ここで!----------! ; !------------! ! Nat : * ) !ゼロ: Nat ) ! suc n : Nat )

宣言は、が種類Natを持つ型（つまり単純型）であり、とという2つのコンストラクタを持っていることを示しています。コンストラクタは1つの引数を取り、を返します。これはHaskellの宣言 " "と同等です。 *zerosucsucNatNatdata Nat = Zero | Suc Nat

LaTeX では、コードは次のように表示されます。

{\underline {\mathrm {data} }}\;\left({\frac {}{{\mathsf {Nat}}:\star }}\right)\;{\underline {\mathrm {where} }}\;\left({\frac {}{{\mathsf {zero}}:{\mathsf {Nat}}}}\right)\;;\;\left({\frac {n:{\mathsf {Nat}}}{{\mathsf {suc}}\ n:{\mathsf {Nat}}}}\right)

水平線表記は、「（上部にあるもの）が真であると仮定すると、（下部にあるもの）が真であると推論できる」と解釈できます。例えば、「nが型であると仮定するとNat、suc nは型ですNat。」上部に何もない場合、下部の記述は常に真です。「は（すべての場合において）zero型ですNat。」

自然数の再帰

{\mathsf {NatInd}}:{\begin{matrix}\forall P:{\mathsf {Nat}}\rightarrow \star \Rightarrow P\ {\mathsf {zero}}\rightarrow \\(\forall n:{\mathsf {Nat}}\Rightarrow P\ n\rightarrow P\ ({\mathsf {suc}}\ n))\rightarrow \\\forall n:{\mathsf {Nat}}\Rightarrow P\ n\end{matrix}}

{\mathsf {NatInd}}\ P\ mz\ ms\ {\mathsf {zero}}\equiv mz

{\mathsf {NatInd}}\ P\ mz\ ms\ ({\mathsf {suc}}\ n)\equiv ms\ n\ (NatInd\ P\ mz\ ms\ n)

ASCII の場合:

NatInd : all P : Nat -> * => P zero -> ( all n : Nat => P n -> P ( suc n )) -> all n : Nat => P n NatInd P mz ms zero => mz NatInd P mz ms ( suc n ) => ms n ( NatInd P mz ms n )

追加

{\mathsf {plus}}\ x\ y\Leftarrow {\underline {\mathrm {rec} }}\ x\ \{

\quad {\mathsf {plus}}\ x\ y\Leftarrow {\underline {\mathrm {case} }}\ x\ \{

\quad \quad {\mathsf {plus\ zero}}\ y\Rightarrow y

\quad \quad {\mathsf {plus}}\ ({\mathsf {suc}}\ x)\ y\Rightarrow {\mathsf {suc}}\ ({\mathsf {plus}}\ x\ y)\ \}\ \}

ASCII の場合:

プラス x  y <= rec x {プラスx y <= case x {プラスゼロy => yプラス( suc x ) y => suc (プラスx y ) } }

依存型

エピグラムは本質的には型付きラムダ計算であり、一般化された代数的データ型拡張を備えていますが、2つの拡張が異なります。まず、型は型の第一級実体です。型は型の任意の式であり、型の等価性は型の正規形によって定義されます。次に、依存関数型を持ちます。ではなくであり、は関数の引数（型）が最終的に受け取る値に束縛されます。 $\star$ $\star$ $P\rightarrow Q$ $\forall x:P\Rightarrow Q$ $x$ $Q$ $P$

Epigram で実装されている完全な依存型は、強力な抽象化です。( Dependent MLとは異なり、依存する値は任意の有効な型にすることができます。)依存型がもたらす新しい形式仕様機能のサンプルは、Epigram チュートリアルにあります。

参照

Epigram の前身の一つである証明支援ツール ALF 。

さらに読む

マクブライド, コナー; マッキナ, ジェームズ (2004). 「左からの視点」. Journal of Functional Programming . 14 : 69–111 . doi : 10.1017/S0956796803004829 . S2CID 6232997.
マクブライド、コナー（2004）『エピグラムの原型、うなずきと二度のウィンク』（報告書）
マクブライド、コナー（2004）『エピグラム入門』（報告書）
Altenkirch, Thorsten; McBride, Conor; McKinna, James (2005). 依存型が重要な理由（レポート）
Chapman, James; Altenkirch, Thorsten; McBride, Conor (2006). Epigram Reloaded: ETT用スタンドアロン型チェッカー（レポート）.
チャップマン、ジェームズ；ダガン、ピエール＝エヴァリスト；マクブライド、コナー；モリス、ピーター (2010). 『空中浮遊の優しい芸術』（報告書）

参考文献

^ 「エピグラム – 公式サイト」2015年11月28日閲覧。

外部リンク

公式サイト

GitHubのエピグラム 1
GitHubの Epigram2
ALF、レゴ、関連情報に関する EPSRC。2006 年からのアーカイブ版

[1] 「エピグラム – 公式サイト」2015年11月28日閲覧。