全体 List.v

Coq の教材「ソフトウェアの基礎」、 2 回目もやりました。そろそろ機能紹介が主になってきたような、練習問題で定理証明も少なくなるのかな？ Coq の記述言語 Gallina が随分と自由度が高く思えてきます。例えば次のように糖衣構文を自在に定義できます。

(* リストの糖衣構文 *)
Notation "x :: l" := (cons x l) (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x , .. , y ]" := (cons x .. (cons y nil) ..).

(* リストの結合 *)
Fixpoint app (lhs rhs: natlist): natlist :=
  match lhs with
    | nil => rhs
    | head :: tail => head :: (app tail rhs)
  end.

Notation "x ++ y" := (app x y) (at level 60, right associativity).

似たような Haskell だとリストの結合はこんな感じ 出典 Learn You a Haskell for Great Good!

infixr 5  ++
(++) :: [a] -> [a] -> [a]
[]     ++ ys = ys
(x:xs) ++ ys = x : (xs ++ ys)

Coq の at level .. associativity というのは Haskell の infixr, infixl と同じで結合の強さを指定するんですが、随分と大きい値ですね。そんなに沢山の演算子を併用するんでしょうか。それにしても、"[ x , .. , y ]" のような直感的な書き方で字句を拡張できるなんて...。ユーザが扱える表現力が高いのは良いことだと思います。