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
38
views
Is, beta reduction in type theory being considered as counit for hom-tensor adjunction in category theory, a denotational or operational semantic?
In the article at nlab about the relation between type theory and category theory, it is said that "beta reduction" in type theory corresponds to "counit for hom-tensor adjunction" in category theory ...
- 611
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$ ...
- 611
1
vote
0
answers
57
views
A notion dual to a product type having a given type
Consider this class:
class Has record part where
extract :: record -> part
update :: (part -> part) -> record -> record
It captures the notion of ...
- 165
2
votes
2
answers
87
views
What is the adjunct of the evaluation morphism in a closed monodical category?
According to the nlab article about evaluation map if $X, Y \in C$, a closed monodical category then the adjunct to evaluation morphism $[X, Y]\otimes X \rightarrow Y$ is the identity morphism $[X, Y] ...
- 611
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
1
vote
1
answer
167
views
Is monoid the category for untyped lambda calculus?
If cartesian closed categories are the model for simply typed lambda calculus, then can it be said that a monoid is a categorical model for untyped lambda calculus?
- 611
2
votes
1
answer
143
views
How is β-reduction a 2-morphism in Category theory?
According to Categorifying CCCs: Computation as a Process, computation or β-reduction process in untyped-lambda calculus is in fact a 2-morphism in category theory.
Can someone please describe me ...
- 611
1
vote
1
answer
173
views
Category theory structures to describe topics and queues
What are the category theory structures describing queues and topics? By queues and topics I mean the ones described in systems like Apache Kafka, AcriveMQ or Java Messaging Service.
Where I can find ...
- 1,198
1
vote
1
answer
62
views
Generalization of Functors to other datatypes?
Functors in category theory, and also in its application to functional programming, can be seen as a kind of "structured" functions: Given two sets $A,B$, rather than just having a function $f:A\to B$,...
- 3,492
1
vote
0
answers
53
views
Prove that set of operations form a commutative Monoid
this is my first post on this exchange.
I am looking for some help with defining a proof that a set of operations I have designed forms a commutative monoid.
(Disclaimer: I am not sure that I have ...
- 111
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;
...
- 2,960
0
votes
1
answer
91
views
Composition of compostion as a functor
"Composition of Composition" (i.e., (.) . (.)) in Haskell), has type ...
- 1,170
1
vote
1
answer
322
views
join is the heart of the monad because it encompasses everything a monad can do that a functor cannot. Is this true? [closed]
There is a controversy about Monad implementation in S.O .
The original question is,
What's so special about Monads in Kleisli category?
Is there any counterexample that Functors cannot do what ...
- 119
0
votes
1
answer
720
views
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
1
vote
0
answers
48
views
Terminology Questions: Data-structure consisting of lists without repetitions
I've google around and have been unsuccessful in finding a name for a data-structure consisting of a list whose elements are unique.
I've seen "unique sorted lists", but I'm looking into the more ...
- 884
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
2
votes
1
answer
48
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 ...
- 2,103
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
0
votes
1
answer
158
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+...
- 101
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
1
vote
2
answers
78
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 ...
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
1
vote
0
answers
55
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 ...
- 229
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
1
vote
1
answer
57
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?
- 113
2
votes
0
answers
64
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$ ...
- 193
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
2
votes
1
answer
60
views
Expressing that a functor is natural
The Haskell List: Type -> Type constructor implements the Functor typeclass with function ...
- 2,200
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
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
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
3
votes
0
answers
89
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 ...
- 194
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
2
votes
0
answers
58
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 ...
- 221
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
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
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 ...
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
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
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
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
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
3
votes
0
answers
144
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, ...
- 305
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
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
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
1
vote
1
answer
195
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
0
answers
75
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 ...
- 21
1
vote
1
answer
63
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) $$
...
- 223