ECMAScript Modules（ESM）方式のモジュールシステムを前提に、ブラウザ向けJavaScriptプログラムを書いていたら奇妙な現象に遭遇しました。同一のJavaScriptモジュールが、ブラウザ内に二回ロードされていたのが原因でした。内容： クラスの定義とクラスの…

「二重圏を語るために」にて： 広く合意された約束はないので、二重圏を語るときは、ローカルルールをしっかり決めましょう。そうでないと、話がワヤクチャになります。 ローカルルールの事例を述べておきます。$`\newcommand{\twoto}{\Rightarrow} \newcomm…

二重圏を話題としたコミュニケーションは、なかなかに大変です。前もって約束を決めておかないと、話がワヤクチャになります。この記事でガイドラインを示します。$`\newcommand{\cat}[1]{ \mathcal{#1}} \newcommand{\mrm}[1]{ \mathrm{#1}} \newcommand{\I…

圏論、型理論（型付きラムダ計算含む）、論理は、カリー／ハワード／ランベック対応により、同種の構造（例えばデカルト閉圏）を扱っていると理解することが出来ます。しかし、用語法・記法はバラバラです。このバラバラさゆえに、対応関係を捉えられなかっ…

全称型／存在型のことを調べていて（「全称型？ 存在型？ ‥‥？？」参照）、気になったことがありました。some（論理記号 ∃）と any（論理記号 ∀）がほぼ同じ意味で使われていたり、用法が逆転していたりが起きていて、これは何でだろう？ と疑問を感じました…

昨日「まとめ」もしたので、この話題も一段落ですが、僕が言いたいことは； 「全称／存在」という言葉、「∀／∃」という記号を、型理論のなかで使うのはやめたほうがいいよ、ってことです。何も得することがなくて、弊害があります。「全称／存在」「∀／∃」を…

昨日・今日と、「全称型／存在型で困惑した」という話を書きました。 全称型？ 存在型？ ‥‥？？ アハハハハ（ちからない笑い）： 全称型／存在型 全称型／存在型 補遺 なんとなく情勢は見えてきたので、いったんまとめをしておきます。それと、存在型の一部…

「アハハハハ（ちからない笑い）： 全称型／存在型」で触れた Swift の existential any だけど； some というキーワードは既に使われていて、any にするしかなかった、という事情みたいです。Swift では、キーワードを付ける付けないに関わらず、プロトコル…

「全称型？ 存在型？ ‥‥？？」を書き終わった後で見つけた、Swift の存在型に関する記事、： Existential any in Swift explained with code examples Existential any allows you to define existential types in Swift by prefixing a type with the any k…

「多相関数を表す全称記号がしゃくに障るワケ」において、多相関数や依存型を表すときに使う全称記号を話題にしました。僕は全称記号反対派ですが、実際には全称記号が使われています。さてところで、「全称限量された型〈universally-quantified type〉」、…

「グリッド計算とコーナリング、そして二重圏」において、二重圏の2-射を描くペースティング図とストリング図を紹介しました。ストリング図では、縦方向ワイヤーは上から下、横方向ワイヤーは左から右で、常識的な書字方向に一致していて「あー、気持ちいい…

過去記事「フリーモナド 1： 自由で無料な木」において、フリーモナドの説明をしました。その過去記事の冒頭は次のようでした： 説明には、多くの場合、HaskellコードまたはHaskell風擬似コードが使われています。プログラミング言語としてのHaskellの利便性…

テレオロジー圏、コンパクト閉圏、トレース付きモノイド圏などのあいだの親族的関連性を調べたい、という動機から資料を探しているうちに、二重圏を使う手法に出会いました。そのことを前の記事に書きました。 グリッド計算とコーナリング、そして二重圏 モ…

ここ最近、テレオロジー圏、コンパクト閉圏、トレース付きモノイド圏などのあいだの親族的関連性に興味を持っています。なんか資料がないかな、と探していたら次の論文を見つけました。 Title: Cornering Optics Authors: Guillaume Boisseau, Chad Nester, …

「両側テレオロジー圏とプレオートマトン」にて： 両側テレオロジー圏は自己双対コンパクト閉圏とよく似た構造になります。テレオロジー圏とコンパクト閉圏には、親族的関連性があるのでしょう。 テレオロジー圏、コンパクト閉圏、トレース付きモノイド圏の…