Agda2ことはじめ - ラシウラ

参考は

http://www.cs.chalmers.se/~ulfn/darcs/AFP08/LectureNotes/AgdaIntro.pdf

とAgda2添付のexamples、そしてソースコード。

一応emacsインタフェースで、コード補完(別名、証明補助)できるUIがあるのですが、自分はまったく使ってません。

一応、こういうdependently typedな言語では、式と型の区別はないようなもので、型部分でも値や関数適用ができるため、それらを合わせて項(term)として扱うのですが、そのtermの意味で式や型という語をわざと使っています。

Agda2の基本

簡単なものとして、AgdaIntroにもある、trueとfalseからなるBool型データと、その関連関数を定義しましょう。

まず、Boolデータ型

data Bool : Set where
  true : Bool
  false : Bool

構文はHaskellのGADTの構文に似ています。

SetはAgdaの組み込みの型で、基本的にはユーザーデータ型をこのようにSetの要素として定義します。

組み込みの型にはもうひとつProp型があり、Setとは独立した系をつくってます。TypeCheckingのソースを見るとPropはSetよりも少し制約があるようです(プログラミングというよりは、証明システム向けなのかな？)。ちなみにCoqも組み込みの型はSetとPropに分かれているが、その二つを含むTypeという大本の組み込み型があります。が、Agdaにはそういうすべてを含む型を記述する方法はないよう。もしそうなら、Setが対象の関数とPropが対象のの関数とは(たとえ同じ形のものでも)別々に作ることになるでしょう。

つぎは、このtrue/falseに関連する関数です。まず、not関数。

not : Bool -> Bool
not true = false
not false = true

Haskellと違い、トップレベルの関数には型指定が必須です。
また、名前とその型の区切りは「::」ではなく、「:」になります。

つぎは、or andを中値演算子として定義します。

_or_ : Bool -> Bool -> Bool
true or _ = true
false or x = x
infixr 20 _or_

_and_ : Bool -> Bool -> Bool
true and x = x
false and _ = false
infixr 30 _and_

中値演算子関数は、_xxx_として定義し、「_」がパラメータの位置になります。演算子のinfixrは右結合扱いにし、結合度を指定しています。ちなみに、演算子の名前が記号かアルファベットかの区別はないようで、記号であっても、パラメータとの間のスペースは必須のようです(そもそもAgdaはUnicode文字全般を扱う)。

演算子は、さらにパラメータが多数あってもよいようです。以下のように、if_the_else_演算子が定義できます。

if_then_else_ : {A : Set} -> Bool -> A -> A -> A
if true then x else _ = x
if false then _ else x = x
infix 5 if_then_else_

関数の型の{A : Set}は暗黙のパラメータです。関数を適用するときには、引数を指定せず推論によって引数が決まるものに使います。たとえば、このようにジェネリックな関数を作るときのパラメータ型の指定などに使います。

後述のコードでも多用しますが、暗黙引数は推論機能が走らせられるので、いろいろと便利だったりします。

Agdaの関数も、Coqと同様に、パラメータとなるものに対してすべてに適用できる全関数として定義する必要があります。再帰関数も同様に基本は停止するものしか書けません(同様にcodataもある)。

Natの定義

次に、zeroとsuccからなるNat型(0と+1で構成する自然数)とその関連関数を定義します。
これは定理証明やdependently typedなプログラミングの基本になるプログラムです。

data Nat : Set where
  zero : Nat
  succ : Nat -> Nat

意味としての0はzero、1は(succ zero)2は(succ (succ zero))というように表します。

この上での+と*を定義します。

_+_ : Nat -> Nat -> Nat
zero + m = m
succ n + m = succ (n + m)
infixl 40 _+_

_*_ : Nat -> Nat -> Nat
zero * m = zero
succ n * m = m + (n * m)
infixl 50 _*_

