Category theory is used to formalize mathematics and its concepts as a collection of objects and arrows (also called morphisms). Category theory can be used to formalize concepts of other high-level abstractions such as set theory, ring theory, and group theory. (By Steve Awodey)

learn more… | top users | synonyms

0
votes
0answers
20 views

Natural isomorphism of a monoidal category [migrated]

The definition of a Monoidal Category from "Categories for the working mathematician" says that it is a category equipped with tensor products, associative up to a natural isomorphism. What does ...
1
vote
1answer
97 views

Intuition behind F-algebra

I looked at here for getting an intuition about F-algebra, but I am still left with some questions. Suppose I have a group signature as $\Sigma= (* : X \times X \rightarrow X, \thicksim: X ...
5
votes
2answers
52 views

Formalizing basic category theory in Coq

I'm a total beginner in Coq and I'm trying to implement some category theory stuff as an exercise. I surfed a little among git repos of the many avaible such implementations (HoTT, Awodey's Coq ...
0
votes
1answer
27 views

How can I formalize key value stores with set theory?

I'm currently developing a simple key-value NoSQL store and want to build its formal model. I found article about key value formalisation with category theory, but I'm interested are there some works ...
2
votes
0answers
26 views

Exponential Object in a poset [closed]

I have been trying to get to grips with what an exponential object is using a poset as an example. So in the poset... {2, 4, 6, 8, 9, 12, 14, 30, 36, 48, 60, 72, 84} x is related to y iff x is a ...
0
votes
1answer
17 views

identities property of squaring functor?

From page 31 of The algebra of programming : Next, consider the squaring functor $()^2: Fun \leftarrow Fun$ defined by $$ A^2 = \{(a, b) | a \in A, b \in B\} \\ f^2(a, b) = (f a, f b) $$ ...
1
vote
1answer
40 views

Definition of opposite category

From page 29 of The algebra of programming : For any category C the opposite category $C^{op}$ is defined to have the same objects and arrows as C, but the source and target operators are ...
0
votes
0answers
18 views

Mobile Ambients and structure

I am reading text books of category theory, and trying to apply it. My question comes from: Luca Cardelli, Andrew D. Gordon. Mobile Ambients. In Proceedings of POPL'98. In the paper, An ambient is ...
1
vote
1answer
57 views

Identity in the category of types and functions

In the model of (functional) programming languages as a category where the objects are types and the arrows are functions, I'm trying to really understand what's really the identity arrow. Barr-Wells ...
5
votes
2answers
120 views

Which fixpoint is Haskell list type?

Let's say that lists are defined as List a = Nil | Cons a (List a) Then, in Haskell is List x the greatest or least fixpoint? ...
1
vote
1answer
68 views

Category theory and graphs

Could most categories , or a finite part of them be represented on a subset of a complete graph of N vertices (Kn) which is connected. and partly directed? Could all the axioms of category theory be ...
2
votes
0answers
26 views

About computer science and category theory [duplicate]

I read that Category Theory has alot to do with how programs and information can be organised.Can Category theory simplify various programming strategies? If a specific Category is represented as a ...
3
votes
0answers
42 views

What is a polyad? [closed]

I've read the wikipedia article, but I don't speak category theory (and I'm not sure how to start so I'm just picking something that sounds interesting). So, can someone give me a simple, possibly ...
3
votes
1answer
90 views

What do functions look like, if I stated out with the categoical model of my type theory?

I see how objects in a category stand for types, but where do I find the terms and more specifically the rules which tell me which of them are allowed? When I e.g. consider a Cartesian closed category ...
1
vote
1answer
91 views

How much math background do you need to understand how category theory is applied to Haskell? [duplicate]

Basically, how much math background do you need to understand how category theory is applied to Haskell? If you already have mathematical maturity, can you jump right into it, or should you be ...
3
votes
1answer
58 views

Generalized operators for programming languages

After asking this question on stackoverflow, it has changed slightly. Is there a way to represent a grammar as a basis for a vector space and represent a program as an object that lives in that ...
3
votes
1answer
46 views

What's the correct definition of the $\Upsilon$ category of schedules?

I'm reading this article about game semantics and I'm a bit puzzled with the definition given for $\Upsilon$ in section $3.3$. There are some points that are either unintelligible or that don't make ...
12
votes
2answers
769 views

Category theory (not) for Programming?

After learning Haskell and other not so pure FP languages I decided to read about Category theory. After gaining good understanding of Category theory I started thinking about how the concepts of ...
2
votes
1answer
94 views

The List functor

I have been reading some notes on Category Theory. One question that is posed is to verify the definition of $\operatorname{List}$ is a functor... $\operatorname{List}(g \circ f) = ...
4
votes
3answers
180 views

Tool/app for learning category theory?

Being a programmer I appreciate the errors given by a compiler for a programming language and come to rely on the compiler's error as a safety net. In learning category theory I would like to have ...
4
votes
1answer
91 views

Substitution by structural recursion

Following the article's notation, I write $\mathcal{F}$ for the category of presheaves on a (suitable) category $\mathbb{F}$, $TV$ for the presheaf of terms, $\delta$ for the context extension, and ...
13
votes
2answers
545 views

What is meant by Category theory doesn't yet know how to deal with higher-order functions?

In reading Uday Reddy's answer to What is the relation between functors in SML and Category theory? Uday states Category theory doesn't yet know how to deal with higher-order functions. Some ...
13
votes
3answers
1k views

What is the relation between functors in SML and Category theory?

Along the same thinking as this statement by Andrej Bauer in this answer The Haskell community has developed a number of techniques inspired by category theory, of which monads are best known ...
14
votes
2answers
937 views

How are programming languages and foundations of mathematics related?

Basically I am aware of three foundations for math Set theory Type theory Category theory So in what ways are programming languages and foundations of mathematics related? EDIT The original ...
6
votes
2answers
142 views

Are monoids useful in optimization?

Many common operations are monoids. Haskell has leveraged this observation to make many higher-order functions more generic (Foldable being one example). There is ...
53
votes
6answers
11k views

Is Category Theory useful for learning functional programming?

I'm learning Haskell and I'm fascinated by the language. However I have no serious math or CS background. But I am an experienced software programmer. I want to learn category theory so I can become ...
11
votes
1answer
169 views

Natural occurrences of monads that make use of the category-theoretical framework

Today, a talk by Henning Kerstan ("Trace Semantics for Probabilistic Transition Systems") confronted me with category theory for the first time. He has built a theoretical framework for describing ...