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

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

( ! ( ! ( n : Nat !データ!---------!場所!----------! ; !-----------! ! Nat : * ) !ゼロ: Nat ) ! suc n : Nat )

この宣言は、Nat型がカインド*（つまり、単純型）であり、2 つのコンストラクタ と を持つ型でzeroあることを示していますsuc。コンストラクタ はsuc1 つのNat引数を取り、 を返します。これはHaskell の宣言 " "Natと同等です。data Nat = Zero | Suc Nat

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

${\displaystyle {\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」となります。

${\displaystyle {\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{行列}}}$

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

${\displaystyle {\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 )

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

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

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

$\displaystyle \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 ) } }