Когда экземпляр Ap's Num является законным?

Question

Рассмотрим этот тип:

      newtype Ap f a = Ap (f a)
instance (Applicative f, Num a) => Num (Ap f a) where
  (+)         = liftA2 (+)
  (*)         = liftA2 (*)
  negate      = fmap negate
  fromInteger = pure . fromInteger
  abs         = fmap abs
  signum      = fmap signum

Что должно быть правдой, чтобы этот случай был законным? Ясно, что просто быть законным недостаточно (например, x + negate xотличается от fromInteger 0когда xявляется Ap Nothing, Несмотря на то Maybeявляется законным Applicative). Я предполагаю, что это необходимо и достаточно для fбыть представимым функтором. Однако я не уверен, как это доказать (или найти контрпример, если он неверен).

Для справки, вот законы, предложенные Numдокументация :

      -- Associativity of (+)
(x + y) + z = x + (y + z)

-- Commutativity of (+)
x + y = y + x

-- fromInteger 0 is the additive identity
x + fromInteger 0 = x

-- negate gives the additive inverse
x + negate x = fromInteger 0

-- Associativity of (*)
(x * y) * z = x * (y * z)

-- fromInteger 1 is the multiplicative identity
x * fromInteger 1 = x
fromInteger 1 * x = x

-- Distributivity of (*) with respect to (+)
a * (b + c) = (a * b) + (a * c)
(b + c) * a = (b * a) + (c * a)

Answer 1

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

Алгебра тривиальноring(забыв о скалярах), и это единственное, с чем все могут согласиться относительно того, что на самом деле описывает класс. В этом смысле да, Representableэто то, что нужно. В частности, вы используете замену абстрактных векторов их базисным расширением, т.е. вы по существу сводите все к

      instance Num a => Num (r -> a) where
  fromInteger = const . fromInteger
  f + g = \e -> f e + g e
  f * g = \e -> f e * g e
  negate f = negate . f
  abs f = abs . f
  signum f = signum . f

который затем можно использовать с r ~ Rep f, потому что тип Rep f -> aизоморфен f a.

Лично я не сторонник всего этого. В частности, случаи V2и т. д. являются головной болью, потому что, например, 1 :: V2 Double ≡ V2 1 1не имеет никакого смысла геометрически, если вы имеете дело, например, с диаграммами, которые, как предполагается, не зависят от вращения. Видите ли, любое конечномерное векторное пространство может быть реализовано с помощью представимых функторов, но это влечет за собой выбор произвольного базиса. Но это все равно, что выбрать произвольную кодировку символов для текстового редактора, а затем жестко запечь ее таким образом, чтобы она полностью отображалась в общедоступном интерфейсе. Это плохой дизайн. Просто потому, что вы можете , не означает, что вы должны.

Кроме того, многие практически полезные векторные пространства не могут быть разумно реализованы с помощью представимых функторов, или такая реализация может быть очень непрактичной. Я говорю здесь о разреженных векторах, или об эффективном неупакованном и/или распределенном хранилище, или (лично любимом) о бесконечномерных функциональных пространствах.

Поэтому я рекомендую сохранить Numclass к вещам, которые однозначно являются числами , и вызывайте все остальное явно тем, что вы действительно хотите. Мои пакеты free-vector-spaces и linearmap-category пытаются сделать это принципиальным и мощным способом, опираясь на простые и безопасные классы из vector-space .

Answer 2

Что должно быть правдой, чтобы этот случай был законным?

Чтобы набросать аргумент, мы можем начать с сосредоточения внимания на моноиде эффектов (если хотите), который находится под аппликативом. Для сохранения дистрибутивности слева нам нужно, чтобы моноид эффектов был самораспределяемым слева (то есть, u <> (v <> w) = (u <> v) <> (u <> w)), и аналогично для правой дистрибутивности. Кроме того, если моноид является самораспределяемым как слева, так и справа, он должен быть и коммутативным, и идемпотентным . Это уже серьезное ограничение, хотя его недостаточно, чтобы исключить Maybe(который является идемпотентным, коммутативным аппликативом). Раз так, то имеет смысл воспользоваться вашей подсказкой и посмотреть на аддитивный обратный закон:

      x + negate x = fromInteger 0
-- Substitute the instance implementations:
liftA2 (+) x (negate <$> x) = pure (fromInteger 0)
-- (&*&) = liftA2 (,)
(\(a, b) -> a + negate b) <$> (x &*& x) = pure (fromInteger 0)

В частности, используя (() <$)с обеих сторон дает нам:

      () <$ (x &*& x) = pure ()

Возвращаясь к точке зрения моноида эффектов, это равносильно u <> u = mempty. Поскольку ранее мы установили, что моноид эффектов должен быть идемпотентным, u <> u = u. Следовательно, u = mempty; то есть возможен только один .

Что касается остальных законов, то тождество и ассоциативность должны следовать из аппликативных законов, а коммутативность (+)предположительно требует быть коммутативным аппликативом...

      liftA2 g u v = liftA2 (flip g) v u

... что немного сильнее, чем просто требование коммутативности Ap f ()о котором я упоминал ранее (см.Selectдля иллюстрации этого).

Для Num (Ap f a)экземпляра, чтобы быть законным, поэтому, кажется, нам нужно, по крайней мере, чтобы fявляется коммутативным аппликативом, и что существует только один f ()ценность. Хотя аргумент еще не совсем убедителен, эти требования действительно сильно напоминают представимые функторы.