Пример нарушения правил Функтора в Haskell - PullRequest
Новая
       4

Пример нарушения правил Функтора в Haskell

1 голос
/ 02 февраля 2020

У меня есть структура данных для бинарного дерева и Функтор над ним 

data BST a = Empty | Node (BST a) a (BST a)
instance Functor BST  where
  fmap f Empty = Empty
  fmap f (Node l val r) = (Node (fmap f l) (f val  ) (fmap f r))

Мне нужно найти пример некоторого экземпляра BST и функции f, где правила Функтора (Идентификация, состав) нарушены

Может ли кто-нибудь указать мне правильное направление?

Спасибо!

1 Ответ

0 голосов
/ 03 февраля 2020

Вы не найдете никакого примера, потому что ваше определение содержит функтор l aws. Вы можете доказать это путем наведения на глубину дерева. Базовым случаем является дерево глубиной 0 (т. Е. Empty), тогда доказательство для случая Node. Доказательство длинное, но прямое.

Редактировать:

перечитывая ваш вопрос, может быть, вы ищете определение fmap проверки этого типа, но не удерживаете funtor l aws. Просто используйте 

data BST a = Empty | Node (BST a) a (BST a)
instance Functor BST  where
  fmap f Empty = Empty
  fmap f (Node l val r) = (Node (fmap f r) (f val  ) (fmap f l))
--                                      |- notice            |- notice

Почему он не держит l aws? Это на тебе. ниже доказательство того, что ваше определение действительно. Попробуйте создать собственное доказательство того, почему мое определение не

Первый закон 

fmap id == id

Базовый случай 

fmap id Empty = Empty    -- by definition of fmap
              = id Empty -- by definition of id
=> fmap id = id          -- by eta-reducing both sides of the equation

Рекурсивный случай

Supose что гипотеза верна для всех деревьев данной глубины D (или меньше). Доказательство для дерева на одну глубину (D + 1)

fmap id (Node l val r) = Node (fmap id l) (id val) (fmap id r) -- by definition of fmap
                       = Node (fmap id l) val      (fmap id r) -- by applying id to val
                       = Node l val r                          -- by induction hyp. fmap id l == l
                       = id (Node l val r)                     -- by definition of id
=> fmap id             = id                                    -- by eta-reducing both sides of the equation

Второй закон 

 fmap g . fmap f == fmap (g . f)

Базовый случай 

-- Eq 1
(fmap g . fmap f) Empty = fmap g (fmap f Empty)  -- by definition of .
                        = fmap g Empty           -- by definition of fmap
                        = Empty                  -- by definition of fmap
-- Eq 2
fmap (g . f) Empty      = Empty                  -- by definition of fmap

-- Therefore
(fmap g . fmap f) Empty = fmap (g . f) Empty     -- By transition of equality on Eq1 and Eq2
fmap g . fmap f         = fmap (g . f)           -- by eta-reducing both sides of the equation

Рекурсивный случай

Supose что гипотеза верна для всех деревьев данной глубины D (или меньше). Пруф для дерева одна глубина (D + 1)

-- Eq 1
fmap (g . f) (Node l val r) = Node (fmap (g . f) l) 
                                   ((g . f) val) 
                                   (fmap (g . f) r) -- by definition of fmap

                            = Node ((fmap g . fmap f) l) 
                                   ((g . f) val) 
                                   ((fmap g . fmap f) r) -- by induction hyp.

-- Eq 2
(fmap g . fmap f) (Node l val r) = fmap g (fmap f (Node l val r)) -- dy definition of .
                                 = fmap g $ Node (fmap f l) 
                                                 (f val) 
                                                 (fmap f r)       -- by definition of fmap
                                 = Node (fmap g (fmap f l))
                                        (g (f val))
                                        (fmap g (fmap f r))       -- by definition of fmap
                                 = Node ((fmap g . fmap f) l) 
                                        ((g . f) val) 
                                        ((fmap g . fmap f) r)     -- by induction hyp.

fmap (g . f) (Node l val r) = (fmap g . fmap f) (Node l val r)    -- By transition of equality on Eq1 and Eq2
fmap (g . f)                = (fmap g . fmap f)                   -- by eta-reducing both sides of the equation
...