Пример нетривиальных функторов - PullRequest
Новая
       25

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

13 голосов
/ 03 июня 2019

В Haskell функторы почти всегда могут быть получены, есть ли случай, когда тип является функтором и удовлетворяет законам функтора (таким как fmap id == id), но не может быть получен в соответствии с простым набором правил?

А как насчет Foldable, Traversable, Semigroup и других? Есть ли в наличии нетривиальные случаи?

Ответы [ 5 ]

12 голосов
/ 03 июня 2019

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

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

9 голосов
/ 03 июня 2019

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

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)

возможно, это юридический пример.

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

9 голосов
/ 03 июня 2019

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

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

4 голосов
/ 03 июня 2019

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

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!
1 голос
/ 04 июня 2019

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

...