哪些 Haskell 仿函数等价于 Reader 仿函数

Question

对于某些类型 T，某些 Haskell 函子 F a 显然与 T -> a 同构，例如

data Pair a = Pair a a            -- isomorphic to Bool -> a
data Reader r a = Reader (r -> a) -- isomorphic to r -> a (duh!)
data Identity a = Identity a      -- isomorphic to () -> a
data Phantom a = Phantom          -- isomorphic to void -> a

（这些同构仅取决于严格性，并且仅考虑有限的数据结构。）

那么一般来说，我们如何在可能的情况下表征函子？

问题是“哪些 Haskell 函子是可表示的？”同样的问题？

Answer 1

诺亚对动物说：“出去繁殖吧！”但蛇说 “我们不能繁殖，因为我们是加法器。”所以诺亚从方舟中取出木头， 塑造它，说“我正在为你建造一张原木表。”。

可表示的函子有时也被称为“Naperian”函子（这是彼得汉考克的术语：汉克是爱丁堡同一地区的居民，与约翰纳皮尔同属对数名声）因为当 F x ~= T -> x 时，记住这一点，组合起来，@987654323 @ 是“x 的幂 T”，我们看到 T 在某种意义上是 Log F。

首先要注意的是F () ~= T -> () ~= ()。这告诉我们只有一种形状。为我们提供形状选择的函子不能是 Naperian，因为它们没有给出数据位置的统一表示。这意味着 [] 不是 Naperian，因为不同长度的列表具有由不同类型表示的位置。但是，无限 Stream 的位置由自然数给出。

相应地，给定任意两个F 结构，它们的形状必然匹配，因此它们具有合理的zip，为我们提供Applicative F 实例的基础。

确实，我们有

          a  -> p x
=====================
  (Log p, a) ->   x

使p 成为右伴随，因此p 保留所有限制，因此特别是单元和乘积，使其成为单曲面函子，而不仅仅是松散 单曲面函子。也就是说，Applicative 的替代表示具有同构的操作。

unit  :: ()         ~= p ()
mult  :: (p x, p y) ~= p (x, y)

让我们为事物创建一个类型类。我的烹饪方式与Representable 课程略有不同。

class Applicative p => Naperian p where
  type Log p
  logTable  :: p (Log p)
  project   :: p x -> Log p -> x
  tabulate  :: (Log p -> x) -> p x
  tabulate f = fmap f logTable
  -- LAW1: project logTable = id
  -- LAW2: project px <$> logTable = px

我们有一个类型Log f，至少代表f中的一些位置；我们有一个logTable，在每个位置存储该位置的代表，就像一个“f 的地图”，每个位置都有地名；我们有一个project 函数提取存储在给定位置的数据。

第一定律告诉我们logTable 对于所代表的所有位置都是准确的。第二定律告诉我们，我们代表了所有个位置。我们可以推断出

tabulate (project px)
  = {definition}
fmap (project px) logTable
  = {LAW2}
px

还有那个

project (tabulate f)
  = {definition}
project (fmap f logTable)
  = {free theorem for project}
f . project logTable
  = {LAW1}
f . id
  = {composition absorbs identity}
f

我们可以想象一个Applicative 的通用实例

instance Naperian p => Applicative p where
  pure x    = fmap (pure x)                    logTable
  pf <$> px = fmap (project pf <*> project ps) logTable

这等于说p 从函数的常用 K 和 S 继承了自己的 K 和 S 组合子。

当然，我们有

instance Naperian ((->) r) where
  type Log ((->) r) = r  -- log_x (x^r) = r
  logTable = id
  project = ($)

现在，所有类似限制的构造都保留了 Naperianity。 Log 将有限的事物映射到有限的事物：它计算左邻域。

我们有终端对象和产品。

data K1       x = K1
instance Applicative K1 where
  pure x    = K1
  K1 <*> K1 = K1
instance Functor K1 where fmap = (<*>) . pure

