間違いもあると思うが一応記録していく。
#
基本動作
基本的なコードを以下に記載する。
1
2
3
4
|
module hello where
test1 : Set → Set
test1 x = x
|
書いた定義を
C-c C-l でコンパイルすることができる。
書いたコードの解説をすると、
module hello whereは必要な宣言で、moduleの次にファイル名を記述する。test :の行は関数の宣言と仕様の記述をしている。
:の前で関数名を定義している:の後で仕様の記述をしている。
- 意味はこの関数は型がSetの引数を受けとり、返り値として型がSetのものを返す。
test =の行は関数の実装を記述している。
=の前にxがあるが、これは関数が引数としてxを受け取ったことを表している。
- 余談だがHaskellでも同じように関数の後ろに引数を記述する。
- 仕様として、引数で受け取った物をそのまま返しても成り立つ
また、=から後方を削除し、?を入力しC-c C-lすることもできる。その際に{ }が表示される。
- その中でC-c C-, すると引数に何が格納されているのか見ることができる。
- また、C-c C-a するとAuto (proof search)ができ、自動でできるならAgdaが自動的に補完をしてくれる。
関数を実行したい際にはC-c C-n で実行することができる。
コマンド群はここにも記載されている。
特殊文字などもみんなのagdaに記載されている。
#
関数定義
関数定義の際に基本となる記述を記載しておく。
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
test2 : (A : Set) → Set
test2 a = a
-- 引数を増やすこともできる。
test3 : (A B : Set) → Set
test3 a b = b
-- ()ではなく{}で方を定義することもできる。その場合{}で定義した部分の変数を隠すことができる。
test4 : {A B : Set} → A → (A → B) → B
test4 a x = x a
-- {}で定義した部分を取得することも可能
test5 : {A B : Set} → A → (A → B) → B
test5 {A} {B} a x = x a
-- 上記の{}で定義した物を()で書き換えると以下のようになる
test6 : (A B : Set) → A → (A → B) → B
test6 A B a x = x a
-- あまりスマートではないし定義の意味が{}で記述した場合と違う
|
#
data型
1
2
3
4
5
6
7
8
9
10
11
12
|
-- 次はdata型とrecord型の説明
-- 記号などはみんなのagdaにほとんど載っていたり、普通にググっても出る。
data _∨_ (A B : Set) : Set where
front : A → A ∨ B
back : B → A ∨ B
-- 関数名として_∨_を定義しているが、これで中置演算子を定義することができる。
-- 実際にやっていることは下記に定義している関数と同じ
data or (A B : Set) : Set where
front : A → or A B
back : B → or A B
|
data型というのは分岐のことであり、「どちらか一方が必ず動作する。」ということになる。
わかり易い例としてBool型の定義がある。
1
2
3
|
data Bool : Set where
true : Bool
false : Bool
|
data型を使用した例としてジャンケンを定義してみる。
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
data hand : Set where
r : hand
p : hand
s : hand
-- 「手」を二つ受け取って勝った方の手を返すように設計すると
-- 定義は「handを2つ受け取る。最終的にhandを返す」となり、以下のようになる。
rps : (A B : hand) → hand
-- rps : hand → hand → hand これでも良い
-- rps : (_ _ : hand) → hand これでもできるかもしれない
rps r r = r
rps r p = p
rps r s = r
rps p r = p
rps p p = p
rps p s = s
rps s r = r
rps s p = s
rps s s = s
|
場合分けの数が足りない場合、agdaが親切に怒ってくれる。
#
record型
data型とは違い、
オブジェクトあるいは構造体のようなもの。
以下の関数はAND。p1で前方部分が取得でき、p2で後方部分が取得できる。
1
2
3
4
5
6
7
8
9
10
11
12
13
|
record _∧_ (A B : Set) : Set where
field
p1 : A
p2 : B
-- 普通にANDの後ろの方を取得することもできる
datatest1 : {A B C : Set} → (A ∧ (B → C )) → (B → C)
datatest1 x b = _∧_.p2 x b
-- ANDの後ろの方を取得した結果を使用することもできる。
datatest : {A B C : Set} → B → (A ∧ (B → C )) → C
datatest b x = _∧_.p2 x b
|
これらを使用して三段論法を定義することができる。
定義は「AならばB」かつ「BならばC」なら「AならばC」となる。
1
2
|
syllogism : {A B C : Set} → ((A → B) ∧ (B → C)) → (A → C)
syllogism x a = _∧_.p2 x (_∧_.p1 x a)
|