Пример нетривиальных функторов

Ответ 1

Вот забавный аргумент, на который я только что наткнулся. (Уже поздно, поэтому мне интересно, будет ли это завтра чувственным)

Мы можем построить тип доказательств сводимости 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 расходится - и иногда это расходится, но вы не можете доказать это, и мой разум поражен тем, действительно ли это функтор в этом случае или нет)

Ответ 2

Явно пустые параметрические типы могут быть автоматически превращены в функторы:

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)

возможно, является юридической инстанцией.

Можно утверждать, что, используя основания, можно найти контрпример к законам функторов для приведенного выше примера. Однако в таком случае мне интересно, все ли "стандартные" экземпляры функторов на самом деле законны, даже при наличии дна. (Может они?)

Ответ 3

Нет нетривиальных функторов в смысле вопроса. Все функторы могут быть получены механически в виде сумм (Either) и произведений (Tuple) Identity и Const функтора. Посмотрите раздел о Функториальных алгебраических типах данных, чтобы узнать, как эта конструкция работает в деталях.

На более высоком уровне абстракции это работает, потому что тип Haskell формирует декартову замкнутую категорию, где существуют конечные объекты, все продукты и все экспоненты.

Ответ 4

Это немного обманывают, но здесь мы идем. Согласно этому тогда функтор не может быть получен автоматически, когда есть ограничение на тип, например.

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!

Ответ 5

Существует стандартный тип в 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 доступны два разных экземпляра, подсказывает мне, что ни один набор правил не может быть применен автоматически для охвата всех возможных случаев.