instance Naperian K1 where
  type Log K1 = Void -- "log of 1 is 0"
  logTable = K1
  project K1 nonsense = absurd nonsense

data (p * q)  x = p x :*: q x
instance (Applicative p, Applicative q) => Applicative (p * q) where
  pure x = pure x :*: pure x
  (pf :*: qf) <*> (ps :*: qs) = (pf <*> ps) :*: (qf <*> qs)
instance (Functor p, Functor q) => Functor (p * q) where
  fmap f (px :*: qx) = fmap f px :*: fmap f qx

instance (Naperian p, Naperian q) => Naperian (p * q) where
  type Log (p * q) = Either (Log p) (Log q)  -- log (p * q) = log p + log q
  logTable = fmap Left logTable :*: fmap Right logTable
  project (px :*: qx) (Left i)  = project px i
  project (px :*: qx) (Right i) = project qx i

我们有身份和组成。

data I        x = I x
instance Applicative I where
  pure x = I x
  I f <*> I s = I (f s)
instance Functor I where fmap = (<*>) . pure

instance Naperian I where
  type Log I = ()    -- log_x x = 1
  logTable = I ()
  project (I x) () = x

data (p << q) x = C (p (q x))
instance (Applicative p, Applicative q) => Applicative (p << q) where
  pure x = C (pure (pure x))
  C pqf <*> C pqs = C (pure (<*>) <*> pqf <*> pqs)
instance (Functor p, Functor q) => Functor (p << q) where
  fmap f (C pqx) = C (fmap (fmap f) pqx)

instance (Naperian p, Naperian q) => Naperian (p << q) where
  type Log (p << q) = (Log p, Log q)  -- log (q ^ log p) = log p * log q
  logTable = C (fmap (\ i -> fmap (i ,) logTable) logTable)
  project (C pqx) (i, j) = project (project pqx i) j

Naperian 函子在 greatest 固定点下是封闭的，它们的对数是对应的 least 固定点。例如，对于流，我们有

log_x (Stream x)
  =
log_x (nu y. x * y)
  =
mu log_xy. log_x (x * y)
  =
mu log_xy. log_x x + log_x y
  =
mu log_xy. 1 + log_xy
  =
Nat

在没有引入 Naperian bifunctors（对于两种事物有两组位置）或（更好）索引类型上的 Naperian 仿函数（已经索引索引事物的位置）。不过，很容易并希望能给出这个想法的是 cofree 共轭。

data{-codata-} CoFree p x = x :- p (CoFree p x)
  -- i.e., (I * (p << CoFree p)) x
instance Applicative p => Applicative (CoFree p) where
  pure x = x :- pure (pure x)
  (f :- pcf) <*> (s :- pcs) = f s :- (pure (<*>) <*> pcf <*> pcs)
instance Functor p => Functor (CoFree p) where
  fmap f (x :- pcx) = f x :- fmap (fmap f) pcx

instance Naperian p => Naperian (CoFree p) where
  type Log (CoFree p) = [Log p]  -- meaning finite lists only
  logTable = [] :- fmap (\ i -> fmap (i :) logTable) logTable
  project (x :- pcx) []       = x
  project (x :- pcx) (i : is) = project (project pcx i) is

我们可能会采取Stream = CoFree I，给予

Log Stream = [Log I] = [()] ~= Nat

现在，仿函数的导数 D p 给出了它的单孔上下文类型，告诉我们 i）p 的形状，ii）孔的位置，iii）不在洞。如果p是Naperian，就没有形状的选择了，所以把琐碎的数据放到非孔位，我们发现我们只是得到了孔的位置。

D p () ~= Log p

有关该连接的更多信息，请参阅 this answer of mine 关于尝试。

无论如何，Naperian 确实是 Representable 的一个有趣的苏格兰本地名称，您可以为这些东西构建一个原木表：它们是完全以投影为特征的结构，不提供“形状”的选择。