Моноидальный функтор является аппликативным, но где Моноидный тип в определении Аппликатива?

Аппликатив-это Моноидальный функтор: 

mappend :: f         -> f   -> f
$       ::  (a -> b) ->   a ->   b
<*>     :: f(a -> b) -> f a -> f b
Но я не вижу никакой ссылки на моноид в определении прикладного класса типов, не могли бы вы сказать мне, почему ?

Определение: 

class Functor f => Applicative (f :: * -> *) where
  pure :: a -> f a
  (<*>) :: f (a -> b) -> f a -> f b
  GHC.Base.liftA2 :: (a -> b -> c) -> f a -> f b -> f c
  (*>) :: f a -> f b -> f b
  (<*) :: f a -> f b -> f a
  {-# MINIMAL pure, ((<*>) | liftA2) #-}

В этом определении нет упоминания об этом структурном Моноиде, но когда вы это делаете 

> ("ab",(+1)) <*> ("cd", 5) 
>("abcd", 6)

Вы можете ясно видеть использование структурного моноида "(,) String " при реализации этого экземпляра Applicative.

Еще один пример, чтобы показать, что " структурная Моноид " используется: 

Prelude Data.Monoid> (2::Integer,(+1)) <*> (1::Integer,5)

<interactive>:35:1: error:
    • Could not deduce (Monoid Integer) arising from a use of ‘<*>’
      from the context: Num b
        bound by the inferred type of it :: Num b => (Integer, b)
        at <interactive>:35:1-36
    • In the expression: (2 :: Integer, (+ 1)) <*> (1 :: Integer, 5)
      In an equation for ‘it’:
          it = (2 :: Integer, (+ 1)) <*> (1 :: Integer, 5)
3 8
haskell applicative

3 ответа:

Моноид, который называется "моноидальным функтором", не является моноидом Monoid, то есть моноидом уровня значения. Вместо этого это моноид типа . А именно, сверлильный продукт моноид 

type Mempty = ()
type a <> b = (a,b)
(Вы можете заметить, что это, строго говоря, не моноид; это только если вы рассматриваете ((a,b),c) и (a,(b,c)) как один и тот же тип. Они достаточно изоморфны.) Чтобы понять, какое это имеет отношение к Applicative, ОТВ. моноидальные функторы, нам нужно написать класс в другом условия. 
class Functor f => Monoidal f where
  pureUnit :: f Mempty
  fzip :: f a -> f b -> f (a<>b)

-- an even more “general nonsense”, equivalent formulation is
-- upure :: Mempty -> f Mempty
-- fzipt :: (f a<>f b) -> f (a<>b)
-- i.e. the functor maps a monoid to a monoid (in this case the same monoid).
-- That's really the mathematical idea behind this all.

IOW 

class Functor f => Monoidal f where
  pureUnit :: f ()
  fzip :: f a -> f b -> f (a,b)

Это простое упражнение для определения универсального экземпляра стандартного класса Applicative в терминах Monoidal, и наоборот.

Относительно ("ab",(+1)) <*> ("cd", 5): это не имеет большого отношения к Applicative в целом, но только к писателю конкретно. Пример - 

instance Monoid a => Monoidal ((,) a) where
  pureUnit = (mempty, ())
  fzip (p,a) (q,b) = (p<>q, (a,b))
11

Возможно, моноид, который вы ищете, и есть этот.

newtype AppM f m = AppM (f m) deriving Show

instance (Applicative f, Monoid m) => Monoid (AppM f m) where
  mempty                      = AppM (pure mempty)
  mappend (AppM fx) (AppM fy) = AppM (pure mappend <*> fx <*> fy)

Как следует из комментария ниже, его можно найти в библиотеке редукторов под названием Ap. Это фундаментально для Applicative, так что давайте распакуем его.

Обратите внимание, в частности, что поскольку () тривиально a Monoid, AppM f () это тоже Monoid. И это моноид, скрывающийся позади Applicative f.

Мы могли бы настоять на Monoid (f ()) как на суперклассе Applicative, но это все испортило бы. сильно. 
> mappend (AppM [(),()]) (AppM [(),(),()])
AppM [(),(),(),(),(),()]

Моноид, лежащий в основе Applicative [], являетсяумножением натуральных чисел, тогда как "очевидная" моноидальная структура для списков-это конкатенация, которая специализируется насложении натуральных чисел.

Математическое предупреждение. Предупреждение зависимых типов. Фальшивое предупреждение Хаскелла.

Один из способов увидеть, что происходит, - рассмотреть те Аппликативы, которые оказываются контейнерами в зависимо типизированном смысле Эббота, Альтенкирх и Гани. Скоро они будут у нас в Хаскелле. Я просто притворюсь, что будущее уже наступило. 
data (<|) (s :: *)(p :: s -> *) (x :: *) where
  (:<|:) :: pi (a :: s) -> (p a -> x) -> (s <| p) x

Структура данных (s <| p) характеризуется

  • фигуры s что говорит вам, как выглядит контейнер.
  • позиции p которые говорят вам для заданной формы, куда вы можете поместить данные.

Приведенный выше тип говорит, что дать данные для такой структуры - это выбрать форму, а затем заполнить все позиции с данными.

Представление контейнера [] является Nat <| Fin, где 

data Nat = Z | S Nat
data Fin (n :: Nat) where
  FZ :: Fin (S n)
  FS :: Fin n -> Fin (S n)

Так что Fin n имеет ровно n значения. То есть форма списка-это его длина , и это говорит вам, сколько элементов вам нужно заполнить список.

Вы можете найти формы для Хаскелла Functor f, взяв f (). Делая данные тривиальными, позиции не имеют значения. Построение GADT позиций в общем виде в Хаскелле гораздо сложнее.

Параметричность говорит нам, что полиморфная функция между контейнерами в 
forall x. (s <| p) x -> (s' <| p') x

Должно быть дано через

  • функция f :: s -> s' отображение входных фигур в выходные фигуры
  • функция g :: pi (a :: s) -> p' (f a) -> p a отображение (для заданной входной формы) выходных позиций обратно к входным позициям, из которых будет исходить выходной элемент.

morph f g (a :<|: d) = f a :<|: (d . g a)
(Втайне те из нас, кто прошел базовую хэнкоковскую подготовку, также думают о" формах "как о" командах " и о том, что они не могут быть даны. "позиции "как"действительные ответы". Морфизм между контейнерами тогда точно является "драйвером устройства". Но я отвлекся.) Размышляя в том же духе, что нужно сделать, чтобы создать контейнер Applicative? Для начала, 
pure :: x -> (s <| p) x

Что эквивалентно 

pure :: (() <| Const ()) x -> (s <| p) x

Это должно быть дано 

f :: () -> s   -- a constant in s
g :: pi (a :: ()) -> p (f ()) -> Const () a  -- trivial

Где f = const neutral для некоторых 

neutral :: s

А теперь, как насчет 

(<*>) :: (s <| p) (x -> y) -> (s <| p) x -> (s <| p) y

? Опять же, параметричность говорит нам о двух вещах. Во-первых, единственные полезные данные для расчета выходные фигуры - это две входные фигуры. Мы должны иметь функцию 

outShape :: s -> s -> s
Во-вторых, единственный способ, которым мы можем заполнить выходную позицию с помощью y, - это выбрать позицию из первого входа, чтобы найти функцию в `x - > y', а затем позицию во втором входе, чтобы получить ее аргумент. 
inPos :: pi (a :: s)(b :: s) -> p (outShape a b) -> (p a, p b)
То есть мы всегда можем определить пару входных позиций, которые определяют выход в выходной позиции. Прикладные законы говорят нам, что neutral и outShape должны подчиняться моноидные законы, и что, кроме того, мы можем поднимать моноиды следующим образом 
mappend (a :<|: f) (b :<|: g) = outShape a b :<|: \ z ->
  let (x, y) = inPos a b z
  in  mappend (f x) (g y)
Здесь есть еще что сказать, но для этого мне нужно противопоставить две операции с контейнерами.

Композиция 

(s <| p) . (s' <| p')  =  ((s <| p) s') <| \ (a :<|: f) -> Sigma (p a) (p' . f)

Где Sigma - тип зависимых пар 

data Sigma (p :: *)(q :: p -> *) where
  Pair :: pi (a :: p) -> q a -> Sigma p q
Что, черт возьми, это значит?
  • вы выбираете внешнюю форму
  • вы выбираете внутреннюю форму для каждой внешней позиции
  • составная позиция - это тогда пара внешнего положения и внутреннего положения, соответствующего внутренней форме, которая сидит там

Или, по Хэнкоку

  • вы выбираете внешнюю команду
  • вы можете подождать, чтобы увидеть внешний ответ, прежде чем выбрать внутреннюю команду
    • Составной ответ - это ответ на внешнюю команду, за которым следует ответ на внутреннюю команду, выбранную вашей стратегией

Или, более откровенно

  • когда вы составляете список списков, то внутренние списки могут иметь разную длину

join из Monad выравнивает композицию. За ним скрывается не просто моноид на фигурах, а оператор интегрирования . То есть, 

join :: ((s <| p) . (s <| p)) x -> (s <| p) x

Требует 

integrate :: (s <| p) s -> s
Ваша свободная монада дает вам деревья стратегий, где вы можете использовать результат одной команды, чтобы выбрать остальную часть вашей стратегии. Как будто вы взаимодействуете в 1970-е годы телетайп.

Тем временем...

Тензор

Тензор (также благодаря Хэнкоку) двух контейнеров задается 

(s <| p) >< (s' <| p')  =  (s, s') <| \ (a, b) -> (p a, p' b)

То есть

  • вы выбираете две фигуры
  • позиция - это пара позиций, по одной для каждой фигуры

Или

  • вы выбираете две команды, не видя никаких ответов
  • ответ - это тогда пара ответов

Или

  • [] >< [] - это тип из прямоугольных матриц : все "внутренние" списки должны иметь одинаковую длину
Последнее является ключом к тому, почему >< очень трудно получить в руки в Haskell, но легко в зависимости от набора настроек. Как и композиция, тензор является моноидом с тождественным функтором в качестве его нейтрального элемента. Если мы заменим композицию, лежащую в основе Monad, тензором, что мы получим? 
pure :: Id x -> (s <| p) x
mystery :: ((s <| p) >< (s <| p)) x -> (s <| p) x

, но все, что может mystery быть? Это не тайна, потому что мы знаем, что есть достаточно жесткий способ сделать полиморфные функции между контейнерами. Должно быть 

f :: (s, s) -> s
g :: pi ((a, b) :: (s, s)) -> p (f (a, b)) -> (p a, p b)

И это именно то, что мы сказали, определяются <*> ранее.

Applicative является понятие эффективного программирования, порожденного тензором, где Monad порождается композицией. Тот факт, что вам не нужно ждать внешнего ответа, чтобы выбрать внутреннюю команду, является причиной того, что программы Applicative легче распараллеливаются.

Видя [] >< [] как прямоугольные матрицы говорит нам почему <*> для списков строится поверх умножения.

Свободный аппликативный функтор - это свободный моноид с включенными ручками. Для контейнеров, 
Free (s <| p) = [s] <| All p

Где 

All p [] = ()
All p (x : xs) = (p x, All p xs)
Таким образом," команда " - это большой список команд, как колода перфокарт. Вы не увидите никаких выходных данных, прежде чем выберете свою колоду карт. "Ответ" - это результат работы линейного принтера. Это 1960-е годы. [63] Итак, вы идете. Сама природа Applicative, тензор не композиция, требует лежащего в основе моноид и рекомбинация элементов, совместимых с моноидами.
10

Я хотел дополнить поучительный ответ Конора Макбрайда (pigworker) еще несколькими примерами Monoid, найденными в Applicatives. было замечено , что экземпляр Applicative некоторых функторов напоминает соответствующий экземпляр Monoid.; например, мы имеем следующие аналогии: 

Applicative → Monoid
---------------------
List        → Product
Maybe       → All
Either a    → First a
State s     → Endo s

Следующий комментарий Конора, мы можем понять поэтому у нас есть эти соответствия. Мы используем следующие наблюдения:

  1. форма Applicative контейнер образует Monoid в соответствии с операцией приложения <*>.
  2. форма функтора F задается через F 1 (где 1 обозначает единицу ()).

Для каждого из перечисленных выше функторов Applicative мы вычисляем их форму, создавая экземпляр функтора с единичным элементом. Мы это понимаем...

List имеет вид Nat: 

List a = μ r . 1 + a × r
List 1 = μ r . 1 + 1 × r
       ≅ μ r . 1 + r
       ≅ Nat

Maybe имеет вид Bool: 

Maybe a = 1 + a
Maybe 1 = 1 + 1
        ≅ Bool

Either имеет вид Maybe: 

Either a b = a + b
Either a 1 = a + 1
           ≅ Maybe a

State имеет форма Endo: 

State s a = (a × s) ^ s
State s 1 = (1 × s) ^ s
          ≅ s ^ s
          ≅ Endo s

Типы фигур точно соответствуют типам, лежащим в основе Monoid, перечисленных в начале. Одна вещь все еще озадачивает меня: некоторые из этих типов допускают множественные Monoid экземпляры (, например, Bool может быть превращен в Monoid как All или Any), и я не совсем уверен, почему мы получаем один из экземпляров, а не другой. Я предполагаю, что это связано с прикладными законами и тем, как они взаимодействуют с другим компонентом контейнер – его позиции.

1