The ct.category-theory tag has no wiki summary.
-4
votes
0answers
40 views
The List functor [closed]
I have been reading some notes on Category Theory. One question that is posed is to verify the definition of List is a functor...
List(gof) = (List g) o (list f)
I can see this makes sense in ...
7
votes
1answer
145 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 ...
9
votes
1answer
152 views
What is the difference between arrows and exponential types in the 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
138 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 ...
4
votes
2answers
167 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
132 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 ...
17
votes
1answer
389 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
129 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 ...
10
votes
1answer
323 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 ...
11
votes
1answer
405 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
191 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 ...
14
votes
3answers
562 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
161 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
601 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
323 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
321 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
283 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 ...
13
votes
2answers
318 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 ...
8
votes
1answer
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
298 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
233 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
568 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 ...
20
votes
2answers
770 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, ...
20
votes
2answers
674 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
563 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} $ ...
60
votes
5answers
3k 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 ...
6
votes
1answer
149 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
419 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?
