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):
Last updated: Aug 03 2023 at 10:10 UTC