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
1
vote
0
answers
30
views
Is there some math problem that must use category theory to solve? [closed]
If there is no calculus，we can't solve a problem like “surface area”.
Is there some math problem that can be solved thanks to category theory?
If there is no such math problem, it means that category ...
- 5,189
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!
- 111
0
votes
1
answer
66
views
$\beta$ reduction equational equality
In Categories, Types and Structures, authors talk about exponential objects in section 2.3.1.
Let $C$ be a Cartesian category, and $a,b \in Ob_C$. The exponent of $a$ and $b$ is an object $b^a$ ...
CommunityBot
- 1
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 ...
-1
votes
2
answers
132
views
Applying FP/Categorical terminology to non-FP languages
In my continuing effort to finally wrap my brain around advanced FP/categorical concepts, I've been reading dozens of articles and tutorials; what I have concluded is that:
1) Category Theory and ...
- 263
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 ...
- 263
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 ...
- 263
0
votes
0
answers
52
views
Goedel's theorem, halting problem and irreducible complexity
I have a vague idea on the tip of my mind that I can only convey through examples.
Gödel's theorem states that some systems (ZFC, for example) are always incomplete in the sense that new axioms (which ...
0
votes
0
answers
31
views
Ambiguous type of "triangle" operator for sum types
In Meijer, Fokkinga and Patersons "Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire" the ∇ operator for sum types is introduced which removes the tags from its ...
- 26
1
vote
1
answer
46
views
On the logical and categorical interpretation of lambda calculi and type systems
There is a well-known Curry-Howard-Lambek correspondence between certain type systems, proof calculi and categories.
Some variants of Barendregt's pure type systems have the property of strong ...
- 38.2k
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 ...
- 263
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 ...
- 263
0
votes
0
answers
46
views
what are all the ways of delimiting blocks
To my knowledge, in block-structured programming languages, there are 2, maybe 3 main ways of delimiting a block.
Using start and end tokens, this can be brackets or reserved words etc
Using ...
- 81
2
votes
2
answers
75
views
Can we somehow get functoriality from purely type-theoretic reasoning?
In this question, I asked about how to prove naturality from parametric polymorphism, using parametricity. The current answer to that question simply assumes that the functors in question satisfy the ...
- 263
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 ...
- 263
2
votes
2
answers
150
views
The second Functor law is redundant, but I don't understand the proof
When we defining a Functor instance in Haskell, it should satisfy the following two laws:
fmap id = id
...
- 20.3k
0
votes
1
answer
63
views
Does category theory only deal with immutable objects? If so, why?
IIUC, category theory only applies to immutable objects, and mutability is modelled within that using e.g. functors, monads. Is that true? If so, why doesn't category theory include immutability? Has ...
- 29.4k
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 ...
- 328
0
votes
0
answers
32
views
Exercise from Algebra of Programming on catamorphisms
This is an exercise from Algebra of Programming which I'm reading for self-study.
Below, $T$ is the initial algebra of $F$.
What I've tried:
I can construct $h \circ F (\pi_2) : F(A \times B) \...
- 263
1
vote
1
answer
52
views
Category Set language using simply typed lambda calculus
I am currently self learning Category Theory and Simply typed lambda calculus (STLC). For learning purposes, I have implemented an STLC interpreter as given in Types and Programming Languages book ...
- 7,568
0
votes
2
answers
50
views
What is name of type " Function->Value->Bool = if (Bool) Function (Value) " in Category theory?
I am very new to functional programming so sorry if the question is stupid.
Having this function
...
CommunityBot
- 1
2
votes
1
answer
104
views
Why does the CwF definition require a set of types under a context rather than a class of types?
In "Syntax and Semantics of Dependent Types" at the top of page 24, Martin Hoffman describes $\mathit{Ty}_{\mathcal C}(\Gamma)$ as the collection of semantic types under context $\Gamma$.
It ...
- 898
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 ...
- 29.4k
1
vote
1
answer
66
views
Are monads a unification of a number of computer science concepts?
The following commentator writes:
Monads are a unification of a bunch of computer stuff, including sequencing, IO, non-determinism, state, concurrency and exceptions. When I say "unification&...
- 5,421
2
votes
1
answer
213
views
Creating a large tuple from smaller tuples via a monad or applicative
Suppose I have a term $a :\alpha$ of the Simply-Typed Lambda Calculus (in the following, $\alpha, \beta, \gamma$ stand for arbitrary types) and I want to lift it to a term
$\lambda x_{\beta}. \;(x, \, ...
CommunityBot
- 1
2
votes
3
answers
272
views
Set theory pertaining to category theory and functional programming
I'm reading an unfinished Introduction to Category Theory/Products and Coproducts of Sets and have come across the following:
A power set of a set is the set of all its subsets. A script 'P' is used ...
- 121
1
vote
0
answers
35
views
Interpreting Minimal STLC using a $\lambda 1$ Category
On page 139, example 2.4.5 of "Categorical Logic and Type Theory" by Bart Jacobs demonstrates the interpretation of the abstraction typing rule with respect to a $\lambda 1$ category. ...
- 173
2
votes
1
answer
90
views
Meaning of Free (Arbitrary Abstract Algebra Term)
I'm currently learning abstract algebra and the word free appears (free monoid, free vector space) throughout different literatures. Is there a general (and simple) definition of the word (and ...
- 191
1
vote
0
answers
49
views
Is there a term for the inverse of a fixed-point operator?
When working with recursion it is often useful to find the least or greatest fixed points of a morphism, often using a fixed-point combinator. When working with recursion schemes, the inverse ...
- 11
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 ...
2
votes
0
answers
54
views
What does point-free mean mathematically?
Point-free style is generally taken to mean a style of programming without explicit variables.
I have some intuitions on point-free style but I want to know what the formal mathematical definition is.
...
2
votes
0
answers
71
views
The word "algebra" in category theory
I am currently learning category theory and a saying that I see a lot is that X is the algebra of something (e.g. Monoid is an algebra of something). Can someone explain to me what that means? Thanks!
- 317
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 ...
- 1,671
2
votes
0
answers
82
views
What is the category theory interpretation of higher order abstract syntax?
Suppose you have a simple sort of lambda calculus abstract syntax tree. The fine details don't really matter.
...
0
votes
0
answers
94
views
Can we think of a non-symmetric product type in Haskell?
Meta note: I asked this question here a while ago. It got an answer:
type a /\!! b = (a, ((b -> Void) -> Void))
Unfortunately, I do not reckon it to be ...
- 228
1
vote
2
answers
232
views
Has category theory had an impact on computer science?
I've only learned bit of category theory, but so far its relation to type systems seems mostly descriptive. For example, you really don't need to know about coproducts to come up with the idea of ...
- 29.5k
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 ...
1
vote
1
answer
162
views
Functor in category theory: The free theorem for fmap
According to nLab article:
https://ncatlab.org/nlab/show/functor
Definition
External definition
A functor $F$ from a category $C$ to a category $D$ is a map sending each object $x \in C$ to an object ...
- 2,329
1
vote
0
answers
34
views
Can I get the lambda calculus for free from Cartesian closed categories?
I have heard the simply typed lambda calculus is the internal language of closed Cartesian categories.
I have a written a compiler from the STLC to CCCs but this involves a lot of ugly tuple shuffling....
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 ...
- 1,483
1
vote
1
answer
101
views
Datatypes as initial algebras
I'm refining my understanding of the connection between initial algebras and datatypes. This paper suggests that one could even represent the categories corresponding to datatypes definitions:
as ...
CommunityBot
- 1
3
votes
0
answers
98
views
(Co)-monads and terminating implementations
The bounty above should read 'I would like to know whether the example I discuss is a com-monad and why (why not).'
Suppose we set $\mathbb{M} \alpha := r \to \alpha$, where $r$ is some fixed type, ...
- 194
1
vote
0
answers
27
views
Constructing a monad via type synonyms of a particular kind
We can define a reader/environment monad on the simply-typed lambda calculus, using the following three equations, where $r$ is some fixed type, $\alpha$ is any type (I subscript some terms with their ...
- 194
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 ...
- 581
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
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.
...
- 581
1
vote
1
answer
56
views
What are $(S,\Sigma)$-CCCs?
I was reading this and I was trying to understand the definition of $(S,\Sigma)$-CCC. The first requirement says:
a mapping [[_]] : S → |C|, associating some object [[s]] ∈ |C| to
any s ∈ S;
...
- 581
1
vote
0
answers
44
views
Is the identity functor a kind of free object?
My understanding of free objects is: Free functors, free applicatives, free monads, free monoids, &c, give you more structure "for free", i.e. in general, or for all some thing with less structure,...
- 253
0
votes
1
answer
67
views
Is there any correspondence between SUM type in type theory and arithmetical summation?
Is there any correspondence between the coproduct(sum) type in type theory and arithmetical summation?
For example what does 3+4 or x+6 mean in type theory?
- 581
2
votes
0
answers
140
views
Is this possible: In OOP, private methods in a class form a F-coalgebra and public methods in a class form an F-algebra?
I recently found out that OOP classes turn out to be F-coalgebras:
https://www.semanticscholar.org/paper/Objects-and-Classes%2C-Co-Algebraically-Jacobs/c7c45abf7d99e0aef627fd5223023bf82e70dc71
The ...
- 121