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
1answer
15 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 ...
2
votes
0answers
29 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 ...
0
votes
0answers
33 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. ...
1
vote
0answers
24 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 ...
0
votes
1answer
10 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$ ...
1
vote
0answers
39 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 ...
2
votes
2answers
43 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] ...
1
vote
0answers
30 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 ...
1
vote
1answer
42 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?
2
votes
1answer
47 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 ...
1
vote
1answer
71 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
vote
1answer
48 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$,...
1
vote
0answers
45 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 ...
1
vote
0answers
25 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; ...
0
votes
1answer
63 views

Composition of compostion as a functor

"Composition of Composition" (i.e., (.) . (.)) in Haskell), has type ...
0
votes
1answer
106 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 ...
0
votes
1answer
381 views

“Left identity” of Monad laws in Haskell is wrong

Monad laws in Haskell ...
3
votes
1answer
70 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 ...
1
vote
0answers
38 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 ...
2
votes
1answer
87 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
36 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 ...
11
votes
4answers
1k 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
100 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
72 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
64 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
169 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
45 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
53 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
44 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
97 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
45 views

Expressing that a functor is natural

The Haskell List: Type -> Type constructor implements the Functor typeclass with function ...
6
votes
1answer
230 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
561 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 ...
6
votes
1answer
336 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 ...
2
votes
0answers
68 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 ...
3
votes
1answer
250 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
46 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
488 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
119 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
114 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
553 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 ...
4
votes
1answer
554 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 ...
13
votes
2answers
543 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
128 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
172 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
119 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
112 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 ...
2
votes
1answer
495 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
137 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 ...