モジュール・システム

圏論

とりあえず、MLのモジュール・システムでもfunctorという用語が使われてること、そいつが何か圏論に由来するらしいことは分かった。OcamlのmoduleとMLのmoduleって多分一緒なんかな〜


MLモジュールシステムを圏論的に理解しようとしてる論文

    A Category-Theoretic Account of Program Modules
    Fibrations, Logical Predicates and Indeterminates


後者は200ページ以上ある上に、ほとんど圏論の話のみという。いや、前者も短いけどほぼ圏論の話か。しかし、長い論文書くヤツはそれだけで悪。つか、indexed categoryとかfibred categoryとか全然わかんね〜。indexed categoryからfibred category作れることすら初めて知ったよ。基本的な概念の対応は多分、Bをラムダ計算とかのモデルになるcartesian closed categoryとして、indexed category C:B^{op}->CatからGrothendieck構成で、fibred categoryG(C)->Bがつくれて、このG(C)がモジュールの圏になるらしい。さて、意味が分からんが。あと、だから何?という感がひしひしと


後者の論文6.3.1節に載ってるMLモジュールの例

signature Order =
 sig
  type t;
  val le: t*t -> bool
end;

structure IntOrder: Order
  struct 
   type int;
   fun le(m,n) = m <= n //in =< nってなってるけど誤植?それとも、なんか意味が?
end;

functor Dual(structure O1:Order):Order =
  struct
   type t = O1.t;
   fun le(x,y) = O1.le(y,x)
end;

MLとか全然知らないけど、Haskellでは、

class Order t where
 le::(t,t)->Bool

instance Order Int where
 le(m,n) = (m<=n)

data Dual t = Dual t
instance (Order t) => Order (Dual t) where
 le(Dual m,Dual n) = le(n,m)

とか書くとこなんでないかな。Haskellの方が短いッ！というのはいいんだけど、で、このDualというのがG(C)の射と見なすことができるらしい。理屈追ってないけど(ダメ)。てか関手じゃないのかよヽ(｀Д´)ノ

より手軽っぽいのは
A proposed categorical semantics for ML modules
読んでないけど


てかまあ、MLのmoduleはいいんだけど、主にHaskellの型クラスについてはどうなのかというのは宿題。いや一緒っぽいよな〜