これらは基本的な定義で、これらの意味は、nが(succ (succ zero))だとすると、このnの式をそれぞれ:

+ m = (succ (succ m))
* m = (m + (m + zero))

と置き換えるものです。

先ほどのBool型も使う関数を定義してみます。
次に同値ならtrue、そうでなければfalseを返す関数equals n m を定義しましょう。

equals : Nat -> Nat -> Bool
equals zero zero = true
equals zero (succ _) = false
equals (succ _) zero = false
equals (succ n) (succ m) = equals n m

0 = 0はtrue、片方だけが0ならfalse、双方0でないときは、-1したもの同士で比較する定義です。

Natを使う定理の証明

次にこのNatを使ってる定理の証明を行ってみます。

証明とはいっても、やることは定理を型とみなし、その型にあるような関数を書くだけです。そして証明できたかどうかのチェックは、Agdaにソースコードを読み込ませて解釈させて型エラーが出ないことを確認することです(型エラーがでたら、証明失敗なので、通るように書き直します)。

定理全体としては、

成立する定理(命題)は型エラーがでない
成立しない定理(命題)は型エラーがでる

型による命題の表し方

まず定理をかくまえに、「aとbは同値である」という命題を型で表現するための==型を定義します。

data _==_ {A : Set} (x : A) : A -> Set where
  refl : x == x
infix 20 _==_

この定義は、coqのeqの定義とほぼ一緒の定義です。

この定義で重要なのは、唯一のメンバーであるreflの型の==のパラメータが同じものであるということです。逆に言うと、a == b は、aとbが同じものでないと、それに対応する式が作れないことになります。なぜなら x == yとなる型を表す式が存在しないからです。

つまり、reflを関数中で使うと、型チェックのときにその式の型の==の二つのパラメータがチェックされ、それらが同じでないと判定されると、そこで型エラーが出るようになります。

次に==をつかう簡単な命題「0 + n = n」を証明します。

add_zero : {n : Nat} -> (zero + n) == n
add_zero = refl

定理add_zeroは「任意のNat nについて、 0 + n == n」ということを表しています。

定理名が関数名、その型に証明する命題を書きます
暗黙のパラメータ{n :Nat}は「任意のNat nについて」という意味
- 暗黙でなくてもいい

関数定義部分ですが、add_zeroにもreflにも暗黙のパラメータがあり、それが略されています。
以下のように{}を使うことで、引数と適用ともに暗黙のパラメータを明示的に使用することもできます。

add_zero : {n : Nat} -> (zero + n) == n
add_zero {n} = refl {Nat} {n}

Adgaの型チェックで、本体「refl {Nat} {n}」の型が、「(zero + n) == n」であるかチェックされ、一応正しいことがチェックされます。型チェック時に(zero + n)が展開されてnと(項として)同型になると、判別されるためです((zero + n)を「_+_」の定義で展開して、パターンを通せばnそのものになるため)。

定理証明のしくみ

0 + nとnが同値になることは、+の定義から自動で判断できるのですが、逆のn + 0がnと同値になることは、(zero + nのときのような)reflでは自動では判定されません。

これは、n + zeroを「_+_」の定義で展開すると、nがzeroのときと、succ mのときに分かれます。そして、succ mのとき、式は「succ (m + zero)」となり、nとは(項として)同型にならないからです。

先に結果を書くと、以下のようになります。

add_zero_r : {n : Nat} -> (n + zero) == n
add_zero_r {zero} = refl {Nat} {zero}
add_zero_r {succ m} with m + zero | add_zero_r {m}
... | .m | refl = refl {Nat} {succ m}

Agdaの構文の説明:

LHS with COND_A | COND_B; LHS | VALUE_A | VALUE_B = BODY
- 引数パターンだけでなく、「with」を使うことで、さらにその引数の要素を使った条件が書けます
- 追加条件は、「|」で区切って複数書けます
- 各条件に対するパターンは、次の行に書きます。引数パターンを書き「|」の右に追加条件に対するパターンを書きます
  - 二つ目以降の「|」は追加パターンの区切りです。
