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風の定義に…

Sequence, 列 自然数を添字とする族: のこと。 Polynomial, 多項式 Commutative ring について、polynomial over とは、以下を満たすsequence のこと。 このとき、 を、適当にvariable を選んで あるいは と書く。それぞれの をcoefficientという。新たな族…

Finite set 個の元をもつ集合は、全て本質的に等しいので、一つ選んで と書く。特に、 n-tuple 集合 と について、-tuple とは、 の元: のこと。 特に、 つまり、-tuple は、定義により のことだが、特別に、 と書く。 Free monoid 集合 について、monoid を…

Endofunctor Domainとcodomainが同じfunctorのこと。 F-algebra 任意のendofunctor について、 -algebraとは、以下から成る代数的構造 である。 -object: (carrier) -morphism: F-algebra category 任意のendofunctor について、 -algebra category: を次の…

Kind Type familyの集合: を から へのkindという(と思う)。 Higher kind 特に、もkindの場合、higher kindという。 Box Haskellでは全てのkindの集合をboxというらしい。 これを と書くことにする。 命題 ただし、 はsingleton setとする。 これにより、型…

Abstract type member Scalaでは、abstract type memberとtype projectionを使ってtype family を作ることができる。 object PathDepType { trait K { type A // abstract type member } trait a extends K { override type A = Int } trait b extends K { o…

Type family 型族のこと。 つまり、全ての型の集合を とすると なる関数のこと。族の記法を使うと 特に断らない場合は、添字集合 は の部分集合とする。 Dependent type family Dependent type familyとは、添字集合が型になっているtype familyのこと。 つ…

Scala category と同じような感じで、scala category*1: を次のようにして定義できる: scalazが想定していると思われるcategory*2。 厳密に分析するのは止めたほうがよさそう。 参考文献 scalaz/scalaz · GitHub *1:こういう用語があるのかは不明･･･ *2:標準…

(定義に再び挑戦･･･) Terminal object Category について、terminal object: とは、以下を満たす -object のこと。 (universality) このただ一つ存在する を (mediating morphism) で参照することにする。 Terminal objectはunique up to isomorphismなので…

Monoid as category Monoid について、monoid as category*1: を次のように定義できる: *2 Monoidもcategoryだった、ということ。 とは全然違うので注意。 参考文献 Monoid - Wikipedia, the free encyclopedia *1:固有名詞があるのか分からず *2:元は の一…

Kleisli category Monad について、kleisli category: を次のように定義できる。 Monadはcategoryだった、ということ。 参考文献 Kleisli category - Wikipedia, the free encyclopedia Kleisli category in nLab

Haskell category Haskell category*1: を次のように定義できる: 厳密にはundefined :: forall a. aの扱いが難しいらしい。 Bottom ならば、選択公理により ここで をbottom typeと言い*2、その中から元を一つ選んで (bottom) とする。 公理的集合論では、bo…

Monad Monadとは以下から成る代数的構造 である: functor natural transformation (unit) natural transformation (multiplication) これらは以下の要件を満たさなくてはならない。 (associativity) (unitality) 参考文献 Monad (category theory) - Wikiped…

Adjunction: の同値な定義がいろいろある。 Hom-set adjunction 以下から成る代数的構造: functor (left adjoint) functor (right adjoint) natural isomorphism 命題 はnatural と は共にnatural Counit-unit adjunction 以下から成る代数的構造: functor (…

Comma category Functor: について、comma category: を次のように定義できる: 命題 Morphism category identity functor: を使って と定義できる。 Over category, slice category Category と -object について、 constant functor: を使った をcategory o…

The 1 Category を次のように定義できる: 命題 Constant functor Category と -object について、constant functor を次のように定義できる: Constant natural transformation 任意のcategory と -morphism について、constant natural transformation: を定…

Cartesian category @deprecated Category について、以下を満たすとき、cartesian category*1という。 任意のdiscrete diagram in : について、product: が存在する。 Product morphism 二つのproduct: 二つのmorphism: について、 はconeであるから、produ…

Identity natural transformation Functor について、identity natural transformation: を定義できる。 Composite natural transformation 二つのnatural transformation: について、composite natural transformationを次のように定義できる: Functor cate…