В Haskell функторы почти всегда могут быть получены, есть ли случай, когда тип является функтором и удовлетворяет законам функтора (таким как fmap id == id), но не может быть получен в соответствии с простым набором правил?
А как насчет Foldable, Traversable, Segigroup и других? Есть ли в наличии нетривиальные случаи?
Вот забавный аргумент, на который я только что наткнулся. (Уже поздно, поэтому мне интересно, будет ли это завтра чувственным)
Мы можем построить тип доказательств сводимости SK как GADT:
infixl 9 :%:
data Term = S | K | Term :%: Term
-- small step, you can get from t to t' in one step
data Red1 t t' where
Red1S :: Red1 (S :%: x :%: y :%: z) (x :%: z :%: (y :%: z))
...
Теперь давайте создадим тип, который скрывает свою функцию в конце цепочки сокращений.
data Red t a where
RedStep :: Red1 t t' -> Red t' a -> Red t a
RedK :: a -> Red K a
RedS :: (a -> Bool) -> Red S a
Теперь Red t является Functor если t нормализуется к K, но не если он нормализуется к S - неразрешимая проблема. Поэтому, возможно, вы все еще можете следовать "простому набору правил", но если вы разрешаете GADT, правила должны быть достаточно мощными, чтобы что-то вычислять.
(Существует альтернативная формулировка, которую я нахожу довольно элегантной, но, возможно, менее наглядной: если вы отбрасываете конструктор RedK, тогда Red t является Functor тогда и только тогда, когда система типов может выразить, что уменьшение t расходится - и иногда это расходится, но вы не можете доказать это, и мой разум поражен тем, действительно ли это функтор в этом случае или нет)
Явно пустые параметрические типы могут быть автоматически превращены в функторы:
data T a deriving Functor
Однако неявно пустые не могут:
import Data.Void
data T a = K a (a -> Void)
deriving Functor -- fails
{-
error:
• Can't make a derived instance of ‘Functor T:
Constructor ‘K must not use the type variable in a function argument
• In the data declaration for ‘T
-}
Тем не мение,
instance Functor T where
fmap f (K x y) = absurd (y x)
возможно, является юридической инстанцией.
Можно утверждать, что, используя основания, можно найти контрпример к законам функторов для приведенного выше примера. Однако в таком случае мне интересно, все ли "стандартные" экземпляры функторов на самом деле законны, даже при наличии дна. (Может они?)
Нет нетривиальных функторов в смысле вопроса. Все функторы могут быть получены механически в виде сумм (Either) и произведений (Tuple) Identity и Const функтора. Посмотрите раздел о Функториальных алгебраических типах данных, чтобы узнать, как эта конструкция работает в деталях.
На более высоком уровне абстракции это работает, потому что тип Haskell формирует декартову замкнутую категорию, где существуют конечные объекты, все продукты и все экспоненты.
Это немного обманывают, но здесь мы идем. Согласно этому тогда функтор не может быть получен автоматически, когда есть ограничение на тип, например.
data A a where
A1 :: (Ord a) => a -> A a
deriving instance Functor A -- doesn't work
и действительно, если (скажем) мы написали ручную версию, она тоже не будет работать.
instance Functor A where
fmap f (A1 a) = A1 (f a) -- Can't deduce Ord for f a
Однако, поскольку весь алгоритм выполняет проверку на отсутствие ограничений, мы можем ввести класс типов, членом которого является каждый тип.
class C c
instance C c
Теперь, как описано выше, с C вместо Ord,
data B b where
B1 :: (C b) => b -> B b
deriving instance Functor B -- doesn't work
instance Functor B where
fmap f (B1 b) = B1 (f b) -- does work!
Существует стандартный тип в base под названием Compose определяется следующим образом:
newtype Compose f g a = Compose { getCompose :: f (g a) }
Производный экземпляр Functor реализован следующим образом:
instance (Functor f, Functor g) => Functor (Compose f g) where
fmap f (Compose v) = Compose (fmap (fmap f) v)
Но есть еще один совершенно законный пример с другим поведением:
instance (Contravariant f, Contravariant g) => Functor (Compose f g) where
fmap f (Compose v) = Compose (contramap (contramap f) v)
Для меня тот факт, что для Compose доступны два разных экземпляра, подсказывает мне, что ни один набор правил не может быть применен автоматически для охвата всех возможных случаев.