# 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
Filter by
Sorted by
Tagged with
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 ...
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 ...
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 ...
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+...
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 ...
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 ...
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 ...
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 ...
73 views

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?
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$ ...
111 views

50 views

### Expressing that a functor is natural

The Haskell List: Type -> Type constructor implements the Functor typeclass with function ...
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: ...
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 ...
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 ...
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 ...
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? ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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. ...
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....
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 ...
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, ...
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 ...
669 views

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 ...
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 \$\...