PS

Haskell

String diagram による Applicative functor まとめ

Applicative Functors with Strings Applicative functor の記事をまとめました。 strcat/strapp.pdf at master · okomok/strcat · GitHub

Applicative functors in string diagrams rev.2

(役に立つような立たないような・・・) Comma operator Evaluation operator Applicative functors To monoidal functors とすると LiftAn 以上から直ちに: 参考文献 Applicative functors in String diagrams - PS

Reader monad transformers in string diagrams

(図にしてみれば怖くない・・・かも) Reader monad transformers Reader monads 上図の太枠を取り除いたもの。 参考文献 transformers: Concrete functor and monad transformers | Hackage scala - Is it just a coincidence that Kleisli, ReaderT, and Reade…

Haskell-monads in string diagrams rev.2

(・・・といっても Monads in string diagrams - PS にするしかなさそう) Haskell-monads To monads とすると 参考文献 Haskell-monad - PS

Cofree comonads in String diagrams

Cofree comonad Data *1 Implementations 再帰的に定義する(合わせ鏡のように)。 Functions 参考文献 Control.Comonad.Cofree *1:iso は真四角にした

Store comonads in String diagrams

Store(Costate) comonad Functions 参考文献 haskell - What is the Store comonad? - Stack Overflow

Haskell-comonads in String diagrams

@deprecated @todo ・・・と言っても Haskell-monads in String diagrams - PS を上下さかさまにしただけ。*1 Haskell-comonad Laws Functions 参考文献 https://hackage.haskell.org/package/comonad/docs/Control-Comonad.html All About Comonads (Part 1).p…

String diagram のすすめ

こちらは Haskell Advent Calendar 2015 - Qiita の 20 日目の記事です。 前の日・・・Hakyllでブログを作る(実践編) - Wake up! Good night* 次の日・・・「第2期 H本読書会 in 秋葉原」を終えて #readhbon #haskell - セカイノカタチ String diagram String diag…

Arrows in String diagrams

Arrow laws (・・・やっぱりつらいので左右逆にならないようにする) 以下、水平方向は考えないで、垂直方向のみ 1-category の composition とする。 メモ 「1.」と「 2.」は の functoriality。 「6.」は の についての extranaturality。 ただし、naturality …

Free monads in String diagrams

(・・・というのは少し嘘かもしれない) Catamorphisms Free monad - PS の より・・・ Free monad 参考文献 Haskell for all: Why free monads matter Control.Monad.Free

Traversable functors in String diagrams

Identity functor Constant functor Traversable functor Traversable functor laws Traversable functor - PS より・・・ foldMap/foldr 参考文献 Foldable and Traversable - Jakub Arnold Blog

Applicative functors in String diagrams

@deprecated 代わりに Applicative functors in string diagrams rev.2 - PS を参照。 以下、curry/uncurry したものは区別にしないことにする。 (右足を上げたり下げたりするだけ) Applicative functor Applicative functor laws Monoidal functors via app…

Identity monads in String diagrams

Identity monad 参考文献 All About Monads - HaskellWiki

List monads in String diagrams

Concatenation List monad 参考文献 All About Monads - HaskellWiki

Error monads in String diagrams

Error monad Maybe monad の を にしただけ。 throw/catch 参考文献 All About Monads - HaskellWiki haskell - Is there no standard (Either a) monad instance? - Stack Overflow

Maybe monads in String diagrams

Universality of coproducts Merge morphism Initializing morphism (とはたぶん言わない) Monoidal category with finite coproducts Cocartesian monoidal category ともいう。 命題 Maybe monad 参考文献 [1401.7220] Category Theory Using String Diagr…

Continuation monads in String diagrams

Evaluation Continuation monad Flip bijection を使って・・・ callCC ・・・かえって分かりにくい。 参考文献 All About Monads - HaskellWiki

Writer monads in String diagrams

Writer monad 参考文献 All About Monads - HaskellWiki

Reader monads in String diagrams

@deprecated 代わりに Reader monad transformers in string diagrams - PS を参照。 Constant morphism Reader monad を たちにばらまいている。 参考文献 All About Monads - HaskellWiki

State monads in String diagrams

Monoidal category にて・・・ Diagonal morphism Naturality Terminating morphism (とはたぶん呼ばない) Naturality これらは、より一般には cartesian monoidal category のときに作れる。 State monad get/put 参考文献 [1203.0202] Pictures of Processes:…

Haskell-monads in String diagrams

@deprecated 代わりに Haskell-monads in string diagrams rev.2 - PS を参照。 Monoidal category にて・・・ Haskell-monad の flip 版を使った方が分かりやすいみたい。*1 Haskell-monad laws Kleisli composition Haskell-monad @deprecated Haskell-monad …

Adjunction からの monad transformer

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

Continuation monad

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

Reader monad

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

Writer monad

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: …

fold/build fusion

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

GADTs

複雑な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: をこっそり使って *…

Inductive family of types

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

Traversable functor

