Questions in category theory

learn more… | top users | synonyms (1)

0
votes
1answer
61 views

understanding programming monads through diagrams

I am trying to understand better how the category definition of monad is related to the computer science definition. nlab has a rather terse definition of Monad in terms of a bicategory. an object ...
0
votes
0answers
61 views

How is IO a monad? [migrated]

I am learning the Haskell programming language. From what I am reading, Input/Ouput (IO) raises challenges for Haskell's purity, since by definition we are interacting with the outside world. From ...
28
votes
8answers
3k views

Algebra oriented branch of theoretical computer science

I have a very strong base in algebra, namely commutative algebra, homological algebra, field theory, category theory, and I am currently learning algebraic geometry. I am a math major with an ...
5
votes
2answers
107 views

Explaining monad transformers in categorical terms

Most resource regarding categorical notions in programming describe monads, but I've never seen a categorical description of monad transformers. How could monad transformers be described in the terms ...
3
votes
0answers
135 views

Generalizing Haskell: could we replace Hask with Cat?

N.B. I asked the same question on Stack Overflow but it was suggested that it is too theoretical for this forum. It is great that Haskell allows us to walk around in the category $Hask$. But ...
7
votes
3answers
507 views

Categories a computer scientist should know about

I am a computer scientist with a CS degree from the 80's. I am learning category theory by myself. I am looking for advice about learning category theory. E.g. it is quite helpful in learning ...
3
votes
2answers
122 views

Isomorphism between algebraic data-types

I have two types of trees in Haskell, defined as the least solution of the following equations: $T_1(A) \cong 1 + A + T_1(A) \times T_1(A)$ $T_2(A) \cong 1 + A \times T_2(A) + T_2(A) \times T_2(A)$ ...
2
votes
1answer
118 views

Faithful functors vs forgetful functors: exact category-theoretic defs?

In category theory, a functor between two categories $C,D$ is a map $F$ that assigns to each object (resp. morphism) $x$ of $C$ a corresponding object (resp. morphism) $F(x)$ of $D$ by respecting the ...
1
vote
0answers
68 views

Composition series and isogeny

I'm not sure this question is appropriate for this site, but it might have some connections with computational algebra. Consider a fixed "category" $\sf{Cat}$ (in the sense of category theory, but ...
5
votes
0answers
117 views

Structures admitting directed sums and directed products?

Some structures have a property of closure by a "sum" or "product" operation. Given a family of structures $(S_i)_{i \in I}$, we can then define a new structure denoted by $\sum_{i \in I} S_i$, resp. ...
7
votes
1answer
171 views

Natural Transformations and Parametricity

In Theorems for Free!, Wadler says that the characterization of parametricity can be re-expressed in terms of lax natural transformations and this will be the subject of a further paper. Which paper ...
6
votes
0answers
137 views

Equivalence of categories of directed complete posets

I asked this question there: http://math.stackexchange.com/questions/700975/equivalence-of-categories-of-directed-complete-posets. Since I had no answer, I try here. In the book ``Domains and ...
1
vote
1answer
162 views

What's the relation between OOP and category theory?

What's the relation between OOP and category theory? Is there some related work on this topic one can read?
11
votes
1answer
156 views

Algebraically Compact Categories

I read Freyd's paper "Algebraically Complete Categories" in the famous Como90 and I have two questions about the notion of algebraic compactness he defined in that paper. (If you are not familiar with ...
4
votes
2answers
158 views

What are the uses of Limits and Colimits of Category Theory in every day problems?

I am interested in knowing how we can use the concepts of Limits and Colimits in modeling problems in every day life? Could anyone provide (Software) engineering examples, perhaps? Or describe ...
3
votes
1answer
378 views

In what sense are Scala's Try[T] and Future[T] dual?

In a recent course based on Scala I found a hint that the Scala types Try[T] and Future[T] are dual. This was explained only ...
8
votes
2answers
383 views

Full Completeness vs Full Abstraction of a program translation