- 「...」はキーワードです。LHSがまったく同じパターンになる場合につかえる省略のための記法です。つまり上のコードは以下のコードと同じです。

add_zero_r {succ m} with m + zero | add_zero_r {m}
add_zero_r {succ m} | .m | refl = refl {Nat} {succ m}

.IDENT
- 「.」つきの識別子はパターン中で使うもので、with行のドットなしのものと同じものであることを示すもののようです。ドットなしだと名前は同じでもあらたな別の変数として解釈されるようです。

前半は簡単です。nのパターンがzeroの場合はreflですみます。これは、zero + zeroを「_+_」で展開し、パターンマッチ後の式が同型になるためです。

後半は、少し複雑です。パターンがsucc mの場合、展開パターンマッチ後は、succ (m + zero)になるので、これがsucc mと同型であることを示す必要があるからです。それを示すために追加条件が入ります。

追加条件の意味はそれぞれ以下のようになります:

succ (m + zero)とsucc mが同型である ← m + zero が m と同型である: 右は成り立つかどうかわからない
add_zero_r {m} が(常に)成り立つ ⇔ (m + zero) == mがなりたつ ⇔ (m + zero) と m は同型である

という感じで、型チェックが通るようになります。前者の条件は機械的にも不要にも思いますが、この形式で記述した場合、Agda2ではこの条件がないと型チェックが通りません。

再帰データ型とcatamorphism

Natはzeroとsucc nとで構成され、succの引数はNatが入るようになってます。

そして、これまでの関連関数や証明用関数の定義部には同じ性質が存在しています。

「zeroのとき」、「succ mのとき」に分かれてる
さらに後者のsucc mのとき、再帰的にその関連関数を内部で呼び出す

Natに関するこの処理を一般化すると、以下のような関数recNatが定義できます。

recNat : {A : Nat -> Set} ->
         A zero -> ({m : Nat} -> A m -> A (succ m)) -> (n : Nat) -> A n
recNat {A} z s zero = z
recNat {A} z s (succ m) = s {m} (recNat {A} z s m)

多少複雑にみえますが、やってることは簡単です。
たとえばrecNat z sに2をくわせるということは、

recNat z s (succ (succ zero)) => (s (s z))

単にzeroとsuccをzとsに入れ替えているだけです。

つまり、zとsにzeroとsuccを渡せば、もとのものそのままになります

idNat = recNat zero succ

これまでの関数はすべて、recNatを使って定義可能です

addR : Nat -> Nat -> Nat
addR a b = recNat b succ a

mulR : Nat -> Nat -> Nat
mulR a b = recNat zero (addR b) a

add_zeroR : {n : Nat} -> (zero + n) == n
add_zeroR {n} = recNat refl (\_ -> refl) n

add_zero_rR : {n : Nat} -> (n + zero) == n
add_zero_rR {n} = recNat refl (\_ -> refl) n

equalsR : Nat -> Nat -> Bool
equalsR = recNat (recNat true (\_ -> false))
                 (\f -> recNat false (\{m} _ -> f m))

どうやら条件指定で複雑になっていたadd_zero_rも、recNatを使うと単純に書けるようです(推論が強力なのかな)。

パターンで定義した関数fをrecNatを使う定義f'へ変換する方法は:

分解する引数nに着目、
fのzeroのときの本体コードP、succ mのときの本体コードQとすると
Q中の"f m"のところを"v"に置き換えたコードQ'

f' n = recNat P (\v -> Q') n

となる

equalsはに引数ともパターン分解しているけど、引数をひとつづつrecNat定義へ変換していけば上記のequalsRになります。

equalsR = recNat recZ (\f -> recS f)
  where
    recZ : Nat -> Bool
    recZ zero = true
    recZ (succ m) = false
    recS : (Nat -> Bool) -> Nat -> Bool
    recS f zero = false
    recS f (succ m) = f m

