Category Theory
Zulip Server
Archive

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.

Stream: learning: questions

Topic: f-algebras

marcosh (Apr 06 2020 at 14:29):

in Haskell you usually define newtype Fix f = Fix (f (Fix f)) and treat it as the initial f-algebra for f. Do you know how on does generally proves that Fix f is actually the initial f-algebra for f? Does it hold for any functor f?

Andre Knispel (Apr 06 2020 at 14:34):

Check out https://www.semanticscholar.org/paper/Inductive-and-Coinductive-Types-with-Iteration-and-Geuvers/c88146f46742bab40cea56b152a8467182733eec

Andre Knispel (Apr 06 2020 at 14:35):

Also note that because of undefined, Haskell has no limits

marcosh (Apr 06 2020 at 14:35):

thanks Andre

marcosh (Apr 06 2020 at 14:35):

let's leave undefined aside for the moment

marcosh (Apr 06 2020 at 14:36):

is some specific theorem of the paper relevant or the whole paper?

Andre Knispel (Apr 06 2020 at 14:38):

I think the Proof of Prop 3.4 is what you're looking for

marcosh (Apr 06 2020 at 14:38):

thanks!

Andre Knispel (Apr 06 2020 at 14:39):

Oh, wait, I just realized that this uses a different definition than what you gave

Jules Hedges (Apr 06 2020 at 14:40):

I have a faint memory of being told that in Haskell-like categories (with lazy datatypes) initial algebras and final coalgebras coincide

marcosh (Apr 06 2020 at 14:44):

@Andre Knispel looking here, 3.4 seems to be a Definition, are we looking at different versions of the paper?

Andre Knispel (Apr 06 2020 at 14:46):

Oh, sorry, that's not the same version of the paper that I have locally. It's Prop. 4.6 there

marcosh (Apr 06 2020 at 14:46):

ah, thanks

Andre Knispel (Apr 06 2020 at 14:48):

I think this can probably be converted in what you want, just need to check something

Andre Knispel (Apr 06 2020 at 14:49):

Jules Hedges said:

I have a faint memory of being told that in Haskell-like categories (with lazy datatypes) initial algebras and final coalgebras coincide

That sounds interesting!

Andre Knispel (Apr 06 2020 at 14:54):

Yeah, so if you Church-encode your definition of Fix, you end up with ∀ X. (f X -> X) -> X, which is exactly what you see there

Andre Knispel (Apr 06 2020 at 14:57):

I don't know how well Church encoding works for Haskell though

marcosh (Apr 06 2020 at 15:10):

that's exactly https://hackage.haskell.org/package/recursion-schemes-5.1.3/docs/Data-Functor-Foldable.html#t:Mu

marcosh (Apr 06 2020 at 15:11):

but the proposition you mention states the existence of a weakly intial algebra, so it does not guarantee uniqueness

Andre Knispel (Apr 06 2020 at 15:53):

I think generally the issue here is that it's not really possible to get uniqueness, at least not with the usual type theories. This is the whole issue with extensional equality not implying equality

Andre Knispel (Apr 06 2020 at 15:57):

You could of course quotient your category by extensional equality, which might what you want to do if you actually want to consider limits, but that seems like an ugly solution

Gershom (Apr 06 2020 at 20:53):

the initial question is answered by "lambek's lemma" which is described many places but here is one i found on a quick google http://www.cs.ru.nl/~jrot/coalgebra/ak-algebras.pdf

Gershom (Apr 06 2020 at 21:03):

the conditions for initial and final gadgets to coincide are given below remark 6.2.2 in fiore's thesis: https://www.lfcs.inf.ed.ac.uk/reports/94/ECS-LFCS-94-307/ (he doesn't use the words bilimit compact, but i've seen those around in more recent stuff)

Andre Knispel (Apr 06 2020 at 21:10):

How does lambek's lemma imply initiality?

Gershom (Apr 06 2020 at 21:33):

well my sense is consider the commutative square given here: https://ncatlab.org/nlab/show/initial+algebra+of+an+endofunctor#LambeksTheorem

now, since we have F(F(X)) isomorphic to F(X) then that says we must have a pair (a,X) such that F(X) = F(F(X)) = F(F(F(X)))... and clearly taking the fixed point of F itself satisfies this.

marcosh (Apr 06 2020 at 21:53):

