Подтвердить что ты не робот

Есть ли функтор, который не может быть законопослушным?

A недавний вопрос в основном задавал границы между различными классами Haskell. Я придумал Handler как пример действительного Functor без разумного экземпляра Apply **, где

class Functor f => Apply f where
  (<.>) :: f (a -> b) -> f a -> f b
  -- optional bits omitted.

Однако мне еще не удалось найти пример допустимого Functor, который нельзя сделать допустимым (если бессмысленным) экземпляром Apply. Тот факт, что Apply имеет (см. Обновление), но один закон,

(.) <$> u <.> v <.> w = u <.> (v <.> w)

похоже, делает это довольно сложным.

pigworker (Conor McBride) ранее привел пример Functor, который не является Applicative, но он полагался на pure, чтобы сделать это, и который недоступен в Apply.

** Затем я понял, что на самом деле может быть разумный (хотя и немного странный) экземпляр Apply для Handler, который концептуально собирает одновременные исключения.

Update

Эдвард Кметт теперь принял два дополнительных закона, предложенных мной для Apply (для проверки оптимизаций, которые я сделал для экземпляра Apply (Coyoneda f)),

x <.> (f <$> y) = (. f) <$> x <.> y
f <$> (x <.> y) = (f .) <$> x <.> y

Было бы интересно посмотреть, изменят ли эти дополнения ответ на этот вопрос.

4b9b3361

ОТВЕТЫ

Ответ 1

Да, есть Functor без экземпляра Apply. Рассмотрим сумму двух функций (которые являются показателями в алгебраических типах данных):

data EitherExp i j a
    = ToTheI (i -> a)
    | ToTheJ (j -> a)

Существует экземпляр Functor для всех i и j:

instance Functor (EitherExp i j) where
    fmap f (ToTheI g) = ToTheI (f . g)
    fmap f (ToTheJ g) = ToTheJ (f . g)

но нет экземпляра Apply для всех i и j сек

instance Apply (EitherExp i j) where
    ...
    ToTheI f <.> ToTheJ x = ____

Невозможно заполнить пробел ____ i -> b или j -> b, когда у вас есть только f :: i -> a -> b и x :: j -> a. Для этого нам нужно что-то знать о i и j, но нет способа заглянуть внутрь каждого типа i или j в Haskell. Интуиция отвергает этот ответ; если вам что-нибудь известно о i или j, например, что они населены одним значением, то вы можете написать экземпляр Apply для EitherExp

class Inhabited a where
    something :: a

instance (Inhabited i, Inhabited j) => Apply (EitherExp i j) where
    ...
    ToTheI f <.> ToTheJ x = ToTheI (const ((f something) (x something)))

Но мы не знаем, что каждый i и каждый j - это Inhabited. Тип Void ничем не населён. У нас даже нет способа узнать, что каждый тип является либо Inhabited, либо Void.

Наша интуиция на самом деле очень хорошая; когда мы можем проверить, как создаются типы, для алгебраических типов данных нет Functor, у которого нет экземпляров Apply. Ниже приведены два ответа, которые могут быть более приятными для нашей интуиции.

Нет...

... для алгебраических типов данных. Есть 3 варианта. Структура void, структура может быть пустой или структура не может быть пустой. Если структура недействительна, то она absurd является Apply. Если он может быть пустым, выберите любой пустой экземпляр и возвращайте его постоянно для любого применения. Если он не может быть пустым, то если это сумма структур, каждая из которых не может быть пустой, то можно применить законопослушное применение, применив одно из значений † от первого к одному из значений второго и возвращая его в некоторой постоянной структуре.

Применяемый закон очень слабый. Применить не нужно, чтобы иметь какой-либо смысл. Это не должно быть "zip-y". Это не обязательно должен быть fmap в сочетании с подозрительными вещами, такими как pure из Applicative; в pure нет понятия, с помощью которого можно написать закон, требующий, чтобы он имел смысл.

Когда структура может быть пустой

Выберите любой пустой экземпляр и возвращайте его постоянно для любого применения

u <.> v = empty

Proof

  (.) <$> u  <.> v  <.> w = u <.> (v <.> w)
(((.) <$> u) <.> v) <.> w = u <.> (v <.> w) -- by infixl4 <$>, infixl4 <.>
(_                ) <.> w = u <.> (_      ) -- by substitution
                    empty = empty           -- by definition of <.>

Когда структура не может быть пустой

Если структура f не может быть пустой, существует функция extract :: forall a. f a -> a. Выберите другую функцию c :: forall a. a -> f a, которая всегда создает одну и ту же непустую структуру, всюду заполненную аргументом, и определите:

