关于类型构造器F a=(a→p)→q是否为Applicative函子的技术问询

非等价非平凡p、q时，F是否为Applicative函子？ #

结论：当p和q是不等价的非平凡固定类型时，无法为F构造满足Applicative定律的实例。

实例验证：F a = (a -> Bool) -> Int #

以p=Bool、q=Int为例，尝试推导Applicative核心方法的可行性：

• pure方法：Applicative要求pure :: a -> F a，代入定义后是pure :: a -> ((a -> Bool) -> Int)。构造这个函数确实需要依赖Bool -> Int类型的映射，但这只是基础要求。
• ap方法：ap :: F (a -> b) -> F a -> F b代入后为ap :: ((a->b)->Bool)->Int -> ((a->Bool)->Int) -> ((b->Bool)->Int)。要实现这个方法，需要将((a->b)->Bool)与(a->Bool)组合得到(b->Bool)再映射到Int，但Bool和Int的结构差异导致没有自然合法的组合方式，更无法满足Applicative的基本定律（比如pure id <*> x = x：pure id是((a->a)->Bool)->Int，无法通过组合操作保证其与任意x :: ((a->Bool)->Int)的<*>结果等于x）。

因此这个实例无法构造合法的Applicative实例。

F成为Applicative函子的最小必要条件 #

实现pure确实需要存在p -> q类型的值，但这只是必要不充分条件。真正的最小必要条件是p与q同构，推导如下：

• 若p和q同构（存在双向可逆映射f :: p -> q、g :: q -> p，满足f . g = id、g . f = id），则可以构造合法的Applicative实例：
  • pure x = \h -> f (h x)（利用p到q的映射）
  • ap fab fa = \hb -> f (g (fa (\a -> hb (fab' a))))（通过同构的双向映射完成函数组合，满足所有Applicative定律）
• 反之，若F是Applicative函子，可推导出p和q必须同构：
  观察F () = (() -> p) -> q，而() -> p同构于p，因此F ()同构于p -> q。结合Applicative的pure和ap操作，能构造出从q到p -> q的映射，再通过函子的协变性质，最终可推导出p与q之间存在双向可逆映射，即同构。

内容的提问来源于stack exchange，提问作者winitzki