Skip to main content
OverflowAI is here! AI power for your Stack Overflow for Teams knowledge community. Learn more

Questions tagged [ct.category-theory]

Questions in category theory

Filter by
Sorted by
Tagged with
-1 votes
1 answer
88 views

What is a model theory / category theory basis of System F-omega that corresponds to what programmers actually do?

In what books or papers is it explained how the type constructions of a functional programming language correspond to category theory, and what are the models (a rigorous semantics) of programs of ...
winitzki's user avatar
  • 442
-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: ...
Gergely's user avatar
  • 123
0 votes
0 answers
56 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 ...
Corbin's user avatar
  • 271
1 vote
0 answers
84 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: ...
Alecs's user avatar
  • 11
2 votes
0 answers
75 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 ...
Ilk's user avatar
  • 920
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 ...
Johan Thiborg-Ericson's user avatar
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 ...
Johan Thiborg-Ericson's user avatar
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 ...
vigenary's user avatar
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, (...
sparusaurata's user avatar
1 vote
0 answers
111 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 ...
LaR's user avatar
  • 335
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 ...
LaR's user avatar
  • 335
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 ...
vigenary's user avatar
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 ...
TetraDex's user avatar
3 votes
1 answer
92 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.
LaR's user avatar
  • 335
4 votes
2 answers
306 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 ...
Ryan's user avatar
  • 43
3 votes
1 answer
171 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 ...
Ilk's user avatar
  • 920
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 ...
Max New's user avatar
  • 1,695
5 votes
2 answers
194 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 ...
Max New's user avatar
  • 1,695
4 votes
1 answer
142 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 ...
jpt4's user avatar
  • 81
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 ...
EDJ's user avatar
  • 133
1 vote
1 answer
72 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 ...
EDJ's user avatar
  • 133
11 votes
2 answers
585 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-...
daniel gratzer's user avatar
0 votes
1 answer
131 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 ...
Ari Fordsham's user avatar
10 votes
0 answers
223 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 ...
gasche's user avatar
  • 2,040
4 votes
3 answers
374 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 ...
Julian G.'s user avatar
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 ...
Couchy's user avatar
  • 195
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 ...
alessio-b-zak's user avatar
7 votes
1 answer
196 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 "...
xrq's user avatar
  • 1,175
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 ...
Henry Story's user avatar
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 ...
Siddharth Bhat's user avatar
-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$ ...
user65526's user avatar
  • 105
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 ...
user65526's user avatar
  • 105
7 votes
0 answers
248 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
Eric Bond's user avatar
  • 163
5 votes
2 answers
265 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.
user1868607's user avatar
  • 1,019
8 votes
2 answers
351 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 ...
xrq's user avatar
  • 1,175
-1 votes
1 answer
129 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 ...
PhD's user avatar
  • 5,325
2 votes
0 answers
615 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 ...
Yamar69's user avatar
  • 684
8 votes
2 answers
853 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 ...
Henry Story's user avatar
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 ...
Turion's user avatar
  • 616
9 votes
1 answer
212 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 \...
Kevin Clancy's user avatar
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 ...
Henry Story's user avatar
3 votes
0 answers
121 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 ...
Łukasz Lew's user avatar
  • 1,187
11 votes
0 answers
215 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 ...
Neel Krishnaswami's user avatar
4 votes
2 answers
689 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 ...
Henry Story's user avatar
2 votes
1 answer
83 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$ ...
user avatar
7 votes
2 answers
308 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 ...
MT_'s user avatar
  • 173
4 votes
1 answer
183 views

What are values relative to Hask?

According to ncatlab's page on category theory and haskell, "we can identify a subset of Haskell called Hask that is often used to identify concepts used in basic category theory. One considers ...
lightning's user avatar
  • 433
3 votes
2 answers
330 views

Moggi's computational metalanguage

In Notions of Computation and Monads Moggi models the notion of a computation of type $A$, $TA$, using a monad $T$. Among other things this ensures the $T\eta$ rule: $$\frac{x: A \vdash a:TB}{x:A \...
Andrew Bacon's user avatar
17 votes
0 answers
279 views

Using Dependent Type Theory for Categories that are not LCCC

I have recently been working with polynomial functors and monads based mostly on Gambino-Kock. There they define polynomial functors in a Locally Cartesian Closed Category (LCCC) and extensively use ...
Max New's user avatar
  • 1,695
6 votes
1 answer
219 views

Can all structurally recursive functions be written without explicit recursion using a catamorphism/fold?

In particular, I am thinking of a function which involves conditionals changing the recursive behavior and multiple F-algebras. ...
lightning's user avatar
  • 433