Lambek lemma says that given an initial F-algebra (a, X), then a : F X -> X is an isomorphism. Since it is initial it is the least fiexed point. Existence of an F-algebra could be given by Adamek theorem (https://ncatlab.org/nlab/show/initial+algebra+of+an+endofunctor#AdameksTheorem). But why is it Fix F the least fixed point?

Gershom (Apr 06 2020 at 21:59):

By inspection, Fix f ~= Fix f (Fix f) ~= etc. So clearly it satisfies the requirement I gave above, which suffices to characterize it as an initial algebra.

Christian Williams (Apr 06 2020 at 22:06):

This was also being discussed at https://categorytheory.zulipchat.com/#narrow/stream/229156-practice.3A-applied.20ct/topic/Algebras/near/191558018.
I'm very interested in this "$\forall$/end" way of describing the initial algebra, but I haven't yet wrapped my head around it.

Christian Williams (Apr 06 2020 at 22:17):

I picture $\forall X. (FX\to X)\to X$ as a big product (subject to naturality). Now this is an algebra in some canonical way. What is this object? What does it mean to apply $F$ to it?

Maybe it would help everyone if we brought in a concrete example. Let's take $f:\mathrm{Set}\to \mathrm{Set}$ to be $F(X)=1+X^2$.

Andre Knispel (Apr 06 2020 at 22:28):

Gershom said:

By inspection, Fix f ~= Fix f (Fix f) ~= etc. So clearly it satisfies the requirement I gave above, which suffices to characterize it as an initial algebra.

There is still the issue of equality though. If you check https://ncatlab.org/nlab/show/initial+algebra+of+an+endofunctor#semantics_for_inductive_types then you'll see that this only works in extensional theories (and that weak initial algebras are the equivalent in intensional theories). I don't know about the internals of Haskell enough to be able to say definitively how that category behaves, but for Coq, Agda and Idris this is what you get.

Verity Scheel (Apr 06 2020 at 22:32):

Haskell is not a dependent type theory, it doesn’t have any internal notion of equality (extensional vs intensional), so we simply reason meta-theoretically using extensionality (and a lot of handwaving :wink:)

Andre Knispel (Apr 06 2020 at 22:46):

Christian Williams said:

I picture $\forall X. (FX\to X)\to X$ as a big product (subject to naturality). Now this is an algebra in some canonical way. What is this object? What does it mean to apply $F$ to it?

Maybe it would help everyone if we brought in a concrete example. Let's take $f:\mathrm{Set}\to \mathrm{Set}$ to be $F(X)=1+X^2$.

In general, this is the Church-encoding of that datatype. There are two ways I get my intuition for it: by considering special functors and by regarding elements as general ways to map out of that type.

$F$ is usually derived from constructors of a datatype, and if you have $n$ constructors, you can write $F$ as $F_1 + \cdots + F_n$. The constructor corresponding to $F_i$ is $F_i(T) \to T$ where $T$ is the type we're defining. So in your example, the constructors would be $c_1 : T$ and $c_2 : T^2 \to T$, which would be a type of binary trees.

If you look at the Church encoding, let's see what you can do with it. Let's fix a type $A$ and an element $t : T$ of the type we defined. Then $t A$ has type $(FA \to A) \to A$, i.e. mapping an $F$ algebra structure on $A$ to an element of $A$. So if you consider the map $\lambda t : T. t A alg : T \to A$ for some $alg$, you can define morphisms out of $T$. And this is basically the only way you can map out of $T$. This gives you a fold, and from that you can also derive recursion.

Andre Knispel (Apr 06 2020 at 22:47):

Nicholas Scheel said:

Haskell is not a dependent type theory, it doesn’t have any internal notion of equality (extensional vs intensional), so we simply reason meta-theoretically using extensionality (and a lot of handwaving :wink:)

Well, there still need to be some form of equality on the morphisms if you actually define the category though. Are functions equal if their code is equal or if the produce the same output given the same input? That gives you different categories.

John Baez (Apr 06 2020 at 22:51):

I don't know anything about this, but I'll still say something:

You'd darn well better have a category where morphisms are actual programs (or at least useful "isomorphism classes" of programs), and another category where programs that produce the same output given the same input count as the same morphism, and a functor from the first category to the second.

Andre Knispel (Apr 06 2020 at 22:55):

I'm pretty sure that's the case, there are even different levels to this depending on if you work within the language or look at it from the outside

Andre Knispel (Apr 06 2020 at 22:58):

There is also this nice paper https://arxiv.org/abs/1011.0014
It doesn't deal with types, but in the case of simple programs on natural numbers it gives you a whole galois correspondence

Verity Scheel (Apr 06 2020 at 23:01):

Sorry, I misunderstood what extensionality was referring to. Haskell would probably be considered an extensional type theory, because types cannot be equal in interesting ways and it has a form of equality reflection. But my other point still stands. If you were to define a category to reason about Haskell, it would most likely use function extensionality too, but there are greater obstructions there (“Hask is not a category”, non-strictness, etc.).

Andre Knispel (Apr 06 2020 at 23:07):

I mean it wasn't really clear the way I've phrased it, usually you think internally if you care about these things :slight_smile:

I really want to see what could be done with applying the paper I've mentioned to such a setting (I haven't checked if there were any follow ups on this though). Naively, it seems to have the potential to categorize the issues with how to define it properly (pun intended).

