Coqでアドホック多相

overload.v

(* Coqでアドホック多相 *)
(* Coqで多引数の型クラスを用いた多相関数のサンプル *)
(* 型クラスに性質(定理)が書けるのもCoqらしさではあるが、その辺は他所でも紹介されているので割愛 *)
(* そういった機能については例えば: http://yosh.hateblo.jp/entry/20090904/p1 *)

(* 角括弧でのリスト記法が使いたかっただけなので、コンストラクタ直書きならImport不要 *)
Require Import List.
Import List.ListNotations.

(* 型クラス定義 ここでは関数を一つ持っているだけなので単に多相関数定義と思ってもいい *)
Class Join A B C := {
  join : A -> B -> C
}.

(* インスタンス定義 要素だろうがリストだろうがjoinで繋げてしまうようにする *)
(* JoinListsがJoinElementsより優先されるように、JoinElementsのpriorityを適当に下げる *)
Instance JoinElements : forall A, Join A A (list A) | 5 := {
  join a b := [a; b]
}.
Instance JoinLists : forall A, Join (list A) (list A) (list A) := {
  (* join a b := a ++ b でいいのだが、短い方にしてしまった @は暗黙引数を明示的にする *)
  join := @app A
}.
Instance JoinElemList : forall A, Join A (list A) (list A) := {
  (* join e l := e :: l でいい Coqでは(OCamlと違い)コンストラクタも部分適用可能 *)
  join := @cons A
}.
Instance JoinListElem : forall A, Join (list A) A (list A) := {
  join l e := l ++ [e]
}.

(* とりあえず++と同じ優先度にしておく *)
Infix "+++" := join (at level 60).

(* 実行例 *)
Compute (1 +++ 2). 
(* = [1; 2] *)
Compute ([1; 2] +++ [3; 4]).
(* = [1; 2; 3; 4] *)
Compute (1 +++ [2; 3]).
(* = [1; 2; 3] *)
Compute ([1; 2] +++ 3).
(* = [1; 2; 3] *)