Questions tagged [ct.category-theory]

Questions in category theory

Filter by
Sorted by
Tagged with
16 votes
3 answers
673 views

Are there knot theoretic formulations of NP complete problems?

Are there NP complete(or even NP-hard, or NP) problems that have good topological properties to study. Do NP problems have knot theoretic formulations? We know about #$P$ results about the Jones ...
-1 votes
1 answer
127 views

What theorems are interesting in a monad?

In a monad, one can prove that the Kleisli composition is associative, and eta is its right and left unit, this is the famous monoid in the endofunctor category: ...
0 votes
0 answers
53 views

What is Shutt abstractiveness?

In software development, there is a pre-formal notion of abstraction. Several attempts have been made to formalize it. In particular, what is Shutt abstraction, or Shutt abstractiveness, and how does ...
1 vote
0 answers
83 views

Abstract domain monad

I was reading old lecture from a CS course at Cornel and I have some doubts about the following at 2.4 It defines how to transform domains between each other via a Galois Insertion, more formally: ...
11 votes
4 answers
1k 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 ...
1 vote
0 answers
82 views

Is the Category of $(* \to)^n *$-kinded types freely generated from the discrete graph with $n$ nodes?

In Introduction to Higher Order Categorical Logic part 1, section 4, Lambek defines an adjunction between $\mathbf{Graph}$, the category of graphs and graph homomorphisms, and the category of ...
2 votes
0 answers
74 views

Categorical consequences in practical algorithms outside type theory

Most of my exposure to using categorical results to design algorithms, is through modularity in functional programming. I am wondering whether there are examples where the proof of existence of ...
0 votes
0 answers
31 views

Which family of bicartesian closed functors can define the semantics of simply typed lambda calculus with products and sums

Given any bicartesian closed category $\mathbf{C}$, any natural number $n \geq 0$, and any vector $\boldsymbol{A} \in \mathbf{C}^n$ with $n$ objects $A_1, A_2, … A_n \in \mathbf{C}$, how can I define ...
22 votes
3 answers
3k 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 co-...
3 votes
1 answer
126 views

Can the initial algebra of a 2-variable polynomial functor be computed on the diagonal?

Given a polynomial functor $F$, its initial algebra is denoted by $\mu X.F(X)$. Now, if $F$ is a 2-variable polynomial functor, $Y \mapsto \mu X.F(X,Y)$ turns out to be functorial and we can, again, (...
3 votes
1 answer
75 views

Is Linear Evaluation Parametric?

Parametric functions satisfy free theorems which state that they take related arguments to related results. This is formalized by the notion of parametric transformation introduced in section 5 of ...
4 votes
3 answers
372 views

Kleisli-like category for applicatives?

I am wondering if there is a good way to complete the following analogy: monad : Kleisli category :: applicative functor : ?? That is, a given monad T on a ...
19 votes
2 answers
1k 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 ...
1 vote
0 answers
110 views

Closely related (?) arrows in categories

Let $f: x\to y$ and $f':x' \to y'$ be arrows in a category ${\bf C}$, where $x\cong x'$ and $y\cong y'$. Assume that for all isomorphisms $v: x \to x'$ and $u: y\to y'$, the corresponding diagram ...
2 votes
1 answer
220 views

Fixpoint of a functor in the category of embeddings

In Section 5.2 of the text on Domain Theory by S. Abramsky and A. Jung, it is mentioned that: "Suppose we are given a recursive domain equation $X \cong F(X)$ where the right hand side defines a ...
6 votes
0 answers
114 views

List Functions That Don't Depend on Length

Intuitively, a polymorphic function of type $f : \forall a. [a] \to [a]$ cannot inspect the type of its elements. This intuition can be captured formally using either natural transformations or ...
5 votes
2 answers
189 views

Relating functors to relational functors with the parametricity translation

$\newcommand{\Type}{\text{Type}}\newcommand{\id}{\text{id}}\newcommand{\map}{\text{map}}$ In attempting to answer the question: Rigorous proof that parametric polymorphism implies naturality using ...
1 vote
0 answers
65 views

Mappings that are not functors in category theory

Let C be a category and let $F$ be a mapping on C. Assume that $F$ is defined for all objects of C. However, on the arrows of C the mapping $F$ does not always behave like a (covariant) functor. For ...
3 votes
1 answer
90 views

Does ${\bf CPO}$ have $\omega$-colimits?

Does the category ${\bf CPO}$ have $\omega$-colimits? By ${\bf CPO}$ I mean the category that has as objects the $\omega$-complete pointed partial orders and as arrows $\omega$-continuous functions.
4 votes
2 answers
296 views

Composition with recursion in functions between types

I always understood functions in functional programming to be modeled by morphisms in the category of types, where any powerful function you write in your code is a morphism that is the composition of ...
6 votes
3 answers
505 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)$ ...
3 votes
1 answer
168 views