Compiler verification efforts often come down to proving the compiler fully abstract: that it preserves and reflects (contextual) equivalences. Instead of providing full abstraction proofs, some ...
2
votes
1answer
177 views

Learning road map for functional programming from the viewpoint of category theory

I am now considering about studying functional programming from the viewpoint of category theory. There are a lot of books about functional programming and category theory, I want some suggestions ...
8
votes
1answer
395 views

Hyperdoctrines and Monadic Second Order Logic

This question is essentially the question I asked on Mathoverflow. Monadic Second Order (MSO) logic is second order logic with quantification over unary predicates. That is, quantification over sets. ...
4
votes
0answers
160 views

What's the connection between these two categories of games and innocent strategies?

Lately I've been reading a lot about game semantics and in particular the problem of PCF's full abstraction. I'm trying to understand how the definition from this article relates to the one found in ...
0
votes
1answer
145 views

Static structure of program

Firstly, I admit that my question is just something very blurred but I hope someone please give me some documents to read. The execution of a program $P$ can be considered as a sequence of state ...
9
votes
1answer
251 views

What is the categorical semantics of subtyping?

Starting from Curry-Howard-Lambek, there has been a nice trinity of type theories, logics, and categories. I'm curious what categorical semantics you get when you add (coercive) subtyping to a type ...
16
votes
1answer
423 views

What is the difference between arrows and exponential objects in a cartesian closed category?

In a Cartesian Closed Category (CCC), there exist the so-called exponential objects, written $B^A$. When a CCC is considered as a model of the simply-typed $\lambda$-calculus, an exponential object ...
0
votes
1answer
187 views

Newbie question: Meta-functions?

Consider a function F that takes a function and produces a function based on structure of the input function. As an example consider F that takes all functions having at least two conditionals and ...
9
votes
3answers
481 views

Is there a concept of something like co-applicative functors sitting between comonads and functors?

Any monad is also an applicative functor and any applicative functor is a functor. Also, any comonad is a functor. Is there a similar concept between comonads and functors, something like ...
5
votes
1answer
172 views

In what sense are coroutines dual to (sub)routines?

The name coroutine suggests that in some sense they should be dual to (sub)routines. Is there a real mathematical duality? I'm hoping for something like "in category theory subroutines are X and ...
18
votes
1answer
555 views

How are Futures described in terms of category theory?

Is there a useful description of futures or promises in terms of category theory? In particular, what could the categorical dual of Future be?
8
votes
2answers
194 views

Closure ordinals for inductive types with function spaces

Functors built from finite products and sums have closure ordinal $\omega$, detailed nicely in this manuscript by Francois Metayer. i.e. we can reach the inductive type $nat := \mu X. 1 + X$ by ...
11
votes
1answer
479 views

A mathematical (categorical) description of type classes

A functional language can be viewed as a category where its objects are types and morphisms functions between them. How do type classes fit in this model? I assume we should only consider those ...
17
votes
2answers
2k views

Explaining Applicative functor in categorical terms - monoidal functors

I'd like to understand Applicative in terms of category theory. The documentation for Applicative says that it's a strong lax ...
3
votes
1answer
268 views

What can the Haskell package category-extras be used for?

See here. Has anyone attempted to use this to verify category theoretic proofs? Given the relationship between categories and graphs, are there some applications with respect to graph algorithms? What ...
15
votes
3answers
1k views

Regular languages from category-theoretical point of view

I noticed that regular languages over the alphabet $\Sigma$ can be naturally thought of as a poset, and indeed a lattice. Moreover, concatenation together with the empty language $\epsilon$ defines a ...
2
votes
2answers
213 views

Difference between Stencil -structures and Cellular Automata Category-theoretically?

Definitions Stencil = "For a given point, a stencil is a pre-determined set of nearest neighbors (possibly including itself)." (source) Wikipedia's definition (source) = It ...
18
votes
4answers
912 views

Data Structure isomorphisms

