Questions tagged [category-theory]
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)
120
questions
136
votes
7
answers
39k
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 ...
dan
31
votes
2
answers
3k
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 ...
- 5,071
27
votes
3
answers
3k
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 but ...
- 5,071
22
votes
2
answers
1k
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 day, ...
- 5,071
22
votes
2
answers
2k
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 ...
- 628
19
votes
1
answer
268
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 ...
- 71.8k
16
votes
4
answers
5k
views
What exactly is the semantic difference between category and set?
In this question, I asked what the difference is between set and type. These answers have been really clarifying (e.g. @AndrejBauer), so in my thirst for knowledge, I submit to the temptation of ...
- 3,492
14
votes
2
answers
712
views
Reference request: Category theory as it applies to type systems
I keep hearing about how one must learn category theory to truly understand programming language theory. So far, I've learned a good deal of PL without ever stepping foot into the realm of categories. ...
- 2,200
12
votes
1
answer
803
views
Is there an isomorphism between (subset of) category theory and relational algebra?
It comes from big data perspective. Basically, many frameworks (like Apache Spark) "compensate" lack of relational operations by providing Functor/Monad-like interfaces and there is a similar movement ...
- 233
10
votes
2
answers
936
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? ...
- 409
10
votes
1
answer
1k
views
Monad in Haskell programming vs. Monad in category theory
I have a question about concept of monad used in Haskell programming
and category theory in math.
Recall in Haskell a monad consists of following components:
A type constructor that defines for each ...
- 213
9
votes
3
answers
328
views
Rigorous proof that parametric polymorphism implies naturality using parametricity?
This question asks for an informal explanation of why all polymorphic functions between functors are natural transformations (This is a claim made by Bartosz Milewski). One answer to that question ...
- 3,492
9
votes
2
answers
638
views
Functor laws and natural transformations in Haskell
As I've been struggling to get a deeper understanding of monads in Haskell, I started reading about functors and their counterparts in category theory. Keep in mind that I have no background in the ...
- 183
9
votes
0
answers
152
views
Using naturality to prove $f: \forall\alpha. \alpha\times\alpha\to\alpha$ must be a projection
Suppose we have a System F term $f : \forall \alpha. \alpha\times\alpha\to\alpha$, interpreted in a parametric model which is a bicartesian closed category.
I was wondering if in such context it is ...
- 14.4k
8
votes
2
answers
691
views
Can the formalisms of category theory replace those of type theory?
The subtleties of the correspondence between type theory and category theory are outside my ken. However, by my naive understanding of the relationship between the two historically convergent ...
- 113
7
votes
1
answer
884
views
What exactly is the relation between Haskell and category theory?
In articles or Quora posts about category theory, I often find mentions of the programming language Haskell. I have little knowledge of category theory and even less of programming. Could someone ...
7
votes
1
answer
358
views
How is the definition of monads in category theory equivalent to the definition in functional programming?
In Haskell, Monad is a class of type constructors which act on types that have the following functions implemented:
...
- 235
7
votes
2
answers
485
views
Why are the laws of an applicative functor defined the way they are?
Let's recall the definition of an applicative functor. Throughout this question, I write $x: T$ to denote that the value $x$ has type $T$.
Definition: An applicative functor consists of a type ...
- 203
7
votes
2
answers
329
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 ...
- 1,538
7
votes
2
answers
201
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 ...
- 311
6
votes
1
answer
230
views
What are some examples of types that can't be derived set theoretically?
I'm hoping for examples that aren't too abstract or useless in day-to-day programming, though not with a lot of hope, since in Bartosz Milewski's book, it is stated that generally speaking, the ...
- 163
6
votes
3
answers
531
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 ...
- 5,071
5
votes
1
answer
828
views
Are there any type constructors which are *not* functors?
So I'm almost done teaching myself category theory. One of the main take-aways for me is that type constructors (higher-kinded types) are endo-functors.
But it this always the case? What's throwing ...
- 2,200
5
votes
1
answer
136
views
DFAs as Categories
I've been recently investigating metacategories (arrows and objects) alongside Automata theory and noticed that a category is a sort of parent container for DFAs, which are just a specific type of ...
user40709
5
votes
1
answer
305
views
How precise is the statement "STLC is the internal language of CCCs"?
I'm studying some basic category theory in the context of type theory and came across the statement "simply typed lambda calculus is the internal language of cartesian closed categories". However ...
- 336
5
votes
0
answers
163
views
What's the internal language of the opposite of a Cartesian closed category?
I have heard the simply typed lambda calculus is the internal language of Cartesian closed categories.
What's the internal language of the opposite type of category?
The rules dual to currying and ...
4
votes
3
answers
196
views
Can lists be defined in a special way so that they contain things of different type?
In https://www.seas.harvard.edu/courses/cs152/2019sp/lectures/lec18-monads.pdf it is written that
A type $\tau$ list is the type of lists with elements of type $\tau$
Why must a list contain ...
- 194
4
votes
2
answers
489
views
Functional Programming and Category Theory
I'm a math Ph.D. having done research in Algebraic Geometry and Algebraic Topology in grad school for my thesis and I've studied a fair amount of category theory in the process (e.g. having worked ...
- 211
4
votes
1
answer
165
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 ...
- 175
4
votes
1
answer
307
views
Semantic readings of the Lambek sequent calculus
I am reading Categorial Grammar: Logical Syntax, Semantics, and Processing by Glyn Morrill and I am stuck with the Fig. 3.9:
Can someone explain this set of formulas and |.| function specifically?
...
- 1,381
4
votes
1
answer
289
views
Generators in category theory
An object K in a category C is called a generator if, for all pairs of
morphisms f, g : A → B between arbitrary objects A and B, f = g iff ∀e
: K → A. f ◦ e = g ◦ e.
Source: http://events.cs.bham....
- 320
4
votes
1
answer
136
views
Writing the coherence conditions for a monad in a functional laguage
i recently asked a related question about the relationship between monads in category theory and Haskell. The answerer showed me the following classes and instances:
...
- 235
4
votes
1
answer
161
views
Why does the category of language types have morphisms, not functors?
I am probably not phrasing this question well, so please bear with me as I try to explain what I mean.
I am working on learning category theory, as applied to programming. So far, I understand that:
...
- 141
4
votes
1
answer
164
views
What is a not-well-founded cotree?
I'm reading the paper "Dual of substitution is Redecoration".
And I'm struggling with understanding the usage of the word "not-well-founded cotrees".
what is a cotree compared to a tree ? I suspect ...
- 381
4
votes
1
answer
267
views
Why are all polymorphic functions between functors natural transformations?
Bartosz Milewski's Category Theory for Programmers says the following:
A parametrically polymorphic function between two functors (including the edge case of the Const functor) is always a natural ...
- 346
4
votes
1
answer
164
views
What is the name of this type of function composition?
If standard function composition is defined as:
(define compose
{ (B → C) → (A → B)
→ (A → C) }
F G -> (λ X (F (G X))))
What type of ...
4
votes
1
answer
78
views
Resources for connections between dependent type theory and LCCC
Can someone recommend introductory articles/papers on the connections between dependent type theory and locally cartesian closed category? Many Thanks!
- 317
4
votes
1
answer
151
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
$\...
- 143
3
votes
3
answers
524
views
Given A to C, and B to C with known complexities, what can be said about A to B?
Say I have two sets of values $A$ and $B$ and for each set I have a computable function from that set to a third set $C$. Now suppose that I want to construct a function from $A$ to $B$, such that if ...
- 354
3
votes
2
answers
81
views
Can we define a program by means of a walk of a graph induced by the category of types?
After reading about Category Theory at https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/ I was wondering whether we can represent any program by means of a walk of a ...
- 33
3
votes
1
answer
905
views
A monad is just a monoid in the category of endofunctors, what's the enlightenment?
Pardon the word play. I'm a little confused about the implication of the claim and hence the question.
Background: I ventured into Category Theory to understand the theoretical underpinnings of ...
- 317
3
votes
5
answers
736
views
functional programming in terms of Set
I'm writing some notes about functional programming, so I'd want to describe some features of the category theory.
I visited wiki page about Category of Set, and I found this:
"The epimorphisms in ...
- 31
3
votes
1
answer
804
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 \...
- 133
3
votes
1
answer
2k
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) = (\operatorname{...
- 31
3
votes
1
answer
140
views
How to determine whether a dependent type that doesn't fit the monad instance is categorically a monad
[Using Idris syntax and terminology, but the question is not about Idris]
If a monad interface (or type class) has a constraint requiring applicative functor, a monad instance can be written by ...
- 253
3
votes
1
answer
131
views
How to explain/understand brackets of applicative functor [[f u1... un]]?
I am reading article about Applicative Abstract Categorial Grammars http://okmij.org/ftp/gengo/applicative-symantics/AACG.pdf and this article uses brackets [[...]] for action on terms inside ...
- 1,381
3
votes
3
answers
387
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 ...
- 155
3
votes
1
answer
293
views
Describing the Bool-And monoid in terms of categories
Normally I put the question before the context, but in this case I want to admit
the possibility that the context and my understanding nullify the question.
Plus it helps me think through my question.
...
- 645
3
votes
1
answer
70
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 ...
- 797
3
votes
2
answers
75
views
Mapping a free variable of type A to a cartesian closed category
In From Lambda Calculus to Cartesian Closed Categories, the author explains the interpretation of lambda calculus in cartesian closed category and at one point he explains how a term representing a ...
- 611