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)
104
questions
3
votes
1answer
125 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 ...
2
votes
1answer
40 views
Any mathematical tools for analyzing mutable memory
Wondering if there are any documents, theories, or methodologies for dealing with mutable memory mathematically. Basically a formal algebraic model of how computers manipulate memory. Along the lines ...
12
votes
4answers
2k 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 ...
0
votes
1answer
121 views
Can we define the Functor Category in Haskell (or any other language with a more expressive type system)?
Here I am talking about the Functor category, which is defined as a category whose objects are functors and morphisms are natural transformations.
For reference: https://ncatlab.org/nlab/show/functor+...
3
votes
2answers
76 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 ...
1
vote
2answers
72 views
What mathematical terminology exists for “embellished trees”?
I'm looking for some pointers on proper mathematical (FP?, category-theory?) terminology.
My apologies if the below is somewhat imprecise; I suppose the precision is precisely what I'm looking for in ...
4
votes
1answer
189 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 ...
1
vote
0answers
50 views
How can I prove impossibility of generalizing a given higher order function from pure to monadic or applicative?
There is a great divide in Haskell between pure and monadic algorithms. While the latter are indistinguishable from their usual imperative counterparts, the former can get much more magical. What this ...
3
votes
1answer
73 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
vote
1answer
46 views
What's the theory behind the operator precedences of common operators?
Could for example the precedence ordering of addition, multiplication, exponentiation, boolean and/or and zip/cross product be inferred from a few rules?
2
votes
0answers
60 views
Select/Barrier statements in $\pi$-Calculus denotational semantics
A select statement waits on $n$ channels until channel $0$ or $1$ or ... or $n-1$ have data.
A barrier lock waits on $n$ ...
4
votes
1answer
111 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:
...
2
votes
1answer
50 views
Expressing that a functor is natural
The Haskell List: Type -> Type constructor implements the Functor typeclass with function ...
6
votes
1answer
272 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:
...
8
votes
2answers
643 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 ...
7
votes
1answer
388 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 ...
3
votes
0answers
75 views
Examples of continuations in pure mathematics [closed]
I am not a computer scientist and have no knowledge of programming.
However, I wondered continuations occur as natural and interesting mathematical structures, perhaps as algebraic or type theoretic ...
4
votes
1answer
273 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
vote
0answers
49 views
Formal name of the product of product type
What is the formal name in type theory of the operation that creates a "matrix of types" from product types (such as std::tuple in C++)?
For example if we consider ...
3
votes
5answers
580 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 ...
9
votes
0answers
129 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 ...
4
votes
1answer
141 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 ...
12
votes
1answer
668 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 ...
5
votes
1answer
678 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 ...
14
votes
2answers
637 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. ...
3
votes
1answer
190 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....
5
votes
1answer
219 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 ...
3
votes
0answers
129 views
Scott/Lawson topology for function space domain
Given two domains, $D_1$, $D_2$,
already equipped with Scott (or Lawson) topology,
the product domain $D=D_1\times D_2$
has the Tychonoff product topology, e.g.,
Mathematical Theory of Domains, ...
5
votes
1answer
118 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 ...
3
votes
1answer
669 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 \...
7
votes
2answers
156 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 ...
1
vote
1answer
161 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
65 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 ...
1
vote
1answer
56 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) $$
...
2
votes
1answer
74 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 ...
2
votes
1answer
433 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 ...
10
votes
2answers
838 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? ...
3
votes
3answers
331 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
41 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
80 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 ...
4
votes
1answer
147 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
266 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
66 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
63 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 ...
21
votes
2answers
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 ...
3
votes
1answer
1k 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{...
6
votes
3answers
458 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
138 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
$\...
22
votes
2answers
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, ...
26
votes
3answers
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 ...
