Хорошие примеры не Contravariant / Contravariant / Divisible / Decidable? - PullRequest
Новая
       56

Хорошие примеры не Contravariant / Contravariant / Divisible / Decidable?

9 голосов
/ 14 мая 2019

Семейство Contravariant классов типов представляет стандартные и фундаментальные абстракции в экосистеме Haskell: 

class Contravariant f where
    contramap :: (a -> b) -> f b -> f a

class Contravariant f => Divisible f where
    conquer :: f a
    divide  :: (a -> (b, c)) -> f b -> f c -> f a

class Divisible f => Decidable f where
    lose   :: (a -> Void) -> f a
    choose :: (a -> Either b c) -> f b -> f c -> f a

Однако, не так просто понять концепции, лежащие в основе этих классов типов.Я думаю, это помогло бы лучше понять эти классы типов, если бы вы могли увидеть некоторые контрпримеры для них.Итак, в духе Хороших примеров Не Функтор / Функтор / Аппликатив / Монада? , я ищу контрастные примеры типов данных, которые удовлетворяют следующим требованиям:

  • Конструктор типа, который не является Contravariant?
  • Конструктор типа, который является Contravariant, но не Divisible?
  • Конструктор типа, которыйэто Divisible, но не Decidable?
  • Конструктор типа, который является Decidable?

Ответы [ 2 ]

6 голосов
/ 14 мая 2019

(частичный ответ)

Не контравариантно 

newtype F a = K (Bool -> a)

не является контравариантным (это, однако, ковариантный функтор).

Контравариант, но не делится 

newtype F a = F { runF :: a -> Void }

является контравариантным, но не может быть Divisible, поскольку в противном случае 

runF (conquer :: F ()) () :: Void

Примечание о "делимых, но не разрешимых"

У меня нет разумного примера делимого, которое нельзя решить. Мы можем заметить, что такой контрпример должен быть таким, потому что он нарушает законы, а не только сигнатуру типа. Действительно, если Divisible F выполнено, 

instance Decidable F where
    lose _ = conquer
    choose _ _ _ = conquer

удовлетворяет сигнатурам типов методов.

В библиотеках мы находим Const m как делимое, когда m является моноидом. 

instance Monoid m => Divisible (Const m) where
  divide _ (Const a) (Const b) = Const (mappend a b)
  conquer = Const mempty

Возможно, это не может быть законным Decidable? (Я не уверен, кажется, что он удовлетворяет Decidable законам, но в библиотеках нет экземпляра Decidable (Const m).)

Разрешимый

Взято из библиотек: 

newtype Predicate a = Predicate (a -> Bool)

instance Divisible Predicate where
  divide f (Predicate g) (Predicate h) = Predicate $ \a -> case f a of
    (b, c) -> g b && h c
  conquer = Predicate $ const True

instance Decidable Predicate where
  lose f = Predicate $ \a -> absurd (f a)
  choose f (Predicate g) (Predicate h) = Predicate $ either g h . f
5 голосов
/ 14 мая 2019

(частичный производный ответ?)

Я верю, что @chi верен , когда они выдвигают гипотезу , что Const m не может быть законным Decidable длявсе Monoid s m, но я основываю это на предположениях о Decidable законах.

В документах мы получаем этот дразнящий намек на Decidable law:

Кроме того, мы ожидаем того же рода закона распределения, который удовлетворяет обычная ковариантная альтернатива, по отношению к Applicative, которая должна быть полностью сформулирована и добавлена ​​здесь в какой-то момент!

Какого рода распределительные отношения должны быть между Decidable и Divisible?Ну, у Divisible есть chosen, который строит вещь, принимающую продукт, из элементов, принимающих элементы, и Decidable имеет divided, которая строит вещь, принимающую сумму из вещей, принимающих элементы.Поскольку продукты распределяются по суммам, возможно, закон, который мы ищем, относится от f (a, Either b c) к f (Either (a, b) (a, c)), значения которых можно построить с помощью a `divided` (b `chosen` c) и (a `divided` b) `chosen` (a `divided` c) соответственно.

Так что я буду выдвигать гипотезучто отсутствующий закон Decidable является чем-то вроде 

a `divided` (b `chosen` c) = contramap f ((a `divided` b) `chosen` (a `divided` c))
  where f (x, y) = bimap ((,) x) ((,) x) y

, что действительно удовлетворяется для Predicate, Equivalence и Op (три Decidable случая, которые я принялпока что время проверять).

Теперь я считаю, что единственный экземпляр, который вы можете иметь для instance Monoid m => Decidable (Const m), использует mempty для lose и mappend для choose;любой другой выбор, а затем lose больше не является идентификатором для choose.Это означает, что вышеприведенный закон распределения упрощает до 

a `mappend` (b `mappend` c) = (a `mappend` b) `mappend` (a `mappend` c)

, что является явно фальшивым неправдой в произвольном Monoid (хотя, как замечает Сьорд Висшер, в некоторых * 1058 это верно* s - так что Const m все еще может быть законным Decidable, если m является распределительным моноидом).

...