Andre Knispel (Apr 06 2020 at 23:11):

If that was possible, you'd have a tower of different categories with projections between them, with maybe the category formed by syntax at the top and the "classical mathematical picture" at the bottom and maybe some stuff in between. And if it fully works out, some automorphisms that correspond to that structure. That would be pretty cool.

Verity Scheel (Apr 06 2020 at 23:18):

My guess is that the bottom layer “programs” would be syntax quotiented by definitional equality, otherwise the composition in the category isn’t well-behaved. Well, you at the very least need to quotient out f . g = \x -> f (g x) and id x = x, so that identities and associativities hold. Actually, that’s not quite true, you also need eta-equivalence: f = \x -> f x.

Andre Knispel (Apr 06 2020 at 23:20):

I think you can just quotient by extensional equality (for Haskell)

Andre Knispel (Apr 06 2020 at 23:20):

You can probably do so as well in dependent type theories, but I'm not sure if you'd want to

Verity Scheel (Apr 06 2020 at 23:29):

Sorry, I guess I flipped top/bottom from what you mentioned. Would you quotient the syntax side of it or the semantics side of it by extensional equality?

Andre Knispel (Apr 06 2020 at 23:31):

I'd quotient the syntax. So you could first quotient out the equations you mentioned at the first step and then extensional equality at the second step

Andre Knispel (Apr 06 2020 at 23:34):

I've just played around with the intuition a little bit, and it seems plausible to get a Galois connection from this. So the category given by quotienting by the equations you gave would give you a subgroup of the automorphisms of the syntactic category, namely those that keep objects fixed (I think) and only perform rewrites with those equations on the morphisms

Verity Scheel (Apr 06 2020 at 23:36):

it would be interesting to think about optimizations in this framework

Andre Knispel (Apr 06 2020 at 23:38):

Indeed, you could get functorial compiler optimizations

Andre Knispel (Apr 06 2020 at 23:40):

Seems like the author of that paper hasn't followed up on it, so confirming if it actually works in a typed setting would need some actual work

Gershom (Apr 07 2020 at 00:44):

There is a standard notion of a tower of the sort described going between syntax and semantics. this is the tower (or really lattice) of abstract interpretation as given in e.g. https://www.di.ens.fr/~cousot/COUSOTpapers/ENTCS-97.shtml

Gershom (Apr 07 2020 at 00:46):

btw the nlab link above links eventually to wadler's classic note that describes the fixpoint construction in the initial question and gives a full proof, discussing both weak and strict settings https://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt

Gershom (Apr 07 2020 at 00:49):

and finally another notion of a "tower" is given in the lovely paper by John and Christian on enriched lawvere theories and operational semantics: https://arxiv.org/abs/1905.05636 @John Baez btw you may not have thought of your work in light of the cousot & cousot stuff on abstract interpretation. i wonder if it may be of interest to you.

John Baez (Apr 07 2020 at 01:48):

That paper has lots of scary symbols. :ogre:

John Baez (Apr 07 2020 at 01:50):

I have trouble with papers like this:

cousot.jpg

Nathanael Arkor (Apr 07 2020 at 01:51):

$\langle, \tau \rangle$ seems particularly mysterious

John Baez (Apr 07 2020 at 01:51):

Maybe you can tell me a bit about the basic idea, Gershom?

sarahzrf (Apr 07 2020 at 01:57):

Nathanael Arkor said:

$\langle, \tau \rangle$ seems particularly mysterious

-XTupleSections :thinking:

Gershom (Apr 07 2020 at 04:17):

Hrm ok. Let me give this "explaining" thing a shot.

So when one has a computer program, a typical thing to want to do is verify properties of it that hold under many different inputs, but do so without running under all such inputs. This is "static analysis". (I.e. you analyze it as a static object without dynamically executing it). One very powerful method of static analysis is something called "abstract interpretation" which you can think of as "running the program on generic inputs" or "running the program in an abstract domain" or the like. So imagine you want to prove that a result of a program that sends a number to another number never exceeds 100. You can give a suitably modified version of the program that does interval arithmetic a number that represents the range of the input, and then just examine the range of the output. Suppose you hit a choice point where the program branches if the number is greater than 50 or not. Your "abstracted" program can then take "both" paths, and attempt to "merge back" to the unioned state representing the range of possible values that can occur no matter which path was taken. So you need some way to "split" your bags of "general values" and "merge" them as well.

