Какие Haskell-функторы эквивалентны функтору Reader

Некоторые функторы 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 являются представимыми?" тот же вопрос?

Ответ 1

И сказал Ной животным: "Иди и размножись!", но змеи сказали: "Мы не можем размножаться, потому что мы - сумматоры", поэтому Ной взял дерево из Ковчега и, формируя его, сказал: "Я строю вам таблицу журналов".

Представляемые функторы иногда также называются "неберианскими" функторами (это термин Петер Хэнкок: Хэнк - обитатель той же части Эдинбурга, как Джон Напир, с логарифмической известностью), потому что, когда 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 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, представляющий по крайней мере некоторые из положений внутри a F; мы имеем a 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

Нейперианские функторы замкнуты относительно больших фиксированных точек, причем их логарифмы являются соответствующими наименьшими фиксированными точками. Например, для потоков мы имеем

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 на индексированных типах (которые индексировали позиции для индексированных вещей). Что легко, и, надеюсь, дает идею, это 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) вид a p, ii) положение дырки, iii) данные, которые не находятся в дыра. Если p является Naperian, выбор формы невозможен, поэтому вводя тривиальные данные в позиции без отверстия, мы обнаруживаем, что мы просто получаем положение отверстия.

D p () ~= Log p

Подробнее об этом соединении можно найти в этом ответе о попытках.

Во всяком случае, Naperian - действительно смешное местное шотландское имя для Представителя, которые являются тем, для чего вы можете построить таблицу журналов: это конструкции, полностью очерченные проекцией, не предлагающие выбора "формы".