Exposition of categorical models of type theory from type-theoretic perspective

Are there any formalizations or expositions of categorical models from type theoretic point-of-view? What I have in mind to get a better grasp of categorical models of dependent types, treating ...
2 votes
0 answers
132 views

Why Multiple Clocks in Guarded Dependent Type Theories?

The main purpose of clocks in guarded type theories (originating in Atkey & McBride ICFP 2013) is so that we can define coinductive constructions from guarded recursive definitions. Semantically ...
5 votes
2 answers
193 views

Commutativity of Clock Quantification and Disjunction/Existential Quantification in Guarded Type Theories

In Atkey & McBride ICFP 2013, they extend a simple type theory with guarded recursion indexed by clock variables $\triangleright^k$ and a clock quantification $\forall k. A$ that conveniently ...
4 votes
1 answer
141 views

Is there a relation between the techniques used by Dan Willard, versus those of Brown and Palsberg, to exclude diagonalization?

This question extends my inquiry from a previous post [0]. Dan Willard's Self-Justifying Axiom Systems/Self-Verifying Theories [1] and Brown and Palsberg's self-interpreter for F-Omega [2] both employ ...
2 votes
1 answer
79 views

Question about "Free-ness" of Free SCWF

In Category with Family by Castellan et al., they introduce the concept of Free SCWF as correspondence of STLC with base type. Seemingly, they define Free B-SCWF as the synonym of initial B-SCWF. My ...
1 vote
1 answer
70 views

Question in relating STLC and Free CCC

In Lambek's Intro to Higher Order Cat Logic, Chapter 1 Section 4 introduces the free construction (upon graph) My question is, if I want to have STLC + (fake/incomplete) boolean type, how do I have ...
19 votes
3 answers
2k views

"The" category of Turing machines?

Disclaimer: I know very little about complexity theory. I'm sorry but there is really no way to ask this question without being (terribly) concise: What should be the morphisms in "the" category ...
11 votes
2 answers
583 views

Induction-recursion in models other than $\mathbf{Set}$

It is well-known that various flavors of induction-recursion are consistent*. Typically, this is proven by showing that the standard model of type theory in sets can be extended to include induction-...
0 votes
1 answer
130 views

Why can't opaque optics form a category?

The optics Haskell package is an alternative to the famous lens package. lens uses a van ...
10 votes
0 answers
222 views

What is the "standard" lambda-calculus model for bicartesian closed categories?