Along with extrema, one can verify things like e.g. memory safety, type soundness, various information security properties, etc. You just need to pick the right "abstract domain" to interpret into that tracks exactly the information you want, and turns the rest into "generalized data". And of course there are many tradeoffs between how precise you are, how hard it is to do, and how much information you can track. I should note this is a "real world" technique that has been used in practice to verify safety-critical software for areospace and the like.

What the Cousots worked on is a general formalism for this sort of thing, to let you believe that your original program and the abstracted interpretation of the program bear the sort of relationship you would like.

If you're in a theory without recursion, all this is very straightforward. It really is just sort of starting with an algebraic theory, and interpreting it with different models. But we want to work in real programs, with unbounded recursion. So they came up with a lattice theoretic formulation so that domain theory and fixpoint operators can be used, and a way of interpreting morphisms between different lattice-theoretic "abstract domains" so that you can show something is a "correct" abstract interpretation -- i.e. that it exists somewhere "between" the syntax and the intended concrete semantics, so that you can go all the way down, then partway back "up" or partway down, then the rest of the way down, and always end up in the same place. You also want to make sure that even if your original program is recursive and may never terminate, the "abstract domain" you interpret into should have some fixpoint semantics such that it _does_ terminate. (otherwise your "static" analysis may never complete).

That's where all the dense notation comes from.

you might be thinking "all this stuff about syntax and semantics and algebraic theories and their models sounds like there's some adjoints about." Indeed, there are ! One approach to how to get correct and terminating abstract interpretations is to construct the "abstract domain" as a lattice which relates to the "concrete domain" via a nice galois connection. This lets product types, function types, etc. be "pushed through" in a very general way. (Which makes sense, because to be a "sensible" interpretation, it is reasonable that you would want to preserve either meets or joins, depending on how you come at it).

The paper I linked above is a later paper that's dense, but I just really wanted to highlight the diagram on the last page that shows the big tower of related interpretations and semantics.

The earliest paper is probably the most directly readable, or rather difficulty in reading it arises not because it is complicated, but just because it is old: https://courses.cs.washington.edu/courses/cse501/15sp/papers/cousot.pdf

A later paper that explains the galois connection approach a bit is: https://www.di.ens.fr/~cousot/COUSOTpapers/publications.www/CousotCousot-PLILP-92-LNCS-n631-p269--295-1992.pdf

I confess I like the galois approach because it is simple and pretty, so don't really get what's happening with the "widening" stuff which the paper argues is more powerful. With the right categorical toolkit, I wonder if the latter approach can't be made prettier as well.

Sam Tenka (Apr 07 2020 at 05:14):

In abstract interpretation, "widening" refers to an intentional overapproximation step to make the fixpoint search terminate, e.g.:

If we want to analyze a program with an integer variable, we might abstract its state using a lattice of intervals like [1, 6]. But since this lattice isn't noetherian, an ascending search for a least fixpoint might not terminate: [1, 6], then [1, 7], then etc. Instead, at some point we might just "widen" to something that surely is an upper bound, in this case e.g. the top element. One way to think about this is to use the lattice of intervals except without any intervals of size too big --- so we immediately jump to top. But there are other cases one might want to widen, even if the lattice technically has Ascending Chain condition (e.g. the chains might be impractically long!)

marcosh (Apr 07 2020 at 07:18):

Gershom said:

By inspection, Fix f ~= Fix f (Fix f) ~= etc. So clearly it satisfies the requirement I gave above, which suffices to characterize it as an initial algebra.

@Gershom I'm sorry but I'm not sure I follow your reasoning. Which requirement are you referring to? Could you expand on it, please?

Gershom (Apr 07 2020 at 08:15):

By requirement I simply meant that F(X) =~ X. I agree the sketch I gave was handwavy. You need other ambient properties of the category you're working in -- things like fixed points actually existing, etc. And you need to be in a very special situation (which Haskell has) for the fixed point to imply initiality and not simply vice-versa. The wadler note I linked does it up right.

@Sam Tenka (naive student) thanks for that nice explanation of widening. I understand the paper I linked gives an example where widening cannot be captured by a galois connection. But surely there must be some more general way of thinking about adjoints where it makes sense?