Questions tagged [category-theory]

Category theory is a branch of abstract mathematics concerned with exposing and describing the underlying structure of logical and mathematical systems. Concepts from category theory have proven to be extremely effective as tools for structuring both the semantics of programming languages and programs themselves. Various category theoretic structures are used as tools for abstraction in programming, including functors, monads, and algebras.

Filter by
Sorted by
Tagged with
0 votes
0 answers
19 views

What Category theory object makes Array in JavaScript chainable?

I don't know much about Category theory but I bet array chaining has a name in category theory. Is it monoid? I was asking a long time ago about a proof of concept library that I've written and ...
jcubic's user avatar
  • 62.3k
1 vote
1 answer
42 views

initial and terminal object make the category unique?

I've been reading Carli Masimo book "Functional programming in Kotlin by tutorials" and there is a sentence not clear for me. Not all categories have initial and terminal objects but, if ...
user avatar
1 vote
1 answer
83 views

cats effect evaluates only the final for coprehension and ignores rest

I'm a newbie to functional programming and cats effect. Started practicing cats effect 3 with the below code package com.scalaFPLove.FabioLabellaTalks import cats.effect.IOApp import cats.effect.{IO, ...
Somu's user avatar
  • 28
2 votes
2 answers
162 views

Monad and Functor law for Monad and Functor type class in Haskell

I am a somewhat experienced functional programmer, but I have always been confused by the statement “A monad is just a monoid in the category of endofunctors” and the actual implementation of monads/...
SmoothTraderKen's user avatar
6 votes
1 answer
168 views

Deriving a monad from a cofree comonad

Edward Kmett writes on his blog that using the Co newtype (from the kan-extensions package), it's possible to derive a Monad from any Comonad. I'd like to learn how to mechanically do this for any ...
Johannes Riecken's user avatar
0 votes
0 answers
44 views

Install SML for Computational Category Theory

