и почти вначале статьи:
or from a family of isomorphisms:
iso :: (a -> c) -> (d -> b) -> LensFamily a b c d
iso f g h a = fmap g (h (f a))
Почему пара (a -> c, d -> b) является изоморфизмом?
Те, я понимаю почему пара (to: a -> c, from: c -> a) является таковым - тк две функции можно связать условиями:
1. forall e: c. to (from e) == e
2. forall e: a. from (to e) == e
Но как что-то подбное можно сформулировать для (a -> c, d -> b)? У них же ведь типы никак не связанны.
Iso (Identity a) (Identity b) a b
это такой расширенный изоморфизм, чтобы, например, сначала A x превратить в B x, потом зайти внутрь x, поменять его на y, потом вернуться на уровень выше, к B y, и поменять его обратно на A y
это частный случай, но работает ли это всегда? Те существует ли, к примеру, такой исо Iso [a] (Maybe b) a b зная функции [a] -> a, b -> Maybe b? (интуитивно нет, но я не уверен какое отношение должно быть между s t a b, чтобы две функции являлись изоморфизмом)
корректной [a] -> a нет, но вообще почему нет?
А как тогда обратное преобразование c from построить? Те должно выполняться iso . from iso ≡ id from iso . iso ≡ id Те мы ведь не можем однозначно восстановить [a] из а.
[a] -> a мы тоже не можем. но дело в другом. в документации к библиотеке lens сказано, что f . from f ≡ id from f . f ≡ id это законы. то есть если не выполняются эти условия, то построенный объект Iso не будет правильным изоморфизмом
такой iso будет просто незаконный бтв iso интересен в своем определении type Iso s t a b = forall p f. (Profunctor p, Functor f) => p a (f b) -> p s (f t) iso должен работать для любого профунктора, что не позволит делать никаких замыканий например, где можно сохранить часть значений, чтобы потом восстановить (поэтому не выйдет сделать [a] ~ Maybe a) iso должен работать для любого функтора, что не позволит сделать 0 или 2 фокуса, строго 1
Нет, какой может быть изоморфизм между [] и Maybe?
Обсуждают сегодня