このスライドは、2020/10/17 - 18 に開催された「ScalaMatsuri」で発表したものです。Read less
![Scala 初心者が米田の補題を Scala で考えてみた](https://cdn-ak-scissors.b.st-hatena.com/image/square/1fc089bd631a95a410f1c2a93a8b2a2a2e064f83/height=288;version=1;width=512/https%3A%2F%2Fcdn.slidesharecdn.com%2Fss_thumbnails%2Fyoneda-201017060719-thumbnail.jpg%3Fwidth%3D640%26height%3D640%26fit%3Dbounds)
このスライドは、2020/10/17 - 18 に開催された「ScalaMatsuri」で発表したものです。Read less
『プログラマのための圏論』はこれまでの分をまとめてPDFファイルにしました。参考にしてください。
はじめに 対象読者 数学以前 数学の基礎 ホモロジー代数 圏論 もっと手取り早く圏論の勉強を始めたい人へ おわりに 紹介した書籍 はじめに 私が圏論という分野を知るきっかけは、おそらくこの文章を読んでいるほとんどの人と同様に Haskell の勉強をしたことがきっかけでした。 Haskell のモナドなどを利用する上では圏論を理解する必要は全くないのですが、型システムや処理系に関して詳しく知りたくて論文を読むと圏論の言葉が普通に使われていて、理解できずに断念していました。 そこで、当時数人が集まってやっていた圏論勉強会に参加して圏論の勉強を始めました。当時読んでいた書籍は Conceptual Mathematics: A First Introduction to Categories でした。この本は圏論の初学者向けに書かれた本で、数学的な知識をほとんど仮定せずに理解できるように書かれ
ネットワークの計測と解析 インターネットの使われ方やネットワークの挙動を把握する事は、ネットワークを運用し、その技術開発を行う ために欠かせません。しかし、観測で得られるデータ量は膨大ですがノイズが多く、また、観測できるのは極めて限られた部分でしかありません。そこで、膨大なデータから意味のある情報を抽出したり、部分的な観測からより一般的な傾向を推測する事が必要となります。... インターネット基盤技術 速くて、安全で、信頼性が高く、使いやすく、など、インターネットサービスへの要求はますます高まっています。これらの要求に応えるために、インターネットの 基盤技術も日々進歩しています。いまやインターネットはつながるだけのサービスではなく、高度で複雑な機能を備えた社会基盤となりました。IIJ技術研究所は、インターネットの基盤として実現が期待される機能を提供するために、さまざまな技術課題に取り組んで
Menu Menu Agda で証明しながら圏論を学ぶという予定です。あまり入門ではないかも。 Higher-Order Categorical Logic の 0章に相等する内容です。 BitBucket category-exercise-in-agda source code Agda の入門の要約 Agda の入門 Agda の集合の Level Agda の record Agda のReasoning Caategory module と圏の入門 自然変換 IdentityFunctor と Hom Reasoning Monad の結合則 Sets と Monoid を使った Monad の例 Kleisli 圏の構成 ここまでが Monad を理解するための部分。以下は、Adjoint 関連です。 Adjoint から Monad を導く Kleisli 圏による Mona
つまりなぜかいきなり高階型の話です。 これ 関数を扱えることはどのようにプログラミング言語の能力をあげるか に対する便乗というかツッコミとして。 つい先日もある人がこんなこと https://twitter.com/koropicot/status/365014333413011457 を言っていて*1、「ですよねー」と勝手に納得していたりしましたが。 つまりScalazでよくみるような高階型 trait Monad[F[_]] extends Applicative[F] { implicit val listMonad = new Monad[List]{ がないと、モナドとして抽象化や共通化ができない、という話です。*2 高階型についてはたとえばこれ (もりそば)Scalaによる高階型変数 - Higher-kind Generics とか読んでください。 関数がオブジェクトとして扱
来年も作りたい!ふきのとう料理を満喫した 2024年春の記録 春は自炊が楽しい季節 1年の中で最も自炊が楽しい季節は春だと思う。スーパーの棚にやわらかな色合いの野菜が並ぶと自然とこころが弾む。 中でもときめくのは山菜だ。早いと2月下旬ごろから並び始めるそれは、タラの芽、ふきのとうと続き、桜の頃にはうるい、ウド、こ…
「モナドは自己関手圏のモノイド対象にすぎない」とワドラーはいったがその事を説明したいと思います。 次のものを説明します。 対象 射 結合則 恒等射 圏 関手 自然変換 圏の基礎 圏は以下のものから構成されます 射 対象 射はソースとターゲットを結ぶ矢印とされます XがソースYがターゲットの社は次の通りに記述されます。 射の結合 の二つの射が存在した場合結合する事ができます さらに以下の公理を満たす必要があります。 恒等射 結合則 恒等射 任意の対象Xに対して射 が存在し恒等射という、さらに任意の射に対して が成り立つ。 結合則 が成り立ちこれを結合則という。 関手 圏Cと圏Gが存在したとして、 CからGに対して 対象 射 を対応させるものである。この時関手は以下の性質を保っていなけばならない。 恒等射 射の合成 自然変換 圏Cと圏Dの間に、F、Gという関手が存在し、 FからGへ移す射 が存
first と pure は図式の中では関手っぽさを出すため First と Pure のように先頭大文字にしてみた。 多相なものには気分によって型を補足した。 1.[拡張] first (pure f) = pure (f×id) Hom(X,Y) で X から Y への射の集まりを表すと (-)×id_D Hom(B,C) --------------> Hom(B×D,C×D) | | | Pure | Pure ↓ ↓ Hom(B,C) --------------> Hom(B×D,C×D) First_D 上辺は通常の関数の世界、下辺は Arrow の世界。 first (pure f) = pure (f×id) で f = id とすると first (pure id) = pure (id×id) pure id も pure (id×id) も idA なので firs
集合と写像、位相空間と連続写像、群と準同型等を総括的に扱う概念が圏と関手です。もちろん位相幾何学で重要なのはホモロジーやホモトピーに代表されるように、位相空間と連続写像の圏から群と準同型の圏へのホモトピー不変関手です。 こういった風に数学ではある概念をどんどんと抽象化させていくというのは良く行われることです。抽象化というのは与えられた対象の重要な性質のみの抜き出す、余分な情報は捨てるという作業で、思考を明確にしてくれます。 それともう一つ、抽象化された中で考えた概念というのは、具体性を求めらた時に広く応用がきくという点です。ここで定義する圏(関手)における(co)limitの考えはそのまま、集合、位相空間、群などに反映することができます。 圏論の有名な教科書としては「Categories for the working mathematician」【Mac98】が有名である。日本語版の【M
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く