Ответ 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 - действительно смешное местное шотландское имя для Представителя, которые являются тем, для чего вы можете построить таблицу журналов: это конструкции, полностью очерченные проекцией, не предлагающие выбора "формы".