Questions tagged [ct.category-theory]
Questions in category theory
122
questions
2
votes
0
answers
57
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 ...
0
votes
0
answers
29
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-...
- 2,571
3
votes
1
answer
123
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, (...
- 199
3
votes
1
answer
67
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 ...
- 921
4
votes
3
answers
318
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 ...
- 41
17
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 ...
- 244
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 ...
- 193
2
votes
1
answer
213
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 ...
- 193
6
votes
0
answers
111
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 ...
- 93
4
votes
2
answers
176
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 ...
- 244
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 ...
- 244
1
vote
0
answers
63
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 ...
- 11
3
votes
1
answer
88
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.
- 246
4
votes
2
answers
251
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 ...
- 111
6
votes
3
answers
491
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)$
...
- 244
3
votes
1
answer
147
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 ...
- 32.4k
2
votes
0
answers
119
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 ...
- 1,653
5
votes
2
answers
183
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
135
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 ...
- 921
2
votes
1
answer
78
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,653
1
vote
1
answer
60
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 ...
- 133
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 ...
- 357
10
votes
2
answers
566
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-...
- 28.3k
0
votes
1
answer
129
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 ...
- 26
10
votes
0
answers
212
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 ...
- 2,040
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 ...
- 103
3
votes
0
answers
104
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
181
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 "...
- 32.4k
17
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 ...
- 28.3k
8
votes
3
answers
3k
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?
- 2,359
6
votes
1
answer
142
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 ...
- 28.3k
-2
votes
1
answer
81
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$ ...
- 28.3k
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 ...
- 105
7
votes
0
answers
234
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
- 163
5
votes
2
answers
252
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.
- 28.3k
8
votes
2
answers
325
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 ...
- 13.7k
-1
votes
1
answer
125
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 ...
- 28.3k
5
votes
0
answers
179
views
On the interpretation of coinduction in type theory
The notion of (co)datatype can be modeled satisfactorily in category theory as fixed-points of polynomial functors. Then, (co)induction principles are derived from initial algebras/terminal ...
- 921
2
votes
0
answers
561
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 ...
CommunityBot
- 1
8
votes
2
answers
805
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 ...
- 921
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 ...
- 146
9
votes
1
answer
206
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 \...
- 1,653
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 ...
CommunityBot
- 1
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 ...
- 575
3
votes
0
answers
116
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 ...
- 28.3k
4
votes
2
answers
672
views
What does the category of RDF models look like in Institution Theory?
The Question in short
Here is the question in its pure form. Details of my reasoning can be found below.
The RDF1.1 spec semantics defines a model to consist of a set IR of objects and IP of ...
CommunityBot
- 1
11
votes
0
answers
208
views
Do Banach spaces and linear contraction maps form a model of ILL with an exponential?
Recently, I read on the nLab that the category of Banach spaces and linear contractions is small complete, small cocomplete, and monoidal closed.
This means that Banach spaces and short linear maps ...
- 32.4k
2
votes
1
answer
82
views
Does an initial algebra for a class have to belong to the class itself?
In the context of algebraic data types, a concept of initial algebras is usually defined, e.g., in the following way:
An algebra $S$ is initial in a class $C$ of algebras iff for every $A\in C$ ...
- 28.3k
7
votes
2
answers
301
views
The chromatic number of a graph as a functor
I was fooling around with some concept and was wondering if this viewpoint is explored at all. Let INJ-GRAPH be the subcategory of graphs (with morphisms as homomorphisms) whose morphisms consist only ...
- 1,653