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?
rntz
npub1a2…kdvl3
2026-06-24 18:35:05 UTC
Author Public Key
npub1a2q3hhrv09r6tjka84adev0mhse8mhf04unan0j8hn9gut5ksnpqpkdvl3Seen on
wss://relay.momostr.pinkPublished at
2026-06-24 18:35:05 UTCEvent JSON
{
"id": "d0141559b4089c288c311e9244ee0691de8febcdd533ceb81897e92171f70a51",
"pubkey": "ea811bdc6c7947a5cadd3d7adcb1fbbc327ddd2faf27d9be47bcca8e2e9684c2",
"created_at": 1782326105,
"kind": 1,
"tags": [
[
"proxy",
"https://recurse.social/@rntz/116806523667370297",
"web"
],
[
"proxy",
"https://recurse.social/users/rntz/statuses/116806523667370297",
"activitypub"
],
[
"L",
"pink.momostr"
],
[
"l",
"pink.momostr.activitypub:https://recurse.social/users/rntz/statuses/116806523667370297",
"pink.momostr"
],
[
"-"
]
],
"content": "class Expr a\n add: a × a → a\n lit: Int → a\n\nThe type of expressions in this language is definable by Church-encoding:\n\n∀α. Expr α → α\n\nSince 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?:\n\n(1) ∀α. C α → α\n(2) ∃α. C α × α\n\nI'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?",
"sig": "7053896ec7bdef6f13745007660e01e6493ba3b04206bc50702e2b5b120e7ee2aeeb568a020b0bb0929f2f8db348c5bfdd650c26e51c91dffdf787aa871affab"
}