Papers/2018/nozomi-master: paper/agda.tex comparison

comparison paper/agda.tex @ 79:4985359bd08b

Update agda description

author	atton <atton@cr.ie.u-ryukyu.ac.jp>
date	Wed, 08 Feb 2017 15:52:44 +0900
parents	897fda8e39c5
children	73da47f32888

comparison

equal deleted inserted replaced

-:897fda8e39c5
+:4985359bd08b
 型システムで行なえることには以下のようなものが存在する。
 \begin{itemize}
 \item エラーの検出
-文字列演算を行なう関数に整数を渡してしまったり、データの単位を間違えてしまったり、複雑な場合分けで境界条件を見落すなど、プログラマの不注意が型の不整合となって早期に指摘できる。
+文字列演算を行なう関数に整数を渡してしまったり、複雑な場合分けで境界条件を見落すなど、プログラマの不注意が型の不整合として表れる。
-この指摘できる詳細さは、型システムの表現力とプログラムの内容に依存する。
-多用なデータ構造を扱うプログラム(コンパイラのような記号処理アプリケーションなど)は数値計算のような数種類の単純な型しか使わないプログラムよりも型検査器から受けられる恩恵が大きい。
-他にも、ある種のプログラムにとっては型は保守のためのツールともなる。
-複雑なデータ構造を変更する時、その構造に関連するソースコードを型検査器は明らかにしてくれる。
 \item 抽象化
 型は大規模プログラムの抽象化の単位にもなる。
 例えば特定のデータ構造に対する処理をモジュール化し、パッケージングすることができる。
-モジュール化されたデータ構造は厳格に定義されたインターフェースを経由して呼び出すことになる。
-このインターフェースは利用する側に取っては呼び出しの規約となり、実装する側にとってはモジュールの要約となる。
 \item ドキュメント化
-型はプログラムを理解する際にも有用である。
+関数やモジュールの型を確認することにより、プログラムの理解の助けになる。
-関数やモジュールの型を確認することにより、どのデータを対象としているのかといった情報が手に入る。
+また、型はコンパイラが実行されるたびに検査されるため、常に最新の正しい情報を提供する。
-また、型はコンパイラが実行されるために検査されるため、コメントに埋め込まれた情報と異なり常に正しい情報を提供する。
 \item 言語の安全性
-安全性のの定義は言語によって異なるが、型はデータの抽象化によってある種の安全性を確保できる。
+例えばポインタを直接扱わないようメモリアクセスを抽象化し、データを破壊する可能性をプログラマに提供しないようにできる。
-例えば、プログラマは配列をソートする関数があった場合、与えられた配列のみがソートされ、他のデータには影響が無いことを期待するだろう。
-しかし、低水準言語ではメモリを直接扱えるため、予想された処理の範囲を越えてデータを破壊する可能性がある。
-より安全な言語ではメモリアクセスが抽象化し、データを破壊する可能性をプログラマに提供しないという選択肢がある。
 \item 効率性
-そもそも、科学計算機における最初の型システムは Fortran~\ref{Backus:1978:HFI:960118.808380} などにおける式の区別であった。
+そもそも、科学計算機における最初の型システムは Fortran~\ref{Backus:1978:HFI:960118.808380} などにおける整数と実数の算術式の区別だった。
-整数の算術式と実数の算術式を区別し、数値計算の効率化を測るために導入されたのである。
+型の導入により、ソースからコンパイラがより最適化されたコードを生成できる。
-型の導入により、コンパイラはプリミティブな演算とは異なる表現を用い、実行コードを生成する時に適切な機械語表現を行なえるようになった。
-昨今の高性能コンパイラでは最適化とコード生成のフェーズにおいて型検査器が収集する情報を多く利用している。
 \end{itemize}
-型システムの定義には多くの定義が存在する。
+型システムには多くの定義が存在する。
-型の表現能力には単純型や総称型、部分型などが存在し、動的型付けや静的型付けなど、言語によってどの型システムを採用するかは言語の設計に依存する。
+型の表現能力には単純型や総称型、部分型などが存在する。
+型付けにも動的型付けや静的型付けが存在し、どの型システムを採用するかは言語の設計に依存する。
 例えば C言語では数値と文字を二項演算子 \verb/+/ で加算できるが、Haskell では加算することができない。
 これは Haskell が C言語よりも厳密な型システムを採用しているからである。
 具体的には Haskell は暗黙的な型変換を許さず、 C 言語は言語仕様として暗黙の型変換を持っている。
