@Deprecated Skeletal category なるcategory のこと。つまり、isomorphicなobjectは等しい、というcategory。 Posetal category Skeletalなpreorder categoryのこと。Posetと本質的に等しい。 命題 参考文献 Posetal category - Wikipedia, the free encycl…

Element Category において -morphism のことを、element of with stage という。 ･･･とは書かないようである。書いていいらしい。 Functionはfamily、functorはdiagram、morphismはelementということ･･･か？ Global element Terminal objectをstageとするel…

Group object Has finite productsなcategory において、group objectとは、 -object -morphism -morphism -morhpism から成る代数的構造のこと。(要件略) Groupのcarrierを、集合からobjectへ一般化したということ。 同様にして、monoidを一般化したものをm…

Equivalence relation Reflexiveかつsymmetricかつtransitiveなbinary relationのこと。 Trivial equivalence relation は、equivalence relation on 。 Equivalence class Equivalence relation on : について、 を、equivalence class of modulo といい、 …

Pullback Productは、diagram: のlimitだったが、それにちょっと加えたdiagram: のlimitを と のpullbackという。 参考文献 isbn:0262660717

Equalizer Diagram: のlimitを と のequalizerという。Coneのnaturalityが を表している。 命題 参考文献 equalizer in nLab

Forgetful functor 等は習ったが、 一般の場合の定義は難しいらしい。 Free object forgetful functor: -object: について、free object on とは、 comma category のinitial objectのこと。つまり、initial morphism: のこと。 -object から一番シンプルに…

Faithful functor Functor について、function が、 を満たすとき、functor をfaithful functorという。 Full functor なるfunctor のこと。 Fully faithful functor Fullかつfaithfulなfunctorのこと。 命題 参考文献 isbn:0199237182 Concrete category - …

Constructorとextractorがきっちり対応してないのがくやしい？感じである。 reifyやspliceは、q"..${x}.."が便利なので使わなくていいかもしれない。 当たり前？かも知れないが、型に相当するTree*1は、単独ではtypeCheckできない。 c.TYPEmodeが使える。 参…

Type projection SI-3443にさらっとtype projection: は、 と同値である、と書いてある。一方、言語仕様には しかないようで、コンパイラも にはエラーを出す。 class T { class A } type `_.A` = x.A forSome { val x: T } implicitly[`_.A`

Value type Scalaのコードで書ける型のこと(だと思う)。つまり、 type t = X のXに書けるようなものである。 Value typeはabstractとconcreteの二種類に分かれる。 Abstract value type Type parameterまたは(overrideされていない)abstract type memberのこ…

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

ConstantType Scalaには7.typeのような型(constant type)がこっそり含まれていた。macroで取り出して使うことができる。 object ConstantTypeOf { type apply[T](x: T) = macro impl[T] def impl[T: c.WeakTypeTag](c: Context)(x: c.Expr[T]): c.Tree = { i…

Scalaのmacroについて･･･ Inference-Driving Macros ってどういうことだろうと思っていたが、Scalaのmacroは相当賢くて def apply(x: String) = macro vimpl def vimpl(c: Context)(x: c.Expr[String]): c.Expr[Any] = ... としてもちゃんと戻り値の型をmacr…

Scalaの話 ずっと無くて困っていた「コンパイルに失敗したら成功」というテストが Scalaのmacroで簡単に実装できるようだ。 Testing for compiler errors with untyped macros. shapeless/core/src/main/scala/shapeless/test/typechecking.scala at master …

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…