Ответ 1
Важно, если вы можете делать другие вещи с типом, а не просто extract от него. Интуитивно, если единственное, что вы можете сделать, это извлечь значение, тогда тип содержит только одно значение, поэтому дублирование этого значения дублирует все. Это вообще не так, и это не так для молний.
Законы Comonad - это просто законы категории, маскирующиеся на функции типа w a -> b. Поскольку они исходят из категорий, было бы легче рассуждать о них по категории, а не по законам Comonad. extract является личностью этой категории, а =<= является оператором композиции.
-- | Right-to-left 'Cokleisli' composition
(=<=) :: Comonad w => (w b -> c) -> (w a -> b) -> w a -> c
f =<= g = f . extend g
Мы также знаем, что extend f = fmap f . duplicate, поэтому мы можем написать
f =<= g = f . fmap g . duplicate
Это выглядит довольно легко рассуждать. Теперь позвольте оборудовать ваш тип Z другой функцией, о которой мы можем поговорить. isFirst вернет true только тогда, когда Z представляет значение в позиции в списке, в котором ничего нет.
isFirst :: Z a -> Bool
isFirst (Z [] _ _) = True
isFirst _ = False
Теперь рассмотрим, что происходит, когда мы используем isFirst с тремя законами категории. Кажется, что единственное, что кажется ему применимым, - это то, что extract является левым и правым тождеством для композиции по =<=. Поскольку мы только опровергаем это, нам нужно найти встречный пример. Я подозреваю, что один из extract =<= isFirst или isFirst =<= extract не будет введен для ввода Z [1] 2 []. Оба они должны быть такими же, как isFirst $ Z [1] 2 [], который равен False. Сначала мы попробуем extract =<= isFirst, что будет работать.
extract =<= isFirst $ Z [1] 2 []
extract . fmap isFirst . duplicate $ Z [1] 2 []
extract . fmap isFirst $ Z [] (Z [1] 2 []) []
extract $ Z [] (isFirst (Z [1] 2 [])) []
extract $ Z [] False []
False
Когда мы попробуем isFirst =<= extract, нам не повезет.
isFirst =<= extract $ Z [1] 2 []
isFirst . fmap extract . duplicate $ Z [1] 2 []
isFirst . fmap extract $ Z [] (Z [1] 2 []) []
isFirst $ Z [] (extract (Z [1] 2 [])) []
isFirst $ Z [] 2 []
True
Когда мы duplicate d, мы потеряли информацию о структуре. Фактически, мы потеряли информацию обо всем, что получилось везде, кроме единственного фокуса на молнии. Правильный duplicate имел бы всю "застежку-молнию" всюду в контексте, содержащую значение в этом местоположении и этот контекст местоположения.
Посмотрим, что мы можем вывести из этих законов. С небольшой рукой, размахивающей о категории функций, мы можем видеть, что =<= extract есть fmap extract . duplicate, и это должна быть функция тождества. По-видимому, я заново открываю, как законы написаны в документации для Control.Category. Это позволяет нам написать что-то вроде
z = (=<= extract) z
z = fmap extract . duplicate $ z
Теперь Z имеет только один конструктор, поэтому мы можем заменить это на
Z left x right = fmap extract . duplicate $ Z left x right
Из типа дубликата мы знаем, что он должен возвращать тот же самый конструктор.
Z left x right = fmap extract $ Z lefts (Z l x' r) rights
Если применить fmap к этому Z, мы имеем
Z left x right = Z (fmap extract lefts) (extract (Z l x' r)) (fmap extract rights)
Если мы разделим его на части конструктора Z, мы получим три уравнения:
left = fmap extract lefts
x = extract (Z l x' r)
right = fmap extract rights
Это говорит нам о том, что, по крайней мере, результат duplicate (Z left x right) должен выполняться:
- список с той же длиной, что и
leftдля левой стороны - a
Zсxпосередине для среднего - список с той же длиной, что и
rightдля правой стороны
Кроме того, мы можем видеть, что средние значения в списках слева и справа должны быть такими же, как и исходные значения в этих списках. Учитывая только этот закон, мы достаточно знаем, чтобы потребовать другую структуру для результата duplicate.