このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

パイプライン指向JSON処理プログラミング言語 jq

jq(https://stedolan.github.io/jq/)の紹介では、「JSON処理のワンライナー〈一行野郎〉としてめちゃくちゃ便利!」とアピールするのが定番です。もちろんそれは本当で、「めちゃくちゃ便利!」です。が、実は jq は、ワンライナー記述にとどまらない、か…

JavaScriptモジュールは二回ロードされる可能性がある

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

二重圏の語法・記法、ローカルルール事例

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

二重圏を語るために

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

コンテキスト、判断、指標、シーケントなどのゴチャゴチャを整理

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

型クラス述語とイプシロン型

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

全称型/存在型: 代替案

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

全称型/存在型: まとめと Models-as-Types

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

全称型/存在型 補遺

「アハハハハ(ちからない笑い): 全称型/存在型」で触れた 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, …