Zulip Chat Archive

Stream: general

Topic: Does an applicative depend on pure?

Mario Carneiro (Aug 10 2018 at 07:41):

A surprisingly hard problem: Prove or construct a counterexample to the following claim: If two (lawful) applicative structures on F have the same seq function, then they are equal.

Mario Carneiro (Aug 10 2018 at 07:46):

Originally I thought it might be true, by analogue to the uniqueness of the identity of a monoid, but now I'm not so sure. Nevertheless there are no obvious ways to cook up an applicative with two different pures. Here is the equational theory of applicatives (with map eliminated):
p1(f)p1(x)=p1(fx)p_1(f)\cdot p_1(x)=p_1(f \,x)
fp1(x)=p1(λg.gx)ff\cdot p_1(x)=p_1(\lambda g.\, g\,x)\cdot f
p1()hgx=h(gx)p_1(\circ)\cdot h\cdot g\cdot x=h\cdot (g\cdot x)
p1(id)x=xp_1(id)\cdot x=x

Last updated: Dec 20 2023 at 11:08 UTC