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)

Filter by
Sorted by
Tagged with
137 votes
7 answers
40k 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 ...
user avatar
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 ...
Guy Coder's user avatar
  • 5,091
27 votes
3 answers
4k 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 ...
Guy Coder's user avatar
  • 5,091
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, ...
Guy Coder's user avatar
  • 5,091
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 ...
Ankur's user avatar
  • 628
19 votes
1 answer
277 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 ...
Raphael's user avatar
  • 72.3k
17 votes
4 answers
6k 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 ...
user56834's user avatar
  • 3,702
14 votes
2 answers
746 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. ...
gardenhead's user avatar
  • 2,230
13 votes
1 answer
826 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 ...
dk14's user avatar
  • 243
11 votes
3 answers
455 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 ...
user56834's user avatar
  • 3,702
11 votes
1 answer
2k 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 ...
user267839's user avatar
10 votes
2 answers
948 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? ...
miniBill's user avatar
  • 419
9 votes
2 answers
742 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 ...
giofrida's user avatar
  • 183
9 votes
1 answer
171 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 ...
chi's user avatar
  • 14.5k
8 votes
2 answers
710 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 ...
Polytope's user avatar
  • 113
8 votes
2 answers
569 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 ...
David Zhang's user avatar
7 votes
1 answer
1k 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 ...
tryst with freedom's user avatar
7 votes
1 answer
404 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: ...
Eben Kadile's user avatar
7 votes
2 answers
341 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 ...
Xodarap's user avatar
  • 1,538
7 votes
2 answers
221 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 ...
Pece's user avatar
  • 311
6 votes
1 answer
240 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 ...
bbarker's user avatar
  • 175
6 votes
1 answer
889 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 ...
gardenhead's user avatar
  • 2,230
6 votes
3 answers
549 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 ...
Guy Coder's user avatar
  • 5,091
5 votes
1 answer
1k 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 ...
PhD's user avatar
  • 337
5 votes
2 answers
675 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 ...
del's user avatar
  • 221
5 votes
1 answer
141 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 ...
user avatar
5 votes
1 answer
323 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 ...
effectfully's user avatar
5 votes
0 answers
169 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 ...
Molly Stewart-Gallus's user avatar
4 votes
3 answers
217 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 ...
user65526's user avatar
  • 194
4 votes
1 answer
167 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 ...
Nikolaj-K's user avatar
  • 175
4 votes
1 answer
333 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? ...
TomR's user avatar
  • 1,381
4 votes
1 answer
307 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....
52d6c6af's user avatar
  • 320
4 votes
1 answer
148 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: ...
Eben Kadile's user avatar
4 votes
1 answer
174 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: ...
Crell's user avatar
  • 141
4 votes
1 answer
171 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 ...
Stephane Rolland's user avatar
4 votes
1 answer
363 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. ...
D. Ben Knoble's user avatar
4 votes
1 answer
364 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 ...
Max Heiber's user avatar
4 votes
1 answer
173 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 ...
Jean-Baptiste's user avatar
4 votes
1 answer
95 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!
thoughtpolice's user avatar
4 votes
1 answer
155 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 $\...
pedagand's user avatar
  • 143
3 votes
3 answers
525 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 ...
Ryan1729's user avatar
  • 364
3 votes
2 answers
83 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 ...
Olivetti's user avatar
3 votes
5 answers
774 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 ...
Mike's user avatar
  • 31
3 votes
1 answer
825 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 \...
qartal's user avatar
  • 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{...
user15751's user avatar
3 votes
1 answer
146 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 ...
Kazark's user avatar
  • 253
3 votes
1 answer
163 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 ...
TomR's user avatar
  • 1,381
3 votes
3 answers
391 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 ...
user128932's user avatar
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 ...
Bakuriu's user avatar
  • 807
3 votes
2 answers
77 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 ...
al pal's user avatar
  • 621