哪些 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

And Noah said unto the animals "Go forth and multiply!", but the snakes said "We cannot multiply, for we are adders.", so Noah took wood from the Ark and, shaping it, said "I am building you a table of logs.".

Representable 函子有时也被称为 "Naperian" 函子（这是 Peter Hancock 的术语：Hank 和 John Napier 是爱丁堡同一地区的居民，具有对数名声）因为当 F x ~= T -> x，并记住，T -> x 是“x 的 T 次方”，我们看到 T 在某种意义上是 Log F。

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

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

的确，我们有

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

使 p 成为右伴随，因此 p 保留所有极限，因此特别是单位和乘积，使其成为幺半群函子，而不仅仅是 lax 幺半群函子。也就是说，Applicative 的替代表示具有同构的操作。

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

让我们为事物指定一个类型 class。我做的和 Representable class.

有点不一样

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，在每个位置存储该位置的代表，就像一个 'map of an 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 函子在最大不动点下闭合，它们的对数是相应的最小不动点。例如，对于流，我们有

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（对于两种事物有两组位置）或（更好）的情况下，在 Haskell 中渲染它有点繁琐索引类型上的 Naperian 仿函数（具有索引事物的索引位置）。不过，cofree comonad 很简单，并且希望能给出这个想法。

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，就没有shape的选择，所以把琐碎的数据放在非孔的位置，我们发现我们只是得到了孔的位置。

D p () ~= Log p

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

无论如何，Naperian 确实是 Representable 的一个有趣的苏格兰当地名字，您可以为这些东西构建 table 原木：它们是完全以投影为特征的结构，不提供 'shape'.

的选择

哪些 Haskell 函子等同于 Reader 函子

Which Haskell Functors are equivalent to the Reader functor

haskell

functor

category-theory