(recSでは本体で引数のBoolを使うのではなくmを使う。この場合はsの暗黙の引数から受け取る)

このrecNatのような、dataで定義できる任意のデータ型に対してその各コンストラクタを置き換えるような関数が定義可能です(Listでは、foldrは同じような機能を持っています。)。ちなみにCoqでは、Inductiveでデータ型D定義すると、このような置き換えの意味を持つD_rect関数が自動で定義されます。

一応こういうdataで定義できる型は、圏論的にはF-Algebraというカテゴリーになっています。NatでのrecNatのような、構造をそのまま置き換えるような関数は、F-Algebraのcatamorphismと呼ばれます(ただし、引数は対応するコンストラクタ順の直積で受け取る(cataNat (z, s) n))。

逆に言えば、Agdaのような言語での関数定義のパターンマッチングは、このcatamorphismに基づくものになっています。

"Categorical programming with inductive and coinductive types"
- http://www.cs.ut.ee/~varmo/papers/ のなかにPDFがある

dependently typed なデータ型

サイズを型に含んだリスト、Vec A n型は、この典型的な例です。

data Vec (A : Set) : Nat -> Set where
  [] : Vec A zero
  _::_ : {n : Nat} -> A -> Vec A n -> Vec A (succ n)
infixr 40 _::_

いろいろなVecに関連する関数を定義してみる

head : {A : Set}{n : Nat} -> Vec A (succ n) -> A
head (h :: _) = h

tail : {A : Set}{n : Nat} -> Vec A (succ n) -> Vec A n
tail (_ :: ts) = ts

foldr : {A B : Set}{n : Nat} -> (A -> B -> B) -> B -> Vec A n -> B
foldr c o [] = o
foldr c o (h :: ts) = c h (foldr c o ts)

map : {A B : Set}{n : Nat} -> (A -> B) -> Vec A n -> Vec B n
map f [] = []
map f (h :: ts) = f h :: map f ts

_++_ : {A : Set}{n m : Nat} -> Vec A n -> Vec A m -> Vec A (n + m)
[] ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)
infixl 30 _++_

putLast : {A : Set}{n : Nat} -> A -> Vec A n -> Vec A (succ n)
putLast a [] = a :: []
putLast a (h :: ts) = h :: (putLast a ts)

reverse : {A : Set}{n : Nat} -> Vec A n -> Vec A n
reverse [] = []
reverse (h :: ts) = putLast h (reverse ts)

Listの場合、mapはfoldrを使って定義可能だけど、このVecのfoldrはmapを定義できません。つまり、前述した置き換え関数になってないということです。

そこでVecにも、対応する置き換え関数recVecを定義してみます。Natにくらべてだいぶ複雑になります(型が)。

recVec : {A : Set}{n : Nat}{B : Nat -> Set}  ->
  B zero -> ({m : Nat} -> A -> B m -> B (succ m)) -> Vec A n -> B n
recVec z c [] = z
recVec {A} {succ n} {B} z c (h :: ts) = c {n} h (recVec {A} {n} {B} z c ts)

catamorphism的には_::_側cへの暗黙引数は足りてないかも。

recVecを使った形式

foldrR : {A B : Set}{n : Nat} -> (A -> B -> B) -> B -> Vec A n -> B
foldrR f z = recVec z f

mapR : {A B : Set}{n : Nat} -> (A -> B) -> Vec A n -> Vec B n
mapR f = recVec [] (\a bs -> (f a) :: bs)

appendR : {A : Set}{n m : Nat} -> Vec A n -> Vec A m -> Vec A (n + m)
appendR  a b = recVec b _::_ a

putLastR : {A : Set}{n : Nat} -> A -> Vec A n -> Vec A (succ n)
putLastR a = recVec (a :: []) _::_

