You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Jonathan Castello (Dec 08 2020 at 07:07):I use F-algebras pretty often in software development, since they're closely related to the Visitor pattern in object-oriented programming. (A visitor is basically a choice of algebra.) But I've run into something that's not quite the same thing. I've distilled it into something that looks roughly F-algebraic, but isn't. I'm not sure what to call it, and I'm having trouble finding related concepts in the literature. (My CT comprehension is pretty low, so it's also hard to tell whether something promising is actually relevant at all.)
To my understanding, an F-algebra over an (endo)functor F is a morphism F t -> t with a carrier t. (Programmatically, I'd write Algebra t = F t -> t.) It works great for describing interpreters for single-sorted expressions like (1 + (2 * 3)), where the type of every subexpression is the same. But I have a situation where the type of a subexpression can vary, where a structure IndexedAlgebra f t = F f t -> f t arises. (The name comes from my half-baked understanding of things like indexed monads.)
An example F here might be F f t = t + (exists s. (s -> t) * f s * f s), describing the type of binary trees where combining two subexpressions may also change its type. The lowercase f allows the interpreted type to vary depending on the algebra; for instance, I might use the identity functor when evaluating the expression straight, or the constant functor on String to produce a human-readable representation at any subtree.
Is this a well-founded concept? Are there any immediate references to the literature that investigates constructions like this? (Is the name "indexed algebra" way off base?)
Björn Gohla (Dec 08 2020 at 13:38):My gut reaction would be you need your signature functor F to act on an arrow category.
Dan Doel (Dec 08 2020 at 15:25):I think there's quite a bit of literature about this sort of thing in relation to indexed inductive types that you find in dependent type theories. Stuff like this for instance. The semantics of indexed inductive definitions are initial algebras of that sort.
And yeah, the arrow category/codomain fibration is one way to model those sort of types.
Dan Doel (Dec 08 2020 at 15:25):In the case of the type theory stuff, the index wouldn't need to be a type, of course. You can index by elements of any type, not just a universe.
Jonathan Castello (Dec 08 2020 at 21:35):Great, thanks for the leads! :big_smile: