Coqで型クラス

Show.v

Require Import String.
Open Scope string_scope.

(* 型クラスShowの定義 *)
Class Show (A: Set) := {
  show : A -> string
}.

(* フィールドshowの型 *)
Check @show.
(*
show
     : forall A : Set, Show A -> A -> string
((A:Set)と(s:Show A)の部分は暗黙引数となり、省略可能)
*)

(* string型をShowクラスのインスタンスとする *)
Instance ShowString : Show string := {
  show s := s
}.

(* bool型をShowクラスのインスタンスとする *)
Instance ShowBool : Show bool := {
  show b := match b with | true => "true" | false => "false" end
}.

(* 文字列はShowクラスのインスタンス *)
Definition foo := show "hello".

(* ブール型はShowクラスのインスタンス *)
Definition bar := show true.

(* 混ぜても使える *)
Definition hoge := show "hello" ++ show false.