Реализовать Applicative для пользовательского ZipList

Это взято из упражнения в книге Haskell from First Principles. Упражнение состоит в том, чтобы реализовать Applicative для ZipList', что аналогично ZipList в Prelude. В книге есть такая подсказка

Проверьте Prelude на наличие функций, которые могут дать вам то, что вам нужно. Один начинается с буквы z, другой с буквы r. Вы ищете вдохновение в этих функциях, чтобы не иметь возможности повторно использовать их напрямую, поскольку вы используете пользовательский тип List, а не предоставленный тип списка Prelude.

Я предположил, что функция, которая начинается с z, это zipWith, но я не знаю о функции, которая начинается с r.

data List a =
    Nil
  | Cons a (List a)
  deriving (Eq, Show)

zipWith' :: (a -> b -> c) -> List a -> List b -> List c
zipWith' _ Nil _ = Nil
zipWith' _ _ Nil = Nil
zipWith' f (Cons x xs) (Cons y ys) = Cons (f x y) (zipWith' f xs ys)

newtype ZipList' a = ZipList' (List a)
  deriving (Eq, Show)

instance Functor ZipList' where
  fmap f (ZipList' xs) = ZipList' $ fmap f xs

instance Applicative ZipList' where
  pure x = ZipList' $ Cons x Nil
  (ZipList' fs) <*> (ZipList' xs) = ZipList' $ zipWith' ($) fs xs

Это проходит тестовый пример в книге, но мне интересно, есть ли лучший способ реализовать это, поскольку я не использовал функцию, начинающуюся с r. У меня есть ощущение, что это должно было быть repeat, потому что оно также должно работать с бесконечными списками.


typeclass custom-data-type haskell algebraic-data-types applicative
person Brady Dean    schedule 28.10.2019    source источник
comment
Похоже, ваш instance Applicative работает над типом ZipList', который вы здесь не определили?   -  person Willem Van Onsem    schedule 28.10.2019
comment
@WillemVanOnsem Забыл это вставить, я обновил вопрос   -  person Brady Dean    schedule 28.10.2019
comment
Ваш pure неверен, и как только вы разберетесь с правильной реализацией, вы увидите, о какой функции, начинающейся с r, идет речь. Ключ должен думать о требовании законного Applicative экземпляра, который fmap f x == (pure f) <*> x, и признать, что не существует верхнего предела длины списка x. Этого должно быть достаточно для того, чтобы вы поняли это.   -  person Robin Zigmond    schedule 28.10.2019
comment
@RobinZigmond pure 1 :: ZipList Int создает бесконечный список, так что это, кажется, моя проблема, я сейчас пытаюсь понять, как это удовлетворяет закону.   -  person Brady Dean    schedule 28.10.2019

Ответы (2)


arrow_upward
3
arrow_downward

Читая ветку под исходным постом, я пришел к выводу, что автор поста пытается доказать, что реализация удовлетворяет закону (fmap f xs = (pure f) <*> xs):

Попробуем доказать это как классическое тождество, избавившись от обертки. Итак, поработаем правой рукой:

(pure f) <*> xs = (repeat' f) <*> xs = zipWith' ($) (repeat' f) xs;

Что касается идентичности, достаточно доказать, что zipWith' ($) (repeat' f) xs равно fmap f xs.

Причина, по которой они одинаковы, довольно очевидна:

length (zipWith op xs ys) == min (length xs) (length ys); (это выражение не может быть вычислено в случае, если и xs, и ys бесконечны).

Поскольку repeat' f бесконечно, length $ zipWith' ($) (repeat' f) xs фактически равно length xs (здесь фактически не имеет значения, существует ли такое значение: достаточно существования индексов). Каждый элемент xs применяется к одной и той же функции f, которая повторяется. Как видите, размер сохраняется, и каждый элемент трансформируется постоянной функцией, которая является определением fmap.

person Zhiltsoff Igor    schedule 28.10.2019
comment
вы можете сделать его формальным с помощью структурной индукции, заменив определения zipWith, repeat и map: zW ($) (f:rep f) (x:xs) = (f $ x) : zW ($) (rep f) xs = (f x) : map f xs, где zW ($) (rep f) xs == map f xs соответствует IH, а zW ($) (rep f) [] = [] = map f [] является базовым случаем. - person Will Ness; 28.10.2019
comment
@WillNess Правда, это то, что я хотел опубликовать изначально, но в чем смысл, если у нас есть все определения под рукой? Иногда RT-анализ может оказаться куда более полезным навыком, чем строгое доказательство. - person Zhiltsoff Igor; 28.10.2019
comment
пожалуйста, что такое РТ? - person Will Ness; 28.10.2019
comment
Анализ времени выполнения @WillNess. (Извините, должно было быть «и», а не «е», т.е. не во множественном числе). - person Zhiltsoff Igor; 28.10.2019

arrow_upward
2
arrow_downward

Я немного подумал об этом после комментария Робина Зигмонда:

Суть в том, чтобы подумать о требовании законного Applicative экземпляра, который fmap f x == (pure f) <*> x, и признать, что нет верхнего предела длины списка x.

Эта реализация должна удовлетворять применимым законам.

data List a =
    Nil
  | Cons a (List a)
  deriving (Eq, Show)

zipWith' :: (a -> b -> c) -> List a -> List b -> List c
zipWith' _ Nil _ = Nil
zipWith' _ _ Nil = Nil
zipWith' f (Cons x xs) (Cons y ys) = Cons (f x y) (zipWith' f xs ys)

repeat' :: a -> List a
repeat' x = Cons x $ repeat' x

newtype ZipList' a = ZipList' (List a)
  deriving (Eq, Show)

instance Functor ZipList' where
  fmap f (ZipList' xs) = ZipList' $ fmap f xs

instance Applicative ZipList' where
  pure x = ZipList' $ repeat' x
  (ZipList' fs) <*> (ZipList' xs) = ZipList' $ zipWith' ($) fs xs
person Brady Dean    schedule 28.10.2019
comment
Да, именно так :-) Можете сами убедиться, сравнив со строкой официальная реализация (в конце кода) - person Robin Zigmond; 28.10.2019