Disclaimer: I am not a CS theorist. Coming from abstract algebra, I'm used to dealing with things that are equal up to a isomorphism - but I'm having a trouble translating this concept to data ...
3
votes
5answers
370 views

Advantages and specific applications of massively parallel programming thesis idea

I'm nearly graduated in computer science engineering and my thesis should discuss the massively parallel computational model of CUDA and its advantages/applications. I'm searching for an application ...
12
votes
2answers
351 views

Is there such a thing as a weak coalgebra homomorphism?

Given an endofunctor $F : Set \rightarrow Set$, we can define observation functions as functions that are polymorphic for any $F$-coalgebra, that is $obs$ is defined for any $F$-coalgebra $\langle A, ...
-6
votes
1answer
311 views

What function has the signature $ A \times \left ( B + C \right ) \rightarrow \left ( A \times B \right ) + \left ( A \times C \right ) $?

$ A \times \left ( B + C \right ) $ is isomorphic to $ \left ( A \times B \right ) + \left ( A \times C \right ) $, right? That means there's a function from one to the other and another function ...
14
votes
2answers
343 views

Proof theory of biproducts?

A category has biproducts when the same objects are both the products and coproducts. Has anyone investigated the proof theory of categories with biproducts? Perhaps the best-known example is the ...
13
votes
2answers
2k views

Category theory, computational complexity, and combinatorics connections?

I have been trying to read “Pearls of Functional Algorithm design”, and subsequently “The Algebra of Programming”, and there is an obvious correspondence between recursively (and polynomially) defined ...
11
votes
1answer
319 views

When do coherence spaces have pullbacks and pushouts?

$\newcommand{\symp}{\Bumpeq}$ A coherence relation $\symp_X$ on a set $X$ is a reflexive and symmetric relation. A coherence space is a pair $(X, \symp_X)$, and a morphism $f : X \to Y$ between ...
10
votes
2answers
276 views

Are there semi-decision procedures for this theory?

I have the following typed theory |- 1_X : X -> X f : A -> B, g : B -> C |- compose(g,f) : A -> C F, f : A -> B |- apply(F,f) : F(A) -> F(B) ...
8
votes
3answers
667 views

What is a good Category Theory-Domain Theory dictionary?

When dealing with the domain theoretic categories (say CPO and $\omega$CPO), I frequently wish for a dictionary for the language of category theory in domain theory. That is, given a concept, say ...
21
votes
2answers
887 views

A category of NP-complete problems?

Does it make sense to consider a category of all NP-complete problems, with morphisms as poly-time reductions between different instances? Has anyone ever published a paper about this, and if so, ...
22
votes
2answers
809 views

What is the folk model of linear logic?

Probably the most common application of linear types in PL is to use them to give languages which control aliasing (i.e., a linear value has a single pointer to it, more or less). But there's a ...
15
votes
3answers
2k views

Reader, Writer monads

Let $C$ be a CCC. Let $(\times)$ be a product bifunctor on $C$. As Cat is CCC, we can curry $(\times)$: $curry (\times) : C \rightarrow(C \Rightarrow C)$ $curry (\times) A = \lambda B. A \times B$ ...
28
votes
2answers
590 views

Bounded-input bijections of infinite sequences

Here is a puzzle I haven't managed to solve. I would like to know if this problem is already known, or has an easy solution. It is possible to define a bijection $ 3^\mathbb{N} \cong 5^\mathbb{N} $ ...
74
votes
5answers
4k views

Solid applications of category theory in TCS?

I've been learning a few bits of category theory. It certainly is a different way of looking at things. (Very rough summary for those who haven't seen it: category theory gives ways of expressing all ...
7
votes
1answer
159 views

Maximal subcoalgebras of an $F+1$-coalgebra corresponding to an $F$-coalgebra

This context of this question is Rutten's Universal Coalgebra, used for modelling systems. I'm interested in finding a description of a functor between different types of coalgebras corresponding to ...
4
votes
2answers
471 views

Proof of a unique homomorphism from an initial object

What is the proof that there is only one homomorphism from an initial object to another object?