哪些Haskell函子等价于Reader函子？

Question

对于某些类型的F a，Haskell函子T -> 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“函子(这是Peter Hancock的术语:汉克和约翰·纳皮尔( John Napier )同属爱丁堡的居民，具有对数名望)，因为当F x ~= T -> x和记住，T -> x是"x to the power 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函子在最大不动点下是闭的，其对数是对应的最小不动点。例如，对于溪流，我们有

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

在Haskell中不引入Naperian双函子(对于两种事物有两组位置)，或者(更好的)索引类型上的Naperian函子(它为索引对象设置了索引位置)，这是有点费心的。不过，最简单的是，希望能给出一个想法，那就是共同自由的共餐。

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给出了它的单孔上下文类型，告诉我们1) p的形状，2)孔的位置，3)没有在洞中的数据。如果p是Naperian，就没有形状选择，所以把琐碎的数据放在非空穴的位置上，我们就可以得到洞的位置。

D p () ~= Log p

关于这个连接的更多信息，可以在this answer of mine有关尝试的文章中找到。

不管怎么说，Naperian确实是苏格兰的一个有趣的代表性的名字，它是你可以建立一个日志表的东西:它们是完全以投影为特征的结构，没有提供‘形状’的选择。