reverseR : {A : Set}{n : Nat} -> Vec A n -> Vec A n
reverseR {A} = recVec [] (\a bs -> putLastR a bs)

感想

個人的には、Haskell風になっていて構文的にAgdaはCoqに比べると、より現代プログラマフレンドリー(単一的でシンプルに書ける)になってると感じます(CoqもIsabelleとくらべれば現代プログラマよりではあるんですが。感覚的な比較としては、Agda:Coq:Isabelle = Python:Delphi:Algolくらい？)。

暗黙の引数はcoqでも使えて同じく便利な機能なのですが、coqの場合同様のことをするとき、

Sectionを作る
Variableで暗黙用変数を作る
Sectionを閉じた後、Implicit Argumentsで暗黙変数を指定する

という3段構えになってしまいます。

記法がシンプルだと、より仕組みが明示しやすいという点もあります。recNatとかそう。
証明モードや基本ライブラリもないのも、逆に証明補助のしくみも学びやすいかも。==/reflがどういう意味でそう定義されるのか、とか。

最後に、証明補助(コード生成)機能は使ってないのでわかりません。すべて本人がカバーするような範囲では、基本的に証明補助機能がだせる結果も本人的に自明なので、結局自分で書くのと変わらないです。こういう機能は、自分があまりよく意味をわかってないライブラリを使うとき、などで役に立つのでしょう。

put it all together

MyExample.agda

module MyExample where
{- Adga2 exercise -}
{- Reference:
- http://www.cs.chalmers.se/~ulfn/darcs/AFP08/LectureNotes/AgdaIntro.pdf
-}
{- exec on console
runghc Agda2/src/main/Main.hs -I MyExample.agda
-}

{- Bool -}
data Bool : Set where
  true : Bool
  false : Bool

not : Bool -> Bool
not true = false
not false = true

{- infix -}
_or_ : Bool -> Bool -> Bool
true or _ = true
false or x = x
infixr 20 _or_

_and_ : Bool -> Bool -> Bool
true and x = x
false and _ = false
infixr 30 _and_

{- many-parameter infix -}
if_then_else_ : {A : Set} -> Bool -> A -> A -> A
if true then x else _ = x
if false then _ else x = x
infix 5 if_then_else_
{- [syntax]
- {IDENT : TYPE} -> : implicit parameter: e.g. Types for explicit params
-}


{- Nat -}
data Nat : Set where
  zero : Nat
  succ : Nat -> Nat

_+_ : Nat -> Nat -> Nat
zero + m = m
succ n + m = succ (n + m)
infixl 40 _+_

_*_ : Nat -> Nat -> Nat
zero * m = zero
succ n * m = m + n * m
infixl 50 _*_

equals : Nat -> Nat -> Bool
equals zero zero = true
equals zero (succ _) = false
equals (succ _) zero = false
equals (succ n) (succ m) = equals n m

{- Nat Logic -}
{- equality: same as eq type for coq -}
data _==_ {A : Set} (x : A) : A -> Set where
  refl : x == x
infix 20 _==_

add_zero : {n : Nat} -> (zero + n) == n
add_zero {n} = refl {Nat} {n}
{- [syntax]
- {PATTERN}: refer implicit param explicitly
- {VALUE}: for args, apply implicit args explicitly
-}

add_zero_r : {n : Nat} -> (n + zero) == n
add_zero_r {zero} = refl {Nat} {zero}
add_zero_r {succ m} with m + zero | add_zero_r {m}
... | .m | refl = refl {Nat} {succ m}
{- [syntax]
- LHS with COND_A | COND_B : pattern with checking conditions
- ... | VAL_A | VAL_B = TERM : case of the condisions,
                               "..." is shortcut for the LHS
- .IDENT : unique type value in patterns for conditions (pp. 9)
-}

{- cata-morphism for Nat -}
recNat : {A : Nat -> Set} ->
         A zero -> ({m : Nat} -> A m -> A (succ m)) -> (n : Nat) -> A n
