2022 Developer Survey is open! Take survey.

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
0 votes
0 answers
39 views

Nested stack automaton in category theory

Is there a similar concept in category theory to the Nested Stack Automaton? Actions are the closest thing I could find, as they are similar to deterministic automata. It is unclear what grammars ...
user avatar
2 votes
1 answer
88 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 ...
user avatar
1 vote
1 answer
65 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&...
user avatar
  • 1,189
2 votes
3 answers
235 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 ...
user avatar
  • 121
1 vote
0 answers
30 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. ...
user avatar
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 ...
user avatar
0 votes
2 answers
47 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 ...
user avatar
1 vote
1 answer
49 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 ...
user avatar
  • 3,464
7 votes
2 answers
209 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 ...
user avatar
  • 3,464
2 votes
0 answers
61 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!
user avatar
2 votes
1 answer
87 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 ...
user avatar
1 vote
1 answer
42 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 ...
user avatar
  • 11
2 votes
0 answers
49 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. ...
user avatar
2 votes
0 answers
67 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!
user avatar
11 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 ...
user avatar
0 votes
0 answers
93 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 ...
user avatar
1 vote
2 answers
188 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 ...
user avatar
5 votes
0 answers
132 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 ...
user avatar
0 votes
1 answer
93 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 ...
user avatar
1 vote
0 answers
33 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....
user avatar
2 votes
0 answers
73 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. ...
user avatar
4 votes
3 answers
159 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 ...
user avatar
  • 194
2 votes
1 answer
175 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, \, ...
user avatar
  • 194
3 votes
0 answers
96 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, ...
user avatar
  • 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 ...
user avatar
  • 194
3 votes
1 answer
515 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 ...
user avatar
  • 327
3 votes
1 answer
272 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 ...
user avatar
  • 201
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 ...
user avatar
  • 352
2 votes
1 answer
196 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. ...
user avatar
1 vote
0 answers
41 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,...
user avatar
  • 253
0 votes
1 answer
50 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?
user avatar
  • 593
2 votes
0 answers
92 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 ...
user avatar
  • 121
4 votes
1 answer
192 views

Why are all polymorphic functions between functors natural transformations?

Bartosz Milewski's Category Theory for Programmers says the following: A parametrically polymorphic function between two functors (including the edge case of the Const functor) is always a natural ...
user avatar
1 vote
0 answers
30 views

What is the maths name for a set which contains the Domain and Codomain of a function? [closed]

Im interested in this so that I can name a type parameter in a program I'm writing. There is function that that has three parameters. D, Domain C, Codomain X, where D is a subset of X and C is a ...
user avatar
  • 143
9 votes
1 answer
504 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 ...
user avatar
  • 141
1 vote
0 answers
55 views

Can the most general unifier be defined categorically?

I remember from my reading of Category Theory for Computing Science that classical concepts like weakest preconditions can be seen as the categorical notion of pullback. I was wondering if the same ...
user avatar
  • 2,220
-1 votes
1 answer
116 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 ...
user avatar
  • 141
4 votes
1 answer
136 views

Why does the category of language types have morphisms, not functors?

I am probably not phrasing this question well, so please bear with me as I try to explain what I mean. I am working on learning category theory, as applied to programming. So far, I understand that: ...
user avatar
  • 141
2 votes
0 answers
87 views

Proof of the limit-colimit coincidince

Note: I figured this out, but haven't had the time to write an answer for it: see the comment. For reference: the discussed material appears in http://www.cs.ru.nl/B.Jacobs/CLG/JacobsCoalgebraIntro....
user avatar
1 vote
1 answer
81 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 ...
user avatar
  • 2,220
2 votes
0 answers
46 views

Understanding Isabelle's implementation of coinduction

I'm studying how coinduction was encoded in Isabelle. At page 7 of the attached document, the author describes how some datatypes can be encoded as initial algebras. Here is one example: Finite lists ...
user avatar
  • 2,220
0 votes
0 answers
58 views

How is substitution in type theory the composition of classifying morphisms in category theory?

In the article at nlab about relation between category theory and type theory, it is said that substitution in type theory is the same as composition of classifying morphisms in category theory. ...
user avatar
  • 593
1 vote
0 answers
31 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 ...
user avatar
  • 593
0 votes
1 answer
46 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$ ...
user avatar
  • 593
1 vote
0 answers
55 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 ...
user avatar
2 votes
2 answers
75 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] ...
user avatar
  • 593
3 votes
2 answers
69 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 ...
user avatar
  • 593
1 vote
1 answer
135 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?
user avatar
  • 593
2 votes
1 answer
134 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 ...
user avatar
  • 593
1 vote
1 answer
129 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 ...
user avatar