# Agda入門

間違いもあると思うが一応記録していく。

## 基本動作
基本的なコードを以下に記載する。

```agda:hello.agda
module hello where

test1 : Set → Set
test1  x = x
```

書いた定義を
C-c C-l でコンパイルすることができる。

書いたコードの解説をすると、
- `module hello where`は必要な宣言で、`module`の次にファイル名を記述する。
- `test :`の行は関数の宣言と仕様の記述をしている。
    - `:`の前で関数名を定義している
    - `:`の後で仕様の記述をしている。
        - 意味はこの関数は**型**がSetの引数を受けとり、返り値として**型**がSetのものを返す。
- `test =`の行は関数の実装を記述している。
    - `=`の前にxがあるが、これは関数が引数としてxを受け取ったことを表している。
        - 余談だがHaskellでも同じように関数の後ろに引数を記述する。
    - 仕様として、引数で受け取った物をそのまま返しても成り立つ
        - Setを受け取りSetを返すだけなのでこれで良い

また、`=`から後方を削除し、`?`を入力しC-c C-lすることもできる。その際に`{ }`が表示される。
- その中でC-c C-, すると引数に何が格納されているのか見ることができる。
- また、C-c C-a するとAuto (proof search)ができ、自動でできるならAgdaが自動的に補完をしてくれる。

関数を実行したい際にはC-c C-n で実行することができる。

コマンド群は[ここ](https://agda.wiki.fc2.com/wiki/コマンド一覧)にも記載されている。
特殊文字などもみんなのagdaに記載されている。

## 関数定義
関数定義の際に基本となる記述を記載しておく。

```agda:func.agda
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型

```agda:data.agda
-- 次は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型の定義がある。
```
data Bool : Set where
  true  : Bool
  false : Bool
```
data型を使用した例としてジャンケンを定義してみる。
```agda:rps.agda
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で後方部分が取得できる。

``` agda:record.agda
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」となる。
```
syllogism : {A B C : Set} → ((A → B) ∧ (B → C)) → (A → C)
syllogism x a = _∧_.p2 x (_∧_.p1 x a)
```