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

Question

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

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.".

可表示的仿函数有时也被称为“Naperian”仿函数(这是彼得汉考克的术语:汉克是爱丁堡同一地区的居民，与约翰纳皮尔的对数成名)因为当 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保留所有限制，因此特别是单元和产品，使其成为一个单曲面仿函数，而不仅仅是一个松散的单曲面仿函数。也就是说， Applicative 的替代表示具有同构的操作。

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

让我们为这些东西创建一个类型类。我做的和 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 ，在每个位置存储该位置的代表，就像一个“ f 的 map ” ' 每个地方都有地名；我们有一个 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 for 函数继承其自己的 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 双仿函数(对于两种事物有两组位置)或(更好)索引类型上的 Naperian 仿函数(具有索引事物的索引位置)的情况下，在 Haskell 中呈现它有点繁琐。不过，很容易并希望能给出这个想法的是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，没有形状的选择，所以把琐碎的数据放在非孔的位置，我们发现我们只是得到了孔的位置。

D p () ~= Log p

更多关于该连接的信息可以在 this answer of mine 中找到。关于尝试。

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