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

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

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

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

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

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

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

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

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

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

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

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

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版を作ることができ…

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

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

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

vs. dependent types 一般に、dependent type family: を実装するのは難しい(らしい)。一方、singleton type family: の実装はなんとかなるので、 を満たすことから、 という関係のもと、 Promotion Haskellはすごいことになっており というデータ型があると…

@Deprecated Existential types (集合論の)Unionは、 という定義だったが、型理論においては、このような型は作れず *1 という感じの定義(disjoint union)になっている。 をどこかから探してくれたりはしない。 Scalaでは、(disjointでない)union風の定義に…