勉強記録

• Standard Libraryを読む
  • データ型と論理のGist

typeclass

「2のn乗の計算手続き」と「行列Aのn乗の計算手続き」の実装は極めて似た見た目を持つ。両者は「モノイドのべき乗」という一般化した概念の例であると理解すべき。共通する手続き・性質は typeclass上でまとめて構成・証明して、利用する際はそれをinstance化する というムダのないムーブをしよう:

• モノイドのべき乗の実装
  • べき数が0なら1を返し
  • べき数が S n なら n乗した結果に、もう1回演算した結果を返す（再帰的）
  • 例:　2のn乗、行列のn乗、リストのn回cons

typeclassの実装は単なるパラメータ化されたRecord型とみなせるが、専用の構文 Class, Instance が用意されているのでそれを使う。さて、モノイドに交換則を足した可換モノイドでは例えば(xy)^n=x^n y^nが証明できたりする。このようにtypeclassの持つ仕様を少し強めた（＝少し具体化した、少し適用領域を狭めた）typeclass を subclass という。このように typeclass のヒエラルキー構造を作って無駄のない数学的構造やデータ構造を定める習慣を付けよう。

同値関係のつくる数学的構造

Gist: https://gist.github.com/41semicolon/e164ae33ab05553a6cd1d731160446fc

格子上での経路 ↑→↑→ と ↑↑→→ は 移動先が同じという意味で/with respect to(w.r.t.) 同値関係にある（対称・反射・推移律が移動という操作において成立）。一般に同値関係を定めると同値類が決まり、同値類上で演算が定義されえて、それをProperな操作と呼ぶ。この例では「ルートの結合」「（ルートの要素＝方向に従った）移動」「ルートに移動をconsする」はProperである。

整理しよう。ルートに沿った移動という概念からルートの到着地同値関係 ≈ が定まり、ルートの同値類 R/≈ が定まる。同値類上でもwell-definedに定まる（＝Properな）操作である cons appなどを考える。これらはモノイドとして見れる。つまりキャリアがルートの同値類、操作がProperな操作(注：app,consは結合則を見たす）。空のルートの同値類が1となる。すると、この構造上でモノイド上の操作・性質に関する既存の成果の恩恵を受けることができる。