記法 Category of applicative functors - PS Traversable functor その1 functor: natural transformation: *1 のペアで (unitality) (linearity) を満たすもの。 Traversable functor その2 functor: natural transformation: *2 のペアで (identity) (com…

Category of applicative functors

Applicative morphism 二つのapplicative functor: の間のmorphismを を満たすnatural transformation: とする。 Monoidal morphism Applicative functorはmonoidal endofunctorで表現できたので、同様に 二つのmonoidal endofunctor on monoidal or : の間…

Monadはapplicative

命題 Haskell-monad: について、 とすると、 は、applicative。 系 monoidal category: monad: について、 とすると、 はmonoidal endofunctor on になる(と思う)。 参考文献 haskell - How to show that a monad is a functor and an applicative functor? …

Haskell-monad

Haskell-monad Monad laws - HaskellWikiより、Haskell-monad: とは、 endofunctor: natural transformation: *1 関数族: で、left identity則、right identity則、associativity則、および *2 を満たすものとする。 命題 MonadとHaskell-monadは同値。 Endo…

Functor則

Free theoremのもと、いわゆるfunctor則は一つでいいらしい。 命題 における型族: について、 を満たす関数族: が存在するならば、 証明(の試み) 関数: のrelationによる表現: について、relation: を定義できて*1、 のparametricity: が得られる。 参考文献…

fmapの一意性

命題 Functor: について、 を満たす関数族: が存在するならば、 証明 Free theoremにより、 は、 についてfreely naturalなので vs. Applicative \f -> \x -> pure f <*> x は、functorialなので、上記の命題より fmap f x = pure f <*> x 参考文献 haskell …

Applicative functor

記法 とする。 特に、 のとき、free theoremを想定すれば、naturalityの要件は自明となる。 Monoidal sets は、productとsingleton setにより、monoidal category: を成す。 Monoidal endofunctor over sets Monoidal endofunctor: とは、 endofunctor: natu…

Operational monad

Free monad Free monads are free - PSにより Free functor Free functor object - PSにより Operational monad とすると、Composition of adjunctions - PSにより は、discrete diagram から作った一番シンプルなmonad。 参考文献 Adjoint functors - Wikip…

Element-wise law

Element-free law Monad morphism: の要件は、 *1 *2 であった。 Element-wise law 一方、Control.Monad.Morphでは、 morph . (f >=> g) = morph . f >=> morph . g morph . return = return となっていて、あれ?と思ってしまったが、 これはElement - PSの…

Monad transformer

Inhabited set 空でない集合のこと。 Pointed set 集合とその要素のペア: からなる代数的構造。このとき、 はinhabited。 Pointed object category: terminal -object: について、 -object: -morphism: のペア(からなる代数的構造) をpointed objectという。…

Codensity monad

Codensity monad Functor: について、right Kan extension of along : が存在するならば、 *1 は、monadを成す。このmonadをcodensity monad of という。 Adjunctionからのcodensity monad 特に、 がleft adjoint: を持つとき、Adjunction lifting - PSによ…

(Co)Yoneda reduction for free

(Co)Yoneda reduction Yoneda lemmaの(co)endによる表現: を、(co)Yoneda redunctionという(と思う)。 (Co)Yoneda reduction for free (Co)Ends for free - PSとより、 Functor.(Co)Yoneda 上をHaskellで実装したのが、kan-extenstionsの module Data.Functo…

(Co)Ends for free

Free dinaturalityのもと、difunctor について・・・ Ends for free Limits for free - PSと同様にして、projection: は、 のending wedgeになる: このending wedgeは、identity function: と本質的に等しい。 Coends for free Colimits for free - PSと同様に…

Free theorem vs. dinaturality

Free dinaturality Free theoremはdinaturalityについても有効である(らしい)。 命題 Free naturalityが成立するならば、free dinaturalityも成立する。 以下、非常に怪しい証明・・・ 証明 Twisted arrow category - PSによる、 を利用する。詳しくは、morphis…

Colimits for free

以下、Limits for free - PSのdual。 Cocones for free Functor のcoproduct: について、function: を のcocone for freeと勝手に呼ぶことにする。 これは、以下のcategoryにより のcoconeと本質的に等しい。 Cocone category for free なる をcocone for fr…

Limits for free

以下、category と (的なもの) にて、free naturalityが成立するとする。 Cones for free Functor のproduct: について、function: を のcone for freeと勝手に呼ぶことにする。 これは、以下のcategoryにより のconeと本質的に等しい。 Cone category for f…

Free theorem vs. existential

Free theorem ある種の体系では、naturalityが常に成立するという(ことを含む)定理。 このnaturalityをfree naturalityと勝手に呼ぶことにする。 命題 Functor について、product: に関してfreely naturalならば、coproduct: に関してもfreely natural。 証…

Adjunctionからのmonad

Associated monad with an adjunction Adjunction : left adjoint right adjoint counit unit について、 とすると、 endofunctor unit multiplication *1 はmonadになる。 State monads from currying 特に、 のとき、adjunction: から上記の方法で作ったmo…

Yoneda functor

Haskell(kan-extensions)のYoneda functor: newtype Yoneda f a = Yoneda { runYoneda :: forall b. (a -> b) -> f b } を攻略する試み。 Yoneda lemmaのdual版 Category Theory (Oxford Logic Guides) のyoneda lemmaから を使えば、dual版を作ることができ…

Theorems for free

CoYoneda data CoYoneda f a = forall b. CoYoneda (b -> a) (f b) は、圏論っぽくかくと、morphism族: のこと Parametricity theorem Parametricity theoremにより、なんやかんやで はnaturalになる(らしい)。 特に、 についてのnaturalityにより

Kind generalization

Type-level generics Scalaでは、type-level generics(勝手にそう呼んでいた)が動かないのだが、 おおもとはSI-3443にあるようだ。たとえば trait TypeFunction { type Domain type Codomain type apply[x

Inductive type

Fixed point, 不動点 関数 について、fixed pointとは、 を満たす のこと。これをendofunctorに拡張する。 Endofunctor について、 fixed pointとは、 を満たす のこと。 Initial algebra のinitial objectのこと。 Lambek's theorem initial algebraはfixed…