(I'm familiar with the lambda-calculus, less so with its categorical models.) It is well-known that cartesian-closed categories are in tight correspondence to the simply-typed lambda-calculus with ...
25 votes
3 answers
4k 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 ...
3 votes
0 answers
106 views

CCCs, computational calculi and point-surjectivity

The models of some computational calculi are in a correspondence with Cartesian Closed Categories with an object $U$ that has some relationship to its exponential object $U^U$ e.g. a retraction ...
7 votes
1 answer
191 views

"Interesting" categories whose internal logic is a dependent-linear type theory

Dependent-linear type theories may be a functional programmer's dream, but is it categorically interesting, i.e. is it the internal language of an "interesting" category? By "...
18 votes
2 answers
2k views

Proof relevance vs. proof irrelevance

I want to use use Agda to help me write proofs, but I am getting contradictory feedback about the value of proof relevance. Jacques Carette wrote a Proof-relevant Category Theory in Agda library. But ...
8 votes
3 answers
4k 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?
6 votes
1 answer
146 views

Given a domain, how do we build a language whose denotation is the domain?

Say we have an arbitrary domain $D$ with a countable basis $B$. Now, how do i build a "language" whose "denotation" lives in the domain? My understanding is that Dana Scott ...
-2 votes
1 answer
84 views

Forming ordered pairs using monads and doing without the Kuratowski encoding of ordered pairs

Suppose we have a set $S$ of constants of the Simply-Typed Lambda Calculus (STLC) various types, and the operation of union $\cup$ which takes two constants and forms their union. For example, $S$ ...
0 votes
0 answers
87 views

Is this a reader monad?

I'm unsure whether the following three equations constitute a valid instance of a reader/environment monad on the simply-typed lambda calculus, where $\alpha$ is any type (I subscript some terms with ...
7 votes
0 answers
243 views

Category theory lambda cube?

If simply typed lambda calculus corresponds to cartesian closed categories, what types of categories do other calculi in the lambda cube correspond to? https://en.m.wikipedia.org/wiki/Lambda_cube
5 votes
2 answers
258 views

Categorical equivalent of higher order logic

From Simply typed lambda calculus and higher order logic, I get the impression that HOL is STLC + equality + equality axioms. I was wondering if there is a particular kind of category modelling this.
8 votes
2 answers
346 views

Does the Hindley-Milner type system (i.e. STLC with prenex polymorphism) have a category-theoretic model?

It is well known that any CCC (cartesian closed category) is a model of the simply-typed $\lambda$-calculus. It is less well known that System F admits a categorical model, but it is also well studied ...
-1 votes
1 answer
128 views

Are all computable functions monoidal from a category theory POV? [closed]

I have been studying some category theory only to understand the "why" behind the various categorical constructs we use ("borrow") in the world of functional programming. One of ...
2 votes
0 answers
605 views

Can Category Theory help us prove P != NP?

Scott Aaronson, in this funny April Fools’ Day post, introduces a fictionalized $P \neq NP$ Proof and, among other things, he says that the proof make use of Higher topos theory to solve the biggest ...
8 votes
2 answers
839 views

What category are Tagless Final Algebras final In?

The Haskell and Scala community have been very enamored recently with what they call tagless final 'pattern' of programming. These are referenced as dual to initial free algebras, so I was wondering ...
14 votes
2 answers
2k views

Category-theoretic treatment of diffs, patches and merging?

Is there a category of patches that looks roughly like this: The objects are strings in some base alphabet The morphisms are edit scripts ("diffs" or "patches") between the strings I'm interested in ...
9 votes
1 answer
211 views

Understanding the Beck-Chevalley Condition

I've been reading through Bart Jacobs' "Categorical Logic and Type Theory", and lemma 1.8.9 has me stumped. The lemma is stated as follows: Let $p : \mathbb E \to \mathbb B$ and $q : \mathbb D \to \...
113 votes
7 answers
10k 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 ...
10 votes
2 answers
1k views

What logic correponds via Curry-Howard to a Monad?

According to Moggi's 1991 paper "Notions of computation and monads" one can represent monadic equational logic with the well known monad $(T, \eta, \mu)$ with T an functor and the two natural ...
3 votes
0 answers
120 views

What's the example of natural transformation in 'Type" that is not a parametric function?

Take a type theory of your choice (perhaps System Fω). Parametric functions are known to be natural transformations in 'Type' category. Yet not every natural transformation in 'Type' is a polymorphic ...