镜头和部分镜头有什么区别？ [英] What's the difference between a lens and a partial lens?
问题描述
标记Scala和Haskell，但我希望解释与任何具有镜头库的功能语言有关的解释。
根据Haskell 镜头描述部分镜片 - 我将从此调用命名，棱镜（除了它们不是！见Ørjan的评论） - 我想先从不同的角度看镜头本身。
镜头 Lens sa 表示给定一个 s ，我们可以关注一个<$ c $的子组件在 a 类型中查看它，替换它，并且（如果我们使用镜头族变体镜头刺）甚至改变它的类型。
看这个的一个方法是 Lens sa 证明了 s 和元组类型（r，a）之间的一个同构，等价，未知类型 r 。 p>
Lens s a ======存在r。 s〜（r，a）
这给了我们我们需要的东西，因为我们可以将 a out，替换它，然后通过等价性向后运行，得到一个新的 s ，并更新 a 。
现在让我们花一分钟通过代数来刷新我们的高中代数数据类型。 ADT中的两个关键操作是乘法和求和。当我们有一个由 和的项组成的类型时，我们编写 a * b $ c>和一个 b ，当我们有一个类型为 a 或 b 。
在Haskell中，我们将 a * b 写为元组类型，即（a，b）。我们将 a + b 写为或者ab ，这两种类型之一。
产品表示将数据捆绑在一起，总和表示将捆绑在一起的选项。产品可以代表有许多事情的想法，你只能选择其中一种（一次），而总和代表失败的想法，因为你希望采取一种选择（在 left ），而不得不为另一个（沿着 right ）解决。
最后，总和和产品是分类对偶。他们合在一起，并且有一个没有另一个，因为大多数PL都会让你处于一个尴尬的地方。
所以让我们来看看当我们将上面的镜片公式化为 dualize （部分）时会发生什么。
r存在。 s〜（r + a）
这是 s 是 类型 a 或其他一些东西 r code>。我们有一个镜头型的东西，它体现了选择（和失败）的核心概念。
这完全是一个棱镜（或部分镜头）
Prism sa ======存在r。 s〜（r + a）
存在r。 s〜或者ra
那么这对于一些简单的例子是如何工作的呢？
好吧，考虑棱镜不合列表：
uncons :: Prism [a ]（a，[a]）
相当于这个
head :: exists r。 [a]〜（r +（a，[a]））
为证实类型需要在这里：我们需要写一种方法将 a 转换为 b 并且一个 b 转换为 a ，这样它们可以相互反转。让我们写这个来描述我们的棱镜通过神话功能
$ pre $ prism ::（s〜exists r。或者ra） - > Prism s a
uncons = prism（iso fwd bck）其中
fwd [] = Left（） - 失败！
fwd（a：as）= Right（a，as）
bck（Left（））= []
bck（Right（a，as））= a：as
这说明如何使用这种等价（至少原则上）来创建棱镜，并且还表明他们应该感受当我们处理像列表这样的总和类型时，这真的很自然。
A "lens" and a "partial lens" seem rather similar in name and in concept. How do they differ? In what circumstances do I need to use one or the other?
Tagging Scala and Haskell, but I'd welcome explanations related to any functional language that has a lens library.
To describe partial lenses—which I will henceforth call, according to the Haskell lens nomenclature, prisms (excepting that they're not! See the comment by Ørjan)—I'd like to begin by taking a different look at lenses themselves.
A lens Lens s a indicates that given an s we can "focus" on a subcomponent of s at type a, viewing it, replacing it, and (if we use the lens family variation Lens s t a b) even changing its type.
One way to look at this is that Lens s a witnesses an isomorphism, an equivalence, between s and the tuple type (r, a) for some unknown type r.
Lens s a ====== exists r . s ~ (r, a)
This gives us what we need since we can pull the a out, replace it, and then run things back through the equivalence backward to get a new s with out updated a.
Now let's take a minute to refresh our high school algebra via algebraic data types. Two key operations in ADTs are multiplication and summation. We write the type a * b when we have a type consisting of items which have both an a and a b and we write a + b when we have a type consisting of items which are either a or b.
In Haskell we write a * b as (a, b), the tuple type. We write a + b as Either a b, the either type.
Products represent bundling data together, sums represent bundling options together. Products can represent the idea of having many things only one of which you'd like to choose (at a time) whereas sums represent the idea of failure because you were hoping to take one option (on the left side, say) but instead had to settle for the other one (along the right).
Finally, sums and products are categorical duals. They fit together and having one without the other, as most PLs do, puts you in an awkward place.
So let's take a look at what happens when we dualize (part of) our lens formulation above.
exists r . s ~ (r + a)
This is a declaration that s is either a type a or some other thing r. We've got a lens-like thing that embodies the notion of option (and of failure) deep at it's core.
This is exactly a prism (or partial lens)
Prism s a ====== exists r . s ~ (r + a)
exists r . s ~ Either r a
So how does this work concerning some simple examples?
Well, consider the prism which "unconses" a list:
uncons :: Prism [a] (a, [a])
it's equivalent to this
head :: exists r . [a] ~ (r + (a, [a]))
and it's relatively obvious what r entails here: total failure since we have an empty list!
To substantiate the type a ~ b we need to write a way to transform an a into a b and a b into an a such that they invert one another. Let's write that in order to describe our prism via the mythological function
prism :: (s ~ exists r . Either r a) -> Prism s a
uncons = prism (iso fwd bck) where
fwd [] = Left () -- failure!
fwd (a:as) = Right (a, as)
bck (Left ()) = []
bck (Right (a, as)) = a:as
This demonstrates how to use this equivalence (at least in principle) to create prisms and also suggests that they ought to feel really natural whenever we're working with sum-like types such as lists.
这篇关于镜头和部分镜头有什么区别？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
