Michael Arntzenius irl. PL design, math, calligraphy, &c.

Postdoc at UC Berkeley working on incremental computation, DB ⋈ FP, etc.

Web: http://www.rntz.net
Twitter: https://Twitter.com/arntzenius
cohost: rntz
email: daekharel@gmail.com

Last Notes

- reply

Ah yeah, I just reread my initial post and realized I use "C" without explanation. "C" is meant to stand for a typeclass like Expr, not a functor F, for instance:
Expr ≅ Fa → a for Fa = Int+(a×a)
Stream elem a ≅ a → Fa for Fa = Int × a
so when Ca = Fa → a we get
(1) ∀α. C α → α ≅ ∀α. (Fα → α) → α (Church encoding)
and when Ca = a → Fa we get
(2) ∃α. C α × α ≅ ∃α. (α → Fα) × α (co-Church encoding?)

2026-06-24 23:25:47 UTC

- reply

I don't think (∃x. x -> F x) is actually a F-coalgebra itself! For that I'd need:
(∃x. x -> F x) -> F (∃x. x -> F x)
and I don't see how. The terminal coalgebra is actually (∃x. x * (x -> F x)), I think. So the conatural numbers should be (∃x. x * (x -> Maybe x)), I think.

2026-06-24 23:09:08 UTC

- reply

Ok, I think I worked it out:
(1) is an initial algebra when C a ≅ Fa → a for some functor F.
(2) is a terminal coalgebra when C a ≅ a → Fa for some F. Example:
class Stream elem a where
get: a → elem
step: a → a
Stream Int a ≅ a → Int × a. Then (∃a. Stream Int a × a) is a terminal coalgebra for (Int × _).

2026-06-24 18:35:05 UTC

class Expr a
add: a × a → a
lit: Int → a
The type of expressions in this language is definable by Church-encoding:
∀α. Expr α → α
Since Expr a ≅ Fa → a for Fa = Int+(a×a), this corresponds to initial F-algebras. But it's definable for *any* class C, not just for F-algebras. And it has a... dual?:
(1) ∀α. C α → α
(2) ∃α. C α × α
I'm used to thinking of (2) as OO "objects". But is this related to terminal coalgebras somehow? If so, how? Or is it a different sort of dual entirely?

2026-01-18 15:36:47 UTC

It's well known that set intersection is associative. Unfortunately, it's also false:
import Data.Set
evens = fromList [0, 2 .. 20_000_000]
odds = fromList [1, 3 .. 20_000_000]
ends = fromList [0, 20_000_000]
fast = evens `intersection` (odds `intersection` ends)
slow = (evens `intersection` odds) `intersection` ends
λ> :set +s
λ> size fast
0
(0.00 secs, 70,592 bytes)
λ> size slow
0
(0.68 secs, 1,500,066,912 bytes)

2025-02-11 22:03:56 UTC

- reply

I didn't even realize pointed sets had coproducts until now! But now I see they're "smash" coproducts, ie the coproduct of the underlying sets quotiented by inl ⊥ = inr ⊥ = ⊥. interesting...

2025-02-11 21:50:46 UTC

- reply

sketch of why exponentials don't exist:
Find some f,g : Hom(A x B, C) such that f(⊥,x) ≠ g(⊥,x).
Curry f,g to get f*, g* : Hom(A, B ⇒ C).
But then f*(⊥) = g*(⊥) = ⊥ by preserving points.
So it sure seems like we must have f(⊥,x) = g(⊥,x).
I do not see a way to get around this. This is not proper proof, though.

2025-02-11 21:43:46 UTC

The category of pointed sets (sets w/ a designed "point", ⊥) and point-preserving maps (f(⊥) = ⊥) has:
cartesian products A × B: pairs with ⊥ = (⊥,⊥)
tensor/smash products A ⊗ B: quotient A × B by (⊥,y) = (x,⊥) = ⊥
internal homs A ⊸ B: point-preserving maps with ⊥ = λx.⊥, satisfying Hom(A ⊗ B, C) ≅ Hom(A, B ⊸ C)
but AFAIK no exponential A ⇒ B with Hom(A × B, C) ≅ Hom(A, B ⇒ C)
is there an extension of pointed sets that has exponentials w/o losing ⊸? (& thus models bunched implications?)

2024-10-26 16:08:19 UTC

autumn
https://recurse.social/system/media_attachments/files/113/374/576/557/595/823/original/f6ca7a200231ee3a.jpeg