フリーモナドの「フリー」は、「自由」の意味と共に「ただ〈for free〉」の意味もあります。「ただで手に入るモナド」ということです。しかし、この「ただで」は、「課金したらガチャをただで引けるよ」の「ただで」と同じで、事前のコストはかかっています。 事前のコストとは、「モナドがただで手に入る」環境を構築する手間です。この環境の説明／モナド入手法の説明には、多くの場合、HaskellコードまたはHaskell風擬似コードが使われています。プログラミング言語としてのHaskellの利便性が、当該メカニズムの圏論的内実を抽出するときにはむしろ仇になります。それで苦労している人へのアドバイス／解説がこの記事の内容です。 ここでは、（比較的普通の）圏論の概念・語法・記法により、モナドがただで手に入る状況をセットアップします。ここで行うセットアップが、「モナドをただで手に入れる」ための初期課金なのです
データベース・テーブルのある時点での状態は集合として捉えることができます。しかし、状態の変更である“削除・更新・挿入”を写像としてモデル化するのはうまくいかないようです。写像（集合圏の射）に拘らずに、別な見方をしたほうが良さそうです。 この記事では、変わり者／はぐれ者達に登場してもらって別な見方を提供します。$`\newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\lis}[1]{ \boldsymbol{#1} } \newcommand{\In}{\text{ in } } `$ 内容： テーブルスキーマとテーブル状態 テーブル状態の変更 単射スパン 単射スパンの圏 単射スパンと削除・更新・挿入 テーブル状態と状態変更の圏 テーブルスキーマとテーブル状態 以下、関係データベースを単にデータベースと言います。データベースのテーブルを作るには、事前に
Optics vs Lenses, Operationally (Update: I’ve given a talk about this blog post, which can be found here.) I’ve been thinking a lot about lenses and optics. They’re both abstract gadgets that model various sorts of bidirectional processes. They are found in machine learning, game theory, database systems, and so on. While optics are more general, it’s understood that they’re equivalent to lenses i
A recent paper suggested a new mathematical point of view on version control. I first found out about it from pijul, a new version control system (VCS) that is loosely inspired by that paper. But if you poke around the pijul home page, you won’t find many details about what makes it different from existing VCSes. So I did a bit of digging, and this series of blog posts is the result. In the first
プログラミングにおいて、レンズ〈lens〉と呼ばれる構造が使われる機会が増えているようです。古典的なレンズが幾つかの方向に一般化されていて、「レンズってなに？」と聞かれても答えにくい状況になっています。 一番簡単な（と僕が思っている）ストレージの例からはじめて、具象レンズを導入し、それらのあいだの関係を調べます。記述と計算にストリング図を使用します。 内容： 元祖レンズ 元祖レンズの圏 元祖レンズ達はホントに圏なのか？ Webサーバーモデル 具象レンズ 元祖レンズと具象レンズ おわりに シリーズ目次（リンク）： 圏論的レンズ 最初の一歩： ストリング図を中心に（この記事） 圏論的レンズ 2： 具象オプティック 圏論的レンズ 訂正と補足： 具象レンズ＝具象オプティック 圏論的レンズ 3： レンズ／オプティックのための描画法 圏論的レンズ 4： テレオロジー圏 圏論的レンズ 5： オプティック
去年〈2020年〉の10月に「多相関数と依存型をちゃんと理解しよう」という記事を書いたのですが、基本的な用語を間違っていました。[追記]いや、間違いでもないようです。この記事のコメント欄参照。[/追記] 記号 間違った 呼び方 1 正しい 呼び方 2 別な呼び方 $`\prod`$ 依存積型 依存指数型／依存関数型 パイ型 $`\sum`$ 依存和型 依存積型 シグマ型 $`\prod`$ だから積、$`\sum`$ だから和だろうと安直に思い込んでいて確認しなかったのです。ごめんなさい*1。[追記]「ごめんなさい」は、間違いかどうかの確認もちゃんとしてなかったことです。[/追記] 正しく別な言い方は、$`\prod_{x:X}F(x)`$ は非依存指数型（普通の指数型）の依存版だから依存指数型、$`\sum_{x:X}F(x)`$ は非依存積型（普通の積型）の依存版だから依存積型というネ
比較的最近（今年の9月）、多相関数の記事を書きました。「多相関数」「総称関数」という言葉は知っていても、理解があやふやな人もいそうです。基本的なところを復習しましょう。話を明確にするために、少し圏論を使います。 [さらに追記]下の追記における「間違いです」が間違いだったようです。用語法の流儀が複数あるので、どっちも許容でした。追記内の表は、2つの用語法の対照表になります。[/さらに追記] [追記] この記事内で使っている言葉「依存積型」と「依存和型」は間違いです。申し訳ありません。正しい呼び名は次のとおりです。 記号 間違った 呼び方 1 正しい 呼び方 2 別な呼び方 依存積型 依存指数型／依存関数型 パイ型 依存和型 依存積型 シグマ型 「依存型と総称型の圏論的解釈」の冒頭で釈明(?)説明を書いています。 間違いも記録として残しておく方針なので、お手数ですが、本文内の「依存積型」を「依
2020年9月に書いた一連の記事があります。 蒸し返し： アドホック多相 vs パラメトリック多相 多相関数の「パラメトリック性 vs 満足性」 多相関数と型クラス これらは多相関数に関する記事です。昨日の記事も多相関数を扱っています。 多相関数と依存型をちゃんと理解しよう 9月のシリーズ記事と昨日の記事では、多相関数の定義が違います。これは混乱を招くかも知れないので、この記事で追加の説明をしておきます。 内容： 定義はTPO依存 関手性と自然性 多相関数の少し一般的な定義 9月の記事での多相関数 昨日の記事での多相関数 パラメトリック性 定義はTPO依存 同じ言葉を複数の記事で使い、それらの定義がズレていたのですが、僕はそれが悪いとは思っていません。ただ、関連性が強い記事で異なる定義を採用していると混乱を招くリスクがあるので、断り書きはするべきでしょう。 言葉と定義に関する僕のスタンスは
面白い偶然が起きることがあります。 ごく最近、次の記事を書きました。 2020年9月7日 蒸し返し： アドホック多相 vs パラメトリック多相 2020年9月8日 多相関数の「パラメトリック性 vs 満足性」 そして9月8日と9月9日（昨日）、4年前の記事にkhibinoさんからコメントをいただきました。 2016年9月28日 入門的ではない型クラスの話：Haskellの型クラスがぁ (´^｀;) これらの話題は無関係じゃないんですよね。奇遇。 4年前の記事の背景として、僕には“指標とモデルの圏”の話をしたい動機がありました。それに対して、Haskellの型クラスは用途が制限され過ぎていて気に入らない、といったことを書きました。今思えば、「気に入らない」という感情が先行していて、「君の型クラス vs ワシの型クラス」みたいになっていて、「不毛」とまでは言わないまでも、薄毛な（不毛に近い）議
一年ほど前に「「アドホック多相 vs パラメトリック多相」をマジメに考えてはいけない」という記事を書きました。多相性を二種類に分類できるわけではなくて、パラメトリック性（あるいはアドホック性）はしょせん程度問題だ、という話です。「関数定義がひとつで済む多相はパラメトリック多相」なんていう曖昧な定義はあまり意味がありません。 しょせん程度問題だとすると、その“程度”を測って比較したいとは思います。「「アドホック多相 vs パラメトリック多相」をマジメに考えてはいけない // それでもマジメに考えたいのなら」に次のように書きました。 多相関数を自然変換として定式化して、自然変換のあいだの関係をアドホック性を計る尺度に用います。実際、いくつかの方法で自然変換のあいだの順序を定義できます。その順序は、アドホック性の程度とみなせます。 上記の方法でパラメトリック性（アドホック性）を実際に測って比較し
とあるソフトウェア的な動機から、圏論的な代数系を構成してみます。この代数系は、通常の圏〈ordinary category〉とは違い、横結合、縦結合、モノイド積の3つの演算を持ちます。通常の圏は結合だけしか持たないし、モノイド圏は結合とモノイド積しか持ちません。では、モノイド2-圏〈monoidal 2-category〉*1かというと、そうではありません。モノイド二重圏〈monoidal double category〉*2かというと、そうでもありません。 横結合は、複圏〈オペラッド〉の結合であり、縦結合とモノイド積は、複圏の結合と整合する形に定義されます。こういう構造を何と呼ぶのかな？ とりあえず「圏上の複圏〈オペラッド〉」と呼んでおきます（つまんねー呼び名）。複圏とオペラッドは同じものです。複圏とオペラッドを区別する人もいます*3が、僕は同義語として使います。以下、複圏＝オペラッド
サイト〈site〉とは、圏であり、その対象が位相空間のように扱える構造を備えたものです。“位相を持った圏”とも言われます。“サイト＝位相を持った圏”はグロタンディークのアイディアですが、本来のグロタンディーク位相以外に、様々な変種があるので、それらを総称してグロタンディーク流位相〈topology à la Grothendieck〉と呼ぶことにします。すると、「サイト ＝ なんらかのグロタンディーク流位相を持つ圏」となります。 サイトについて、いくつかの記事を書きました。 ビッグサイト微分幾何と自然変換の上付き添字 サイトと層の大きさやら作り方やら ビッグサイトから巨大サイトへ 三番目の記事で巨大サイト〈giant site〉と呼んだタイプのサイトを使っている例を検索してみたので、それらを眺めた感想を記しておきます。 内容： 巨大サイトを使っている例 被覆系による位相の定義 単元被覆系
去年の秋から半年間 3時間×6回 のコースとして「ゲーデルの不完全性定理」のセミナーをやりました。今年も9月から同様のコースをやる予定です。ガイダンス回（第0回）が 8月4日(日曜) 18時 からあります。 案内ページ： http://romanticmathnight.org/972 ガイダンス回は無料です。興味のあるかたは是非おこしください。 また、並行して圏論のコースも設けます。「圏論」セミナーのガイダンス回は 8月18日(日曜) 18時 からです。 案内ページ： http://romanticmathnight.org/979 こちらもよろしくお願いします。 去年秋から今年春までやった前回の「ゲーデルの不完全性定理」コースでは、予定通り「証明も、否定の証明もできない命題の存在」を示すことができました。が、時間的にイッパイイッパイでした。なので、1回増やして7回を予定しています。 計
先週土曜日（2019年4月20日）、タケヲさん（id:bonotake）から古い記事にコメントをいただきました。 朗報です！ Spivakのオンラインコースが無料で公開されました！ https://ocw.mit.edu/courses/mathematics/18-s097-applied-category-theory-january-iap-2019/index.htm とのことです。 コメントが付けられた古い記事は： 2013-05-24 デイヴィッド・スピヴァックを紹介する2つのニュース デイヴィッド・スピヴァック〈David I. Spivak〉は、関手データモデル／応用圏論で有名なMITの先生です。スピヴァックに関連する記事を幾つか挙げると： 2013-01-28 デイヴィッド・スピヴァックはデータベース界の革命児か -- 関手的データモデル 2013-03-04 スピヴァッ
iOSDC Japan 2018 (Sep 2, 2018) https://iosdc.jp/2018/ https://fortee.jp/iosdc-japan-2018/proposal/45b858e0-753c-4387-9210-5837cff6da7a iOSDC Jap…
「カン拡張のために、柱の絵を描く」にて： 特にシリーズ記事とかにしませんが、関連する幾つかの記事達が、全体としてカン拡張の説明になればいいな、というゆるい計画はあります。 というわけですが、カン拡張を知ったら何かいいことがあるんでしょうか？ 内容： 圏論内部からの動機 関手データモデルとデータ移行関手 型クラスとモデル 相対モナド プログラム最適化 おわりに 圏論内部からの動機 カン拡張というと、マックレーンの有名な言葉： All Concepts are Kan Extensions があります。圏論に出現するすべての概念はカン拡張で説明できる、ということです。ちょっと大げさな気がしなくもないですが、標準的・典型的な圏論の概念がカン拡張に包摂されるのは事実です。 極限／余極限は、圏論の重要な道具ですが、それぞれ右カン拡張／左カン拡張の特別な場合になります。つまり、「極限はカン拡張」（Li
「全称記号の導入規則について考える」の続編として、存在記号の除去規則について考えます。 存在記号の除去規則の背景は比較的に簡単な事実です。にも関わらず、記号を換えたり書き方を縦にしたり横にしたりのどうでもいいワチャワチャが事情を見えにくくしています。この記事によって、ワチャワチャな作業（記法のあいだの翻訳）に慣れて、その“どうでもよさ”（記法が変わっても内実は変わらないこと）を感じていただければ幸いです。 内容： 存在記号の除去規則 限量随伴性 引き戻しと存在限量子の随伴性 随伴性を証明に利用する 随伴性からサイド証明へ メタ循環構造 存在記号の除去規則 標準的な自然演繹における「存在記号の除去規則」は次の形に書かれます。 P(a) : : ∃x.P Q -------------[∃除去] Q僕は、自然演繹に愚痴を言い、悪態をついてます（「自然演繹はちっとも自然じゃない -- 圏論による
米田埋め込みはやっぱり役に立ちますね。米田埋め込みを利用するときに便利なツールを幾つか紹介します。それらのツール達は： 関手に使うラムダ記法 米田の星 (-)米, (-)米 関手・自然変換のテンソル積 マルチ米田埋め込みのドット記法 内容： 過去の事例： CPSと確率変数 困った時の米田頼み、もうひとつの例 米田埋め込み ラムダ記法と米田の星 超巨大圏CATと直積 関手・自然変換のテンソル積 マルチ米田埋め込みとテンソル積 前層の圏とマルチ米田埋め込み おわりに 過去の事例： CPSと確率変数 プログラミングにおいて、継続（continuation）という不思議な概念が登場します。継続を用いたプログラミング技法として、継続渡し方式（CPS; Continuation Passing Style）という何だかヨクワカラナイやり方があります。 継続／継続渡し方式に関わる不可解さは、米田埋め込み
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く