型クラス、ひどい
関数型プログラミングとオブジェクト指向について、何か書く、かも - 檜山正幸のキマイラ飼育記 関連で少し調べてみたら、
ウワーッ、随分とひどいことになってるんだな。
型述語解釈
http://www4.in.tum.de/~wenzelm/papers/constructive_classes.pdf :
axiomatic type classes in Isabelle merely account for the logical aspect as predicates over types,
https://wiki.haskell.org/Multi-parameter_type_class :
If you think of a single-parameter type class as a set of types, then a multi-parameter type class is a relation between types.
型述語解釈が変だが、型関係解釈はもはやトンチンカン。
「型全体の集合」がフィクショナル過ぎる。構文的には定義できなくもない。意味論的には、インスティチューションで言えば、Σ(Φ∈|Sig| : |Mod[Φ]| ) という集合(類)、Σは直和による総和。あるいはインデックス付き圏をグロタンディーク平坦化した圏の対象類とも言えるが、、、そこまで考えているとは思えない。
複パラメータ型クラス(多ソート指標上のセオリーだろう)、so-call"多重継承"の解釈がひどい。
用語、記法
用語や記法が誤解を誘導するよう(ミスリーディング)になっている。
- 型クラスを単にクラスと呼ぶ。
- メソッドとかメンバー関数とか呼んでるし。オブジェクト指向の人は自分のメンタルモデルに飛び付くだろう。
- クラスの継承とか拡張とか呼ぶ。例えば、「OrdクラスはEqクラスの拡張」とか、[OrdクラスはEqクラスを継承している」とか。
- 多重継承とかも言っているし。
- Eq a などが1引数の述語に見える。結果、型述語解釈が生じている。
- HasCasl (http://www.informatik.uni-bremen.de/~till/papers/hascasl.pdf)では、class D < C が使われている。Rubyの継承と同じ記法。これから D⊆C を連想したのだろう。
事例
class Eq a where (==) :: a -> a -> Bool
型クラスのHelloWorld。超越的イコールと計算可能なイコールがあるからだけど、その説明がウザい。演算子オーバーロードが絡んでウザい。
class (Eq a) => Ord a where (<), (<=), (>=), (>) :: a -> a -> Bool max, min :: a -> a -> a
なんだよ、コレ。全順序じゃねーか。部分順序にしろよ。公理が書けないから、指標側に「全順序じゃないと無意味な演算(operation, operator)」を入れて「それらしさ」を出しているんだな。
class Eq a => Ord a where compare :: a -> a -> Ordering (<), (<=), (>), (<=) :: a -> a -> Bool max, min :: a -> a -> a data Ordering = EQ | LT | GT
なんてのもあった。compareは全順序を強く「ほのめかす」ため。
「(Eq a) =>」の部分(括弧はなくてもいい)が制約だが、この構文が述語解釈に繋がったのかもしれない。あるいは逆に、述語解釈からの記法か。
Eq a => Ord a は,Ord クラスのインスタンスは Eq クラスのインスタンスでもなければならないという制約を表します。
型クラスによる制約は、
sum :: Num a => [a] -> a
のようにも使う。
so-called"多重継承"
複数のクラスを継承 (多重継承) する場合,class 宣言は次の例のように記述します。
- class (C a, D a) => E a where ...
型クラス制約が (型クラス1 型変数1, 型クラス2 型変数2, ...) => という形をしている。
- Eq a を、「型aはEqクラスである」「型aはEqクラスに属する」「型aはEqクラスにのインスタンスである」のような型述語解釈をしている。これがそもそもロクデモナイ。
- 複数型クラスの制約を、論理ANDのように解釈している。んなバカな!
- 忘却関手、あるいはキャリア(台)を対応させるキャリア関手(むしろ圏強制というべきか)を考える必要がある。
対処
型クラスのパラメータ概念がイイカゲン過ぎる。相対指標と部分固定指標の概念を使ってちゃんと定義する。基礎圏上の構造の圏の理論も必要。圏強制(忘却関手、キャリア関手)と、圏強制に関するセクション関手、指標とセオリーに関するさまざまな操作などを議論する必要がある。
インスティチューションをグロタンディーク平坦化した圏を“議論の宇宙”と考えるのはまーいい。宇宙の対象類がso-called"すべての型"なのはギリギリ合理化できる。が、部分圏の共通部分とか型の関係とかは完全にナンセンス。
曖昧さとフィクション(夢想)では話にならない。
[追記]ブルバキ流の「構造」を考えるとイイかもしれない。
- https://ncatlab.org/nlab/show/concrete+category
- https://ncatlab.org/nlab/show/structured+set
- https://ncatlab.org/nlab/show/stuff%2C+structure%2C+property
- https://ncatlab.org/nlab/show/free+functor
[/追記]