recNat {A} z s zero = z
recNat {A} z s (succ m) = s {m} (recNat {A} z s m)
{- func applied catamorphism with data constructor is id:
  recNat zero succ == id
-}

addR : Nat -> Nat -> Nat
addR a b = recNat b succ a

mulR : Nat -> Nat -> Nat
mulR a b = recNat zero (addR b) a

add_zeroR : {n : Nat} -> (zero + n) == n
add_zeroR {n} = recNat refl (\_ -> refl) n

add_zero_rR : {n : Nat} -> (n + zero) == n
add_zero_rR {n} = recNat refl (\_ -> refl) n

equalsR : Nat -> Nat -> Bool
equalsR = recNat (recNat true (\_ -> false))
                 (\f -> recNat false (\{m} _ -> f m))
{-
equalsR = recNat recZ (\f -> recS f)
  where
    recZ : Nat -> Bool
    recZ zero = true
    recZ (succ _) = false
    recS : (Nat -> Bool) -> Nat -> Bool
    recS f zero = false
    recS f (succ m) = f m
-}

{- Vector -}
data Vec (A : Set) : Nat -> Set where
  [] : Vec A zero
  _::_ : {n : Nat} -> A -> Vec A n -> Vec A (succ n)
infixr 40 _::_

head : {A : Set}{n : Nat} -> Vec A (succ n) -> A
head (h :: _) = h

tail : {A : Set}{n : Nat} -> Vec A (succ n) -> Vec A n
tail (_ :: ts) = ts

foldr : {A B : Set}{n : Nat} -> (A -> B -> B) -> B -> Vec A n -> B
foldr c o [] = o
foldr c o (h :: ts) = c h (foldr c o ts)

map : {A B : Set}{n : Nat} -> (A -> B) -> Vec A n -> Vec B n
map f [] = []
map f (h :: ts) = f h :: map f ts

_++_ : {A : Set}{n m : Nat} -> Vec A n -> Vec A m -> Vec A (n + m)
[] ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)
infixl 30 _++_

putLast : {A : Set}{n : Nat} -> A -> Vec A n -> Vec A (succ n)
putLast a [] = a :: []
putLast a (h :: ts) = h :: (putLast a ts)

reverse : {A : Set}{n : Nat} -> Vec A n -> Vec A n
reverse [] = []
reverse (h :: ts) = putLast h (reverse ts)


{- Is it cata-morphism for Vec? -}
recVec : {A : Set}{n : Nat}{B : Nat -> Set}  ->
  B zero -> ({m : Nat} -> A -> B m -> B (succ m)) -> Vec A n -> B n
recVec z c [] = z
recVec {A} {succ n} {B} z c (h :: ts) = c {n} h (recVec {A} {n} {B} z c ts)

foldrR : {A B : Set}{n : Nat} -> (A -> B -> B) -> B -> Vec A n -> B
foldrR f z = recVec z f

mapR : {A B : Set}{n : Nat} -> (A -> B) -> Vec A n -> Vec B n
mapR f = recVec [] (\a bs -> (f a) :: bs)
-- mapR {A} {B} {n} f = recVec []
--  (\{m : Nat} (a : A) (bs : Vec B m) -> (f a) :: bs)

appendR : {A : Set}{n m : Nat} -> Vec A n -> Vec A m -> Vec A (n + m)
appendR  a b = recVec b _::_ a

putLastR : {A : Set}{n : Nat} -> A -> Vec A n -> Vec A (succ n)
putLastR a = recVec (a :: []) _::_

reverseR : {A : Set}{n : Nat} -> Vec A n -> Vec A n
reverseR {A} = recVec [] (\a bs -> putLastR a bs)
-- reverseR {A} = recVec []
--   (\{m : Nat} (a : A) (bs : Vec A m) -> putLastR a bs)