As of May 31, 2023, we have updated our Code of Conduct.

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
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 ...
al pal's user avatar
  • 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$ ...
al pal's user avatar
  • 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 ...
0xd34df00d's user avatar
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] ...
al pal's user avatar
  • 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 ...
al pal's user avatar
  • 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?
al pal's user avatar
  • 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 ...
al pal's user avatar
  • 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 ...
Vitaly Olegovitch's user avatar
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$,...
user56834's user avatar
  • 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 ...
goral's user avatar
  • 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; ...
Charlie Parker's user avatar
0 votes
1 answer
91 views

Composition of compostion as a functor

"Composition of Composition" (i.e., (.) . (.)) in Haskell), has type ...
xuq01's user avatar
  • 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 ...
sailsky's user avatar
  • 119
0 votes
1 answer
720 views

“Left identity” of Monad laws in Haskell is wrong

Monad laws in Haskell ...
KenSmooth's user avatar
  • 111
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 ...
Kazark's user avatar
  • 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 ...
Musa Al-hassy's user avatar
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 ...
Stephane Rolland's user avatar
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 ...
Lance's user avatar
  • 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 ...
user56834's user avatar
  • 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+...
Abhiroop Sarkar's user avatar
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 ...
Olivetti's user avatar
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 ...
Klaas van Schelven's user avatar
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 ...
bbarker's user avatar
  • 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 ...
Ignat Insarov's user avatar
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 ...
TomR's user avatar
  • 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?
Johannes Riecken's user avatar
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$ ...
Larry B.'s user avatar
  • 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: ...
Eben Kadile's user avatar
2 votes
1 answer
60 views

Expressing that a functor is natural

The Haskell List: Type -> Type constructor implements the Functor typeclass with function ...
gardenhead's user avatar
  • 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: ...
Eben Kadile's user avatar
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 ...
Polytope's user avatar
  • 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 ...
David Zhang's user avatar
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 ...
user65526's user avatar
  • 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? ...
TomR's user avatar
  • 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 ...
Vincent's user avatar
  • 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 ...
Mike's user avatar
  • 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 ...
chi's user avatar
  • 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 ...
Jean-Baptiste's user avatar
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 ...
dk14's user avatar
  • 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 ...
gardenhead's user avatar
  • 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. ...
gardenhead's user avatar
  • 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....
52d6c6af's user avatar
  • 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 ...
effectfully's user avatar
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, ...
John Forkosh's user avatar
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 ...
user avatar
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 \...
qartal's user avatar
  • 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 ...
Pece's user avatar
  • 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 ...
MainstreamDeveloper00's user avatar
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 ...
Chad950's user avatar
  • 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) $$ ...
qed's user avatar
  • 223