Что такое Призмы?

Ответ 1

Линзы характеризуют отношения has-a; Призмы характеризуют отношения is-a.

Lens sa говорит, что " s имеет a "; у него есть методы, чтобы получить ровно один a из s и переписать ровно один a в s. Prism sa говорит: " a is s "; у него есть методы для повышения уровня a до s и (попытки) сбрасывать s в a.

Включение этой интуиции в код дает вам привычную "get-set" (или "costate comonad cocgebra") формулировку линз,

data Lens s a = Lens {
    get :: s -> a,
    set :: a -> s -> s
}

и "upcast-downcast" представление призмы,

data Prism s a = Prism {
    up :: a -> s,
    down :: s -> Maybe a
}

up вводит a в s (без добавления какой-либо информации), а down проверяет, является ли s a.

В lens up review и down preview. Нет конструктора Prism; вы используете умный конструктор prism'.

Что вы можете сделать с Prism? Типы вложений и проектов!

_Left :: Prism (Either a b) a
_Left = Prism {
    up = Left,
    down = either Just (const Nothing)
}
_Right :: Prism (Either a b) b
_Right = Prism {
    up = Right,
    down = either (const Nothing) Just
}

Объективы не поддерживают это - вы не можете написать Lens (Either ab) a потому что вы не можете реализовать get :: Either ab → a. Как практический вопрос, вы можете написать Traversal (Either ab) a, но это не позволяет вам создать Either ab из a - он позволит вам только перезаписать a который уже существует.

Кроме того: я думаю, что этот тонкий момент об Traversal является источником вашей путаницы в отношении частичных полей записей.

^? с обычными объективами позволяет получить Nothing если поле, о котором идет речь, не принадлежит ветке, представляющей сущность

Используя ^? с реальным Lens никогда не вернется Nothing, потому что Lens sa идентифицирует ровно один a внутри s. При столкновении с частичным полем записи,

data Wibble = Wobble { _wobble :: Int } | Wubble { _wubble :: Bool }

makeLenses генерирует Traversal, а не Lens.

wobble :: Traversal' Wibble Int
wubble :: Traversal' Wibble Bool

Для примера, как Prism может применяться на практике, посмотрите на Control.Exception.Lens, который предоставляет коллекцию Prism в расширяемой иерархии Exception Haskell. Это позволяет выполнять тесты типа времени выполнения в SomeException и вводить определенные исключения в SomeException.

_ArithException :: Prism' SomeException ArithException
_AsyncException :: Prism' SomeException AsyncException
-- etc.

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

Подводя итог, Lens es и Prism вместе кодируют два основных инструментария проектирования объектно-ориентированного программирования, составления и подтипирования. Lens es - это первоклассная версия Java . и =, а Prism - первоклассная версия Java instanceof и неявное повышение.

Одним из плодотворных способов мышления о Lens es является то, что они дают вам способ расщепления композита s на сфокусированное значение a и некоторый контекст c. псевдокод:

type Lens s a = exists c. s <-> (a, c)

В этой структуре Prism дает вам возможность взглянуть на s как на a и на некоторый контекст c.

type Prism s a = exists c. s <-> Either a c

(Я оставлю это вам, чтобы убедить себя, что они изоморфны простым представлениям, которые я продемонстрировал выше. Попробуйте реализовать get/set/up/down для этих типов!)

В этом смысле Prism является Lens co-. Either есть категорическое двойственное (,); Prism является категорическим двойником Lens.

Вы также можете наблюдать эту двойственность в "profunctor оптики" композиции - Strong и Choice двойственны.

type Lens  s t a b = forall p. Strong p => p a b -> p s t
type Prism s t a b = forall p. Choice p => p a b -> p s t

Это более или менее представление, которое использует lens, потому что эти Lens и Prism очень сложны. Вы можете составить Prism для получения большей Prism (" a является s, которая является p "), используя (.); составляя Prism с Lens дает вам Traversal.

Ответ 2

Я просто написал сообщение в блоге, которое могло бы помочь построить некоторую интуицию в отношении Призмы: Призмы - это конструкторы (Объективы - это поля). http://oleg.fi/gists/posts/2018-06-19-prisms-are-constructors.html

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

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

Чтобы представить документацию lens -library, законы призм:

Во-первых, если я review значение с Prism а затем preview, я верну его:

preview l (review l b) ≡ Just b

Во-вторых, если вы можете извлечь значение a с помощью Prism l из значения s, то значение s полностью описывается l и a:

preview l s ≡ Just a ⇒ review l a ≡ s

На самом деле, первого закона достаточно, чтобы доказать инъективность конструкции через Prism:

review l x ≡ review l y ⇒ x ≡ y

Доказательство прямолинейно:

review l x ≡ review l y
  -- x ≡ y -> f x ≡ f y
preview l (review l x) ≡ preview l (review l y)
  -- rewrite both sides with the first law
Just x ≡ Just y
  -- injectivity of Just
x ≡ y

Мы можем использовать свойство инъективности в качестве дополнительного инструмента в инструментальной панели эквационального рассуждения. Или мы можем использовать его в качестве простой собственности, чтобы проверить, является ли что-то законной Prism. Проверка проста, так как мы только review часть Prism. Многие интеллектуальные конструкторы, которые, например, нормализуют входные данные, не являются законными призмами.

Пример использования case-insensitive:

-- Bad!
_CI :: FoldCase s => Prism' (CI s) s
_CI = prism' ci (Just . foldedCase)

λ> review _CI "FOO" == review _CI "foo"
True

λ> "FOO" == "foo"
False

Также нарушен первый закон:

λ> preview _CI (review _CI "FOO")
Just "foo"

Ответ 3

В дополнение к другим отличным ответам, я чувствую, что Iso обеспечивает хорошую точку зрения для рассмотрения этого вопроса.

• Там быть некоторые i :: Iso' sa означает, что если у вас есть s значение вы (практически) есть a значение, и наоборот. Iso' дает вам две функции преобразования, view я :: s → a и review я :: a → s которые гарантированы как успешными, так и без потерь.

• Там, где l :: Lens' sa означает, что у вас есть s вас также есть a, но не наоборот. view l :: s → a может отбросить информацию на этом пути, поскольку преобразование не требуется без потерь, и поэтому вы не можете пойти другим путем, если все, что у вас есть, - это a (cf. set l :: a → s → s, что также требует s в дополнение к значению a, чтобы обеспечить недостающую информацию).

• Если есть какой-то p :: Prism' sa значит, если у вас есть значение s вас также может быть a, но нет никаких гарантий. preview p :: s → Maybe a конвертации preview p :: s → Maybe a не гарантируется успех. Тем не менее, у вас есть другое направление, review p :: a → s.

Другими словами, Iso является обратимым и всегда преуспевает. Если вы откажетесь от требования к обратимости, вы получите Lens; если вы откажетесь от гарантии успеха, вы получите Prism. Если вы бросите оба, вы получите аффинный обход (который не входит в объектив как отдельный тип), и если вы сделаете шаг дальше и откажитесь от того, что у вас будет не более одной цели, вы получите Traversal. Это отражено в одном из алмазов иерархии подтипов объектива:

 Traversal
    / \
   /   \
  /     \
Lens   Prism
  \     /
   \   /
    \ /
    Iso