I am following Computational Category Theory and learning Standard ML. However SML has changed since the book was published, and I am having a little trouble executing the examples/exercises (for ...
Julián Villaquirá's user avatar
4 votes
1 answer
130 views

Is the type constructor `Maybe (BTree a)` a monad?

Question Define the type constructor F in Haskell like this: data BTree a = Leaf a | Branch (BTree a) (BTree a) data F a = F (Maybe (BTree a)) The type constructor F is polynomial, so it is a ...
winitzki's user avatar
  • 3,179
2 votes
2 answers
128 views

How do I prove two applications of the absurd pattern result in the same in Cubical Agda?

Heavy category theory (agda-categories) related question. I'm trying to define a natural transformation and prove its naturality square commutes. Essentially, the error I run into is that two "...
André Muricy's user avatar
2 votes
0 answers
120 views

Is there a semigroup/monoid in the context of a monad?

I'm giving my tensor operations a notion of sharing, using a monadic context Shared (implemented as State Nat), so (+) : Tensor F64 -> Tensor F64 -> Tensor F64 becomes (+) : Tensor F64 -> ...
joel's user avatar
  • 6,471
7 votes
1 answer
127 views

Can one simplify the Codensity monad on Maybe?

The codensity monad on a type constructor f is defined by: newtype C f a = C { unC ∷ forall r. (a → f r) → f r } It is well known that C f is a monad for any type constructor f (not necessarily ...
winitzki's user avatar
  • 3,179
0 votes
2 answers
103 views

In Scala cats-laws, why is the functor composition law different from canonical definition?

The (covariant) functor definition in cats-laws looks like this: def covariantComposition[A, B, C](fa: F[A], f: A => B, g: B => C): IsEq[F[C]] = fa.map(f).map(g) <-> fa.map(f.andThen(...
tribbloid's user avatar
  • 3,958
4 votes
1 answer
117 views

Why doesn't Haskell's `Functor` instance define a "return-like" function? [duplicate]

In Category Theory, a Functor is a morphism between categories, that is, it maps each object in category A to another object in B, as well as mapping each morphism C -> D onto the respective ...
Al Sneed's user avatar
0 votes
1 answer
72 views

Naturality of product functor morphisms

In https://www.cs.ox.ac.uk/ralf.hinze/LN.pdf On page 10, equations (13) and (14) it seems to me that outl on the left of the equations is not the same outl as on the right (likewise for outr). I ...
docjosh's user avatar
  • 85
1 vote
2 answers
68 views

Are there any functions that are computable but not curriable?

Sorry if I'm a bit lost. I've recently started learning about different programming language paradigms and I found that all texts presuppose that all functions written in a programming language are ...
David Velasco Pérez's user avatar
4 votes
2 answers
174 views

Why is FunctionK not the same as a Natural Transformation

The cats documentation on FunctionK contains: Thus natural transformation can be implemented in terms of FunctionK. This is why a parametric polymorphic function FunctionK[F, G] is sometimes referred ...
Joe's user avatar
  • 1,489
5 votes
1 answer
258 views

Can `Fix` and `(,)` be seen as functors in some sense?

I've been wondering what a complete, all-encompassing context for instance Functor (f :.: g) would be. The immediate thought that pops into my head is: newtype (f :.: g) a = Comp (f (g a)) instance (...
fluffyyboii's user avatar
6 votes
2 answers
354 views

Confused about why all morphisms for a monoid are not the same as the identity morphism

I am busy reading Bartosz Milewski's Category Theory book for programmers and I'm struggling with the depiction of non-identity morphisms when moving between describing a monoid as a set and a monoid ...
sdb's user avatar
  • 109
5 votes
1 answer
277 views

How to understand the universal quantification in Yoneda's natural isomorphism?

While learning about the Yoneda lemma, I came across the following encoding of the underlying natural isomorphism in Haskell: forward :: Functor f => (forall r . (a -> r) -> f r) -> f a ...
michid's user avatar
  • 10.6k
4 votes
2 answers
259 views

What is a cocartesian comonoid, and what is a cocartesian comonoidal functor?

I've been experimenting with monoids and Distributives lately, and I think I've found something of interest (described in my answer) - are these already known structures? (I've been unable to find any ...
janet's user avatar
  • 221
7 votes
1 answer
192 views

Does the term "Functor" in Prolog have any relation to the term taken from Category Theory?

I started to learn Prolog and I just read that the atom at the beginning of an structure is usually called functor. I'm also familiar with the term functor from Category Theory and Functional ...
Gabriel Santana Paredes's user avatar
1 vote
1 answer
121 views

Lawvere's fixed point theorem in agda

I was struggling to prove a more basic version of lawvere's fixed point theorem in agda. Precisely I am trying to figure out the proof for the bottom theorem. surjective : {A : _} {B : _} → (A → B) → ...
Ace shinigami's user avatar
2 votes
1 answer
134 views

In depth understanding of Monad

At one time, I thought I understood Monad. However, when I try to connect my understanding of code to the piece of theory, I found myself still not clear. So here it is: part 1. Here is the popular ...
Max Li's user avatar
  • 551
11 votes
2 answers
364 views

Why are traversals defined over Applicatives, fundamentally?

I've been on a bit of a "distilling everything to its fundamentals" kick lately, and I've been unable to find clear theoretical reasons for how the Traversable typeclass is defined, only ...
janet's user avatar
  • 221
2 votes
1 answer
197 views

The identity monad as a free monad

The functor of the identity monad can be defined as: data Identity a = Identity a Because this monad is free, an alternative definition is the following: data Term f a = Pure a | Impure (f (Term f a))...
Bob's user avatar
  • 1,713
2 votes
2 answers
283 views

What is the mathematical theory or theorem underlying join of monad?

For example: Maybe (Maybe Bool) -> Maybe Bool Just (Just True) -----> Just True Just (Just False) ----> Just False Just (Nothing) -------> Nothing Nothing ------------...
Lionhairdino L.'s user avatar
10 votes
1 answer
301 views

Did this construction of free(freer?) monad works?

In the past 2 years, I was interested in using free monad to helping me to solve practical software engineering problem. And came up my own construction of free monad using some elementary category ...
yuxuanchiadm's user avatar
3 votes
3 answers
482 views

How to implement memoization in Scala without mutability?

I was recently reading Category Theory for Programmers and in one of the challenges, Bartosz proposed to write a function called memoize which takes a function as an argument and returns the same one ...
Gabriel Santana Paredes's user avatar
6 votes
2 answers
204 views

Indexed Initial algebras for GADTs

In his paper Generics for the Masses Hinze reviews encoding of data type. Starting from Nat data Nat :: ⋆ where Zero :: Nat Succ :: Nat → Nat It can be viewed as an initial algebra NatF Nat -&...
nicolas's user avatar
  • 9,549
9 votes
1 answer
503 views

The list monad is not a free monad but …

On page 12 of One Monad to Prove Them All, it is written that "a prominent example [of container] is the list data type. A list can be represented by the length of the list and a function mapping ...
Bob's user avatar
  • 1,713
2 votes
3 answers
157 views

Looking for a typeclass where category objects are partially consumable (chemical engineering)

Question I'm looking to describe processes in chemical engineering that that transmute some substances into others. Is there a category that describes morphisms that consume "substances"? ...
idomorphism's user avatar
4 votes
1 answer
191 views

Mergeable with sum and product in type indices

Is there anything in Haskell resembling the following type class? class Mergeable (f :: Type -> Type -> Type) where merge :: f a b -> f c d -> f (a, c) (Either b d) In particular, ...
Sridhar Ratnakumar's user avatar
0 votes
1 answer
69 views

Morphism, product, coproduct operator precedence and associativity

I am writing a parser that will parse a simple functional toy language. I'm having tough time with operator precedence and associativity of morphism, product and coproduct operators. My toy language ...
Cristian's user avatar
  • 654
6 votes
2 answers
165 views

`refold :: Functor s => (a -> s a, a) -> (s b -> b) -> b` as a morphism between universal types

Various recursion scheme boil down to specific instantiation of refold refold :: Functor s => (s b -> b) -> (a -> s a) -> a -> b refold f g = go where go a = f (fmap go (g a)) What ...
nicolas's user avatar
  • 9,549
1 vote
1 answer
76 views

Why is sum-type a disjunction in the Curry-Howard correspondence?

According to the Curry-Howard correspondence the sum-type aka tagged-union is the equivalent of disjunction, logical OR Why is this the case? Is it not closer to XOR? (a or b) implies that it could be ...
mazin's user avatar
  • 395
0 votes
1 answer
80 views

Can we transform a graph in a way that applying DFS to the new graph would result in the same traversal order as applying BFS on the first graph?

This question is purely theoretical. Let's say you have a graph A, a Depth-First Search algorithm and a Breadth-First Search that both searches a graph for nodes matching a given predicate and ...
WhiteMist's user avatar
  • 885
13 votes
3 answers
723 views

Are codatatypes really terminal algebras?

(Disclaimer: I'm not 100% sure how codatatype works, especially when not referring to terminal algebras). Consider the "category of types", something like Hask but with whatever adjustment ...
Sylvain Hubert's user avatar
1 vote
2 answers
795 views

Intersection types with interfaces fails to throw TypeScript error

By mixing TypeScript types with interfaces in an intersection, I seem to loose the stricter behaviour of interfaces in my code. I want to be able to compose types using intersections (such that I can ...
shennan's user avatar
  • 10.9k
2 votes
2 answers
189 views

How are Haskell Monad laws derived from Monoid laws?

The laws for monoids in the category of endofunctors are: And the Haskell monad laws are: Left identity: return a >>= k = k a Right identity: m >>= return = m Associativity: m >>= (\...
Ziyang Liu's user avatar
2 votes
2 answers
146 views

Definition of Category and internal category in coq

I have a two-part question. Goal: I want to define the notion of a category internal to a given category. I came up with the following simple code, that however produces an inexplicable error message,...
santker heboln's user avatar
8 votes
1 answer
188 views

How to prove basic sequence properties

As I understand it, one way to express that something is a free monoid is with a class like this: class (Foldable s, forall a. Monoid (s a)) => Sequence s where singleton :: a -> s a and the ...
dfeuer's user avatar
  • 48.1k
7 votes
1 answer
82 views

What are those class extensions for the Cartesian class for?

The Cartesian class from the constrained-category project is for categories, products of objects in which are objects in the same category yet again. I wonder about the classes Cartesian extends: ...
Zhiltsoff Igor's user avatar
2 votes
1 answer
294 views

Free theorem for fmap

Consider the following wrapper: newtype F a = Wrap { unwrap :: Int } I want to disprove (as an exercise to wrap my head around this interesting post) that there’s a legitimate Functor F instance ...
Zhiltsoff Igor's user avatar
20 votes
3 answers
972 views

Is Haskell's `Const` Functor analogous to the constant functor from category theory?

I understand that many of the names in Haskell are inspired by category theory terminology, and I'm trying to understand exactly where the analogy begins and ends. The Category Hask I already know ...
Benjamin Bray's user avatar
5 votes
4 answers
577 views

Can the composite pattern be used to generate HTML from a tree and handle the indenting as well, or this inherently not possible?

I watched this video on the composite pattern, where the main example is how to use the pattern as a mean to generate HTML code from a tree structure describing a todo list where each item can be in ...
Enlico's user avatar
  • 23.6k
3 votes
1 answer
145 views

What is the relation between ixmap, Array, and contravariant functor?

tl;dr Given the similarity between ixmap's signature and contramap's signature, I'd like to understand if Array i e is a contravariant functor in its first type argument or, at least, how the two ...
Enlico's user avatar
  • 23.6k
1 vote
1 answer
136 views

Is every type constructor (`Type -> Type`) some kind of functor

It is well-known that a type constructor with kind Type -> Type (in System F-omega) is only a Functor if it implements a function (a -> b) -> f a -> f b. This is a lawless functor though, ...
Labbekak's user avatar
  • 517
2 votes
2 answers
240 views

Recursion scheme allowing dependencies between recursive calls (an ordered catamorphism?)

I'm interested in a higher-order way (recursion scheme) to write recursive code in which there might be dependencies between recursive calls. As a simplified example, consider a function that ...
trpnd's user avatar
  • 435
3 votes
1 answer
594 views

Category Theory fundamentals

I am looking for references on Category Theory that are mature (== at least 5 years old) at a level of university education (not post-doctorate, ultra symbolic introductions) start from the basics (...
TFuto's user avatar
  • 1,361
0 votes
1 answer
74 views

Meaning of ⊗ applied to morphisms

I think I understand what ⊗ means when applied to objects (such as M ⊗ M), but what does it mean when applied to morphisms (such as η⊗1). Is it just composition?
DMJ's user avatar
  • 41
4 votes
1 answer
168 views

Understanding of bifunctor from Category Theory for Programmers - Ch. 8

I'm going mental with Chapter 8 from Category Theory for Programmers. In section 8.3, Bartosz defines this type newtype BiComp bf fu gu a b = BiComp (bf (fu a) (gu b)) Here, if I'm understanding a ...
Enlico's user avatar
  • 23.6k

1
2 3 4 5
9