-型システムを定義することはプログラミング言語がどのような特徴を持つか決めることにも繋がる。
+型システムを定義することはプログラミング言語がどのような特徴を持つかを決めることにも繋がる。
 % }}}
 % {{{ Natural Deduction
 \section{Natural Deduction}
 これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなものである。
 例えば Bool 型の値を反転する \verb/not/ 関数を書くとリスト~\ref{src:agda-not}のようになる。
 \lstinputlisting[label=src:agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda}
+関数にはリテラルが存在し、関数名を定義せずともその場で生成することができる。
+これをラムダ式と呼び、\verb/\arg1 arg2 -> function body/ のように書く。
+例えば Bool 型の引数 \verb/b/ を取って not を適用する \verb/not-apply/ をラムダ式で書くとリスト~\ref{src:agda-lambda}のようになる。
+関数 \verb/not-apply/ をラムダ式を使わずに定義すると \verb/not-apply-2/ になるが、この二つの関数は同一の動作をする。
+\lstinputlisting[label=src:agda-lambda, caption=Agda におけるラムダ式] {src/AgdaLambda.agda}
+コンストラクタによって処理を分岐する場合はパターンマッチを利用する。
+関数の変数部分にコンストラクタを指定し、それぞれに対する処理を \verb/=/ で繋いで記述する。
 パターンマッチは全てのコンストラクタのパターンを含まなくてはならない。
-パターンマッチは上からマッチされていくため、優先順位が存在する。
+なお、コンストラクタをいくつか指定した後に変数で受けると、変数が持ちうる値は指定した以外のコンストラクタとなる。
-なお、コンストラクタをいくつか指定した後に変数で受けると、変数が持ちうる値は指定したコンストラクタ以外となる。
+例えばリスト~\ref{src:agda-pattern}の not は x には true しか入ることは無い。
-例えばリスト~\ref{src:agda-pattern}のnot は x には true しか入ることは無い。
+なお、マッチした値を変数として利用しない場合は \verb/_/ を用いて捨てることもできる。
 \lstinputlisting[label=src:agda-pattern, caption=Agdaにおけるパターンマッチ] {src/AgdaPattern.agda}
-なお、マッチした値を変数として利用しない場合は \verb/_/ を用いて捨てることもできる。
+Agda では特定の関数内のみで利用する関数を \verb/where/ 句で記述できる。
+これは関数内部の冗長な記述を省略するのに活用できる。
-単純型で利用した自然数もデータ型として定義できる(リスト~\ref{src:agda-nat})。
+スコープは \verb/where/句が存在する関数内部のみであるため、名前空間が汚染させることも無い。
+例えば自然数3つを取ってそれぞれ3倍して加算する関数 \verb/f/ を定義するとき、 \verb/where/ を使うとリスト~\ref{src:agda-where} のように書ける。
+これは \verb/f'/ と同様の動作をする。
+\verb/where/ 句は利用したい関数の末尾にインデント付きで \verb/where/ キーワードを記述し、改行の後インデントをして関数内部で利用する関数を定義する。
+\lstinputlisting[label=src:agda-where, caption=Agda における where 句] {src/AgdaWhere.agda}
+データ型のコンストラクタには自分自身の型を引数に取ることもできる(リスト~\ref{src:agda-nat})。
 自然数のコンストラクタは2つあり、片方は自然数ゼロ、片方は自然数を取って後続数を返すものである。
 例えば0 は \verb/zero/ であり、1 は \verb/suc zero/に、3は \verb/suc (suc (suc zero))/ に対応する。
 \lstinputlisting[label=src:agda-nat, caption=Agdaにおける自然数の定義] {src/AgdaNat.agda}
 自然数に対する演算は再帰関数として定義できる。
 例えば自然数どうしの加算は二項演算子\verb/+/としてリスト~\ref{src:agda-plus}のように書ける。
 この二項演算子は正確には中置関数である。
-前置や後置で定義できる部分を関数名に \verb/_/ として埋め込んでおくことで、関数を呼ぶ時にあたかも前置演算子のように振る舞う。
+前置や後置で定義できる部分を関数名に \verb/_/ として埋め込んでおくことで、関数を呼ぶ時にあたかも前置や後置演算子のように振る舞う。
-また、Agda は関数が停止するかを判定できる。
+例えば \verb/!_/ 関数を定義すると \verb/! true/ のように利用でき、\verb/_~/ 関数を定義すると \verb/false ~/ のように利用できる。
+また、Agda は再帰関数が停止するかを判定できる。
 この加算の二項演算子は左側がゼロに対しては明らかに停止する。
 左側が1以上の時の再帰時には \verb/suc n/ から \verb/n/へと減っているため、再帰で繰り返し減らすことでいつかは停止する。
+もし \verb/suc n/ のまま自分自身へと再帰した場合、Agda は警告を出す。
 \lstinputlisting[label=src:agda-plus, caption=Agda における自然数の加算の定義] {src/AgdaPlus.agda}
 次に依存型について見ていく。
 依存型で最も基本的なものは関数型である。
 なお、関数の本体で暗黙的な引数を利用したい場合は \verb/{variableName}/ で束縛することもできる(\verb/id'/ 関数)。
 適用する場合も \verb/{}/でくくり、\verb/id-true/のように使用する。
 \lstinputlisting[label=src:agda-implicit-id, caption=Agdaにおける暗黙的な引数を持つ関数] {src/AgdaImplicitId.agda}
-Agda にはレコード型も存在する。
+Agda には C における構造体に相当するレコード型も存在する。
 定義を行なう際は \verb/record/キーワードの後にレコード名、型、\verb/where/ の後に \verb/field/ キーワードを入れた後、フィールド名と型名を列挙する。
 例えば x と y の二つの自然数からなるレコード \verb/Point/ を定義するとリスト~\ref{src:agda-record}のようになる。
 レコードを構築する際は \verb/record/ キーワードの後の \verb/{}/ の内部に \verb/fieldName = value/ の形で値を列挙していく。
 複数の値を列挙する際は \verb/;/ で区切る。
 そのモジュールは引数に型Aと二項演算子 \verb/</を取り、ソートする関数を提供する。
 \verb/Sort/モジュールを \verb/Nat/ と \verb/Bool/ で利用した例がリスト~\ref{src:agda-parameterized-module}である。
 \lstinputlisting[label=src:agda-parameterized-module, caption=Agda における Parameterized Module] {src/AgdaParameterizedModule.agda}
-% TODO: where 句の説明
 % }}}
 % {{{ Reasoning
 \section{Reasoning}

Mercurial > hg > Papers > 2018 > nozomi-master

comparison paper/agda.tex @ 79:4985359bd08b