u <.> v = c (extract u $ extract v)

со свободными теоремами

extract (f <$> u) = f (extract u)
extract . c = id

Proof

  (.) <$> u  <.> v  <.> w = u <.> (v <.> w)
(((.) <$> u) <.> v) <.> w = u <.> (v <.> w) -- by infixl4 <$>, infixl4 <.>
(c (extract ((.) <$> u) $ extract v)) <.> w = u <.> (v <.> w) -- by definition
(c ((.) (extract u)     $ extract v)) <.> w = u <.> (v <.> w) -- by free theorem 
c (extract (c ((.) (extract u) $ extract v)) $ extract w) = u <.> (v <.> w) -- by definition
c (           ((.) (extract u) $ extract v)  $ extract w) = u <.> (v <.> w) -- by extract . c = id
c (((.) (extract u) $ extract v) $ extract w) = u <.> c (extract v $ extract w) -- by definition
c (((.) (extract u) $ extract v) $ extract w) = c (extract u $ extract (c (extract v $ extract w))) -- by definition
c (((.) (extract u) $ extract v) $ extract w) = c (extract u $            (extract v $ extract w) ) -- by extract . c = id
let u' = extract u
    v' = extract v
    w' = extract w
c (((.) u' $ v') $ w') = c (u' $ (v' $ w'))
c ((u' . v') $ w') = c (u' $ (v' $ w')) -- by definition of partial application of operators
c (u' $ (v' $ w')) = c (u' $ (v' $ w')) -- by definition of (.)

Еще немного стоит сказать об определении extract для экспоненциальных типов, функций. Для функции i -> a есть две возможности. Либо i обитаем, либо нет. Если оно обитаемо, выберите какого-нибудь жителя i † и определите

extract f = f i

Если i необитаем (недействителен), то i -> a - это тип устройства с единственным значением absurd. Void -> a - это просто еще один сложный пустой тип, который не содержит a s; рассматривайте это как структуру, которая может быть пустой.

Когда структура пуста

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

absurd :: Void -> a
absurd x = case x of {}

Пустые структуры могут быть Functor с fmap f = absurd. Точно так же они могут иметь экземпляр Apply с

(<.>) = absurd

Мы можем тривиально доказать это для всех u, v и w

(.) <$> u  <.> v  <.> w = u <.> (v <.> w)

Нет u, v или w, и требование неверно верно.

† С некоторыми предостережениями относительно принятия аксиомы выбора, чтобы выбрать индекс a для экспоненциального типа a -> b

Да...

... для Хаскелла. Представьте себе другую базу Monad, отличную от IO, назовем ее OI. Тогда Sum IO OI является Functor, но никогда не может быть Apply.

... для реального мира. Если у вас есть машина, на которую вы можете отправлять функции (или стрелки в категории, отличной от Hask), но не можете объединить две машины вместе или извлечь их рабочее состояние, то они являются функтором без применения ,

Ответ 2

Кажется, что "сумма" двух функторов (Data.Functor.Sum от transformers).

Можно легко отобразить одну ветвь или другую, но как реализовать <.>, когда функция-в-функторе и аргумент-в-функторе лежат в разных ветвях?

ghci> import Data.Functor.Sum
ghci> import Data.Functor.Identity
ghci> let f = InL (Const ())   :: Sum (Const ()) Identity (Int -> Int)
ghci> let x = InR (Identity 5) :: Sum (Const ()) Identity Int
ghci$ f <.> x = ..... ?

Ответ 3

Это не совсем то, что вы ищете, но оно закрывается, поэтому я решил поделиться этим. Стандартная монада Writer имеет дополнительное ограничение на свой экземпляр Apply (а именно, что тип w является экземпляром Monoid или Semigroup), который не имеет экземпляра Functor, так что Writer Foo является Functor, но не Apply, если Foo не является Semigroup/Monoid:

data Writer w a = Writer w a

instance Monoid w => Apply (Writer w) where
  Writer w1 f <.> Writer w2 x = Writer (mappend w1 w2) (f x)

Однако на самом деле это не пример того, о чем вы просите, потому что на самом деле можно создать закономерный экземпляр Apply без ограничения Monoid:

instance Apply (Writer w) where
  Writer w1 f <.> Writer w2 x = Writer w1 (f x)

Проблема с этим экземпляром заключается в том, что он не позволяет сопоставлять экземпляр Applicative, поскольку не существует способа реализовать pure, так что вы получите левую идентификационную информацию, то есть:

pure id <.> x /= x

Это всего лишь длинный способ дать вам тот же ответ, который у вас уже был из Conor: демонстрация, которая полагается на pure, чтобы разбить экземпляр.