俺様 scala.vim を作成中に出くわした Scala の syntax の(知らなくてよさそうな)仕様について･･･ Unicode escape \u1234のような形は tokenize に先立ち unicode文字にエスケープされる: val \u0061b = 3 // val ab = 3 uは何個ついてもok: val \uuuuuu0061…

型推論クイズ - PS とはかけ離れたかもしれない怪しいレポート。 準備 以下の記事は、Scala 2.11.4 および Scala言語仕様 (pdf) (以下、SLS) の June 11, 2014 版を使用しています。また、scala.Singleton - PS に誤りがあり訂正しているので合わせてご覧く…

この投稿は Scala Advent Calendar 2014 - Qiita の24日目の記事です。 前の日の記事: Scala - spray-routingにPlay2ライクなコントローラを導入する - Qiita 次の日の記事: L'Architecture systèmatique [JP]: Patterns on Scala この記事についてのレポー…

記法 2-category: について と書くことにする。 2-category laws n-Category - PS の定義により (associativity) (left unitality) (right unitality) さらに、 の Bifunctoriality - PS より (interchange) (sliding) が成立する。 2-category of small cat…

記法 Under category (Coslice category) *1 Error monad Functor: と forgetful functor: について *2 となるが、この adjunction の associated monad が error monad。 Error monad transformer Adjunction からの monad transformer - PS から functor: …

戦略 任意の monad: について Universal associated adjunctions - PS より少なくとも二通りの -associated adjunction: が作れたので Adjunction からの monad transformer - PS より functor: を作ることが出来る。 問題点 上記の functor の domain が に…

(と呼ぶかは分からない) Kan extension の族から ある functor: について、right kan extension along の族: つまり -terminal morphism の族が存在すれば、Pointwise construction of adjoints - PS より となるような functor: を作れる。 Kan extension …

命題 bifunctor: homset-adjunction の族: について は natural なる bifunctor: がただ一つ存在する。 証明 Conjugate - PS の命題と Bifunctor lemma - PS による。 参考文献 Categories for the Working Mathematician (Graduate Texts in Mathematics)

Adjunction from to Adjunction: を便宜上 adjunction from to と呼ぶことにする: Conjugate Homset-adjunction from to : について を commute にする natural transformation のペア: を conjugate という。 命題 Adjunction from to : および natural tra…

Lifted adjuncts Adjunction: について、Adjunction lifting - PS により natural bijection: が存在するのであった。 命題 上記の adjunction について が comonad: になっているならば は monad になる。 Dual が monad ならば は comonad。 参考文献 Mona…

Adjunctionからのmonad - PS を一般化する。 Adjunction-associated monoidal functor (と呼んでいいと思う) Adjunction: について は monoidal functor: になる。 Monad sandwich Monoid lifting により functor: を作ることが出来る。 State monad transfo…

0-category 集合のこと。その要素を object と言うことにする。 0-funtor 関数のこと。 n-category 再帰的に定義する。-category とは class: (objects) -category の族: -functor の族: (composition) -functor の族: (units) からなる代数的構造で (associ…

はてなブログのMarkdownモードで数式[tex: ]を書くときのバッドノウハウ 問題点 Markdownがパースしたあと、texがパースされているようなので、例えば [tex: a*b*c] が、Markdownのemphasisと解釈されて [tex: abc] となってしまう。 回避策 <div></div>で[tex: ]を囲む…

Product category Product category - PS より、product category: とは ･･･のような category であった。 Bifunctor Domain が product category の functor: のこと。*1 記法 Bifunctoriality Bifunctor の functoriality は 中置記法では 参考文献 Handbo…

Association between monads and adjunctions monad: adjunction: について を満たすとき、互いに associated というのであった。 Identity monad identity functor: identity natural transformation: は monad になる。 Trivial adjunction さらに とする…

Opposite monoidal category Monoidal category: について *1 は、monoidal categoryになる(と思う)ので と書くことにする。 *2 Comonoid object そのopposite monoidal categoryにおけるmonoid objectのこと。 Trivial comonoid object Monoidal category w…

Opposite morphism in in *1 命題 is not a covariant functor. Opposite functor Functor: について、opposite functor: を定義できる。これにより はfunctorial。 Opposite natural transformation Natural transformation: について、opposite natural tr…

Monoid lifting Monoidal functors send monoids to monoids: Monoidal functor: について、functor: *1 を定義できる。 Monads from monoids 特に、 のcodomainがmonoidal category of endofunctors: のとき *2 Writer monad とすると、monoidal functor: …

いわゆるgetter/setterの圏論による表現。 Associated (co)monad with an adjunction Adjunctionからのmonad - PSより、adjunction: について はmonadに、 はcomonadになる。 EM category for a (co)monad Eilenberg-Moore adjunction - PSより、monad: につ…

Functorが絡んだときのparametricityの求め方。 以下、 において･･･ Image Relation Graph Relation lifting Endofunctor: に対応する、relation間のmapping*1を と定義する。 命題 特に、関数: に対応するrelation: について、 証明 *2 参考文献 Theorems f…

Algebraically compact category 任意のendofunctorのinitial algebraとterminal coalgebraが存在し、互いにinverseとなるcategoryのこと。 等がそうらしい。 命題 endofunctor: initial algebra: terminal coalgebra: algebra: coalgebra: について なる -m…

命題 Initial algebraの族: について *1 なるfunctor: がただ一つ存在する。 証明 Fusion law vs. Parameterized algebra *2 参考文献 Theory and Practice of Fusion(pdf) *1:naturalityはevaluation functorによる *2:Initial algebras with parameters - …

いわゆるif文の圏論的表現。 Distributive category has finite products: has finite coproducts: なるcategory のこと。 以下、distributive category について･･･ Predicate Guard If expression 参考文献 thesis.pdf

命題 endofunctor: forgetful functor: について、initial algebra: が存在するならば、そのcatamorphimの族: は、mediatorを とする limiting cone of になる: (fold/build fusion) 参考文献 Initial algebra semantics is enough

命題 functor: initial algebraの族: について なるfunctor: がただ一つ存在する。 証明 参考文献 thesis.pdf

Endofunctor: について･･･ Lambek's lemma Every initial algebra is an isomorphism: *1 系 initial algebra: -morphism: *2 について なる -morphism: がただ一つ存在する。 参考文献 art08_geuvers_poll.pdf initial algebra of an endofunctor in nLab *…

複雑なGADTsはYoneda lemmaを使ってInductive family of types - PSにもっていける、ということらしい。 例 data Z data S n data IntList n where Nil :: IntList Z Cons :: Int -> IntList m -> IntList (S m) Covariant Yoneda lemma: をこっそり使って *…

(Primitive recursive functionの圏論による表現) *1 命題 endofunctor: initial algebra: -morphism: について なる -morphism: (paramorphism) がただ一つ存在する。 証明 参考文献 art08_geuvers_poll.pdf *1:かえって分かりやすい(と思う)

Co-Yoneda lemma - PS を( dinaturality でなく普通の) naturality の世界で表現するとこうなるらしい。 Contravariant Yoneda embedding *1 命題 Every set-valued functor is a colimit of representables: functor: forgetful functor: について 具体的に…

(Higher inductive types･･･と言いたいがそれはまた別物らしい。) Family of inductive types たとえば、Free monad - PS: は、 をfixed pointとするinitial algebraが族になっているだけ(で問題ない)。 Inductive family of types 一方、free applicativeに…