Shattered lensOleg Grenrus
Well-Typed LLP
oleg.grenrus@iki.fi

Very well-behaved lenses do not describe a (virtual) field of a record as we might intuitively think.
Updating a structure through a lens can cause changes in the other parts of the structure in a larger
extent than what is visible through the getter part. That is evident by considering homotopic descriptions of lenses which also suggests that the setter part is the defining part of the lens. On the other
hand prisms can be seen as “generalized constructors”. Builder and matcher uniquely define eachother.

1Introduction

A very well-behaved lens [4] from a structure type S to a value type V is usually specified using twofunctions, a getter f : S → V and a setter g : S → V → S. These functions are required to satisfy threelaws:
GetPut f g := ∏ ∏ f (g s v) = b

PutGet f g := ∏ g s ( f s) = s

s:S v:Vs:S

0PutPut g := ∏ ∏ g (g s v ) v = g s v
s:S v v0 :B

The type of lens is thenLens S V :=GetPut f g × PutGet f g × PutPut g∑( f ,g):(S→V )×(S→V →S)This formulation is problematic if we want to talk about the equality of lenses, for example to prove theassociativity of lens composition. We need to show that law evidences are also equal which may not
be easy as we do not have uniqueness of identity proofs because it is not consistent with univalence.
Compare that with the definitions of isomorphism and equivalence in homotopy type theory. We will
introduce the concepts needed in Appendix A using the standard reference for homotopy type theory:the “HoTT Book“ [5].
Paolo Capriotti proposes the following definition for higher lens [1].
Definition 1.1. A higher lens is a dependent triple
HigherLens S V :=∑∑∏(fiber f v ' P |v|).

f :S→V P:kV k→Type v:V

where fiber f b := ∑a:A ( f a = b) (Definition A.4).
This formulation is equivalent to to an equivalence-lens definition [3]:ELens S V :=∑ (S ' (V × R)) × (R → kV k).
R:TypeSubmitted to:
MSFP2020

c Oleg Grenrus
This work is licensed under the Creative Commons
Attribution-Share Alike License.

2

Shattered Lens

However, these definitions are not easy to work with. The restricting types are not mere propositions asisEquiv (Definition A.5) in case of equivalence. More concretely, the f in the HigherLens definition does
not determine the lens completely. There is non-unique computational content for a setter “hidden” inthe fiber equivalence. It is wrong to only say “ f is a lens” without mentioning how the setter is defined.
We can illustrate this by a small example. See Appendix B for an analogous real-world example.
f :: (Bool, Bool) → Boolf = fstg :: (Bool, Bool) → Bool → (Bool, Bool)g (x, r) y = (y, xor y (xor r x))
It would be highly misleading to call the lens formed from f and g by the getter: fst.
The corresponding higher lens has f = fst and P x = Bool as the first and second fields of a triple.
The third field, a dependent function ∏v:Bool fiberfst v ' Bool, determines the behaviour of the setter.
In fact there are two values which produce the same behaviour, assigning id and not equivalences todifferent values of v. This means that can construct two observably different higher lenses which gettersand setters are equal to f and g. This suggests that HigherLens is “bigger” than Lens (when S and V areh-sets).
The above invites one to look into the homotopic representations of lenses more closely.

2Prisms

Before investigating lenses we look at prisms. Their theory turns out to be quite simple. Prisms are tocoproducts what lenses are to products. A Prism S V is usually specified using two functions, a builder
g : V → S and a matcher f : S → Maybe V . Prisms can also be defined by requiring that the builder
function is a decidable embedding i.e. a function whose fibers are decidable propositions.
Definition 2.1. A function f : A → B is an embedding if for every a : A its fibers are mere propositions:
hasPropFibers f := ∏ isProp (fiber f b).
a:ADefinition 2.2. A type P is decidable if P or ¬P:
Dec P = P + ¬P
Definition 2.3. A function g : V → S is a prism when a proof of isPrism g can be constructed
isPrism g := hasPropFibers g × ∏ Dec (fiberg s)
s:SPrism S V :=∑ isPrism g

g:V →S.
isPrism is a mere proposition because the product of propositions is one, hasPropFibers is a mereproposition and Dec P is a mere proposition if P is. As a corollary, it is easy to show that composition ofprisms is associative.
Contrary to the lens case, saying “a function g is a prism” is justified. The matching function isuniquely defined. To match on a value use the ∏s:S Dec (fiberg s) part. You will either get a fiber whichcontains a value of type V , or a proof that there cannot be one.

Oleg Grenrus

33Lenses

We will try to understand lenses by considering fibers of a getter. We start with a barely behaving lens
which satisfies GetPut law. It can be further strengthened in few ways by imposing addition restrictions
on the fiber mapping.
• If we require the mapping to be an equivalence, we do not get a previously known variant of lenses.
We call such lenses weak.
• If we require the mapping to not change the fiber when v1 = v2 , we get a well-behaved lens which
also satisfies the PutGet law.
• The HigherLens (Definition 1.1) can be thought as requiring the mapping to go through a single(or more correctly: coherently constant) type P |v|.
Definition 3.1. A function f : S → V is a barely behaving lens if it comes together with a value offollowing type:hasBareLens f := ∏ ∏ (fiber f v1 → fiber f v2 )v1 :v v2 :VDefinition 3.2. A function f : S → V is a weak lens if it comes together with a value of following type:
hasWeakLens f := ∏ ∏ (fiber f v1 ' fiber f v2 )v1 :V v2 :VDefinition 3.3. A function f : S → V is a well-behaving lens (the name is due to [4]) if it is a barely
behaving lens with a proof p : hasBareLens f and additionally the following type is inhabited:∏ ∏pvvx=xv:V x:fiber f b

While the definitions above might be useful in various applications, none of them definitions is amere proposition. There does not seem to be a simple way to strenghten HigherLens further.
For prisms we have found an elegant approach of building on top of a known concept: an embedding.
We can try whether related surjection can be used to characterize lens. It is surprising at first that none of
the lens representations allow to show that the getter is a surjection. We end up needing an assumption
like kS + ¬Sk which is not a huge requirement, but a requirement nevertheless.
On the other hand, the setter part when thought as a function S × V → S can be shown to be asurjection when the PutGet law holds, i.e. for well-behaved lenses and stronger variants. Alternatively
we take the setter to be the primary building block of lenses:
Definition 3.4. A function g : S → V → S has getter when
hasGetter g := ∏ isContr (fiberg s s)
s:S

hasGetter is a mere proposition, and lets us show the PutGet law. Interestingly to show the GetPut
law we need a simpler variant of the PutPut law, essentially asking that the setter is idempotent:
Definition 3.5.
idempotentSetter g := ∏ ∏ g (g s v) v = g s v
s:S v:VThe above suggests that the setter is the defining part of a lens. The compatible getter is uniquelydetermined. Yet, we do not yet know what a “higher setter“ would look like. That is a topic for furtherwork.

4

Shattered Lens

References[1] Paolo Capriotti: Higher Lenses. https://homotopytypetheory.org/2014/04/29/higher-lenses/.
Accessed: 2020-03-15.
[2] Koen Claessen & John Hughes (2000): QuickCheck: A Lightweight Tool for Random Testing ofHaskell Programs. In: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, ICFP 00, Association for Computing Machinery, New York, NY, USA, pp. 268–279,
doi:10.1145/351240.351266.
[3] Nils Anders Danielsson: Dependent Lenses. http://www.cse.chalmers.se/~nad/publications/danielsson-dependent-lenses.pdf. Accessed: 2020-03-15.
[4] J. Nathan Foster, Michael B. Greenwald, Jonathan T. Moore, Benjamin C. Pierce & Alan Schmitt (2007):
Combinators for Bidirectional Tree Transformations: A Linguistic Approach to the View-Update Problem.
ACM Trans. Program. Lang. Syst. 29(3), doi:10.1145/1232420.1232424.
[5] The Univalent Foundations Program (2013): Homotopy Type Theory: Univalent Foundations of Mathematics.
https://homotopytypetheory.org/book, Institute for Advanced Study.
[6] Andrea Vezzosi, Anders Mörtberg & Andreas Abel (2019): Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types. Proc. ACM Program. Lang. 3(ICFP),
doi:10.1145/3341691.

AHomotopy Type Theory overview

As we mentioned in the introduction, the “HoTT Book“ [5] is the standard reference for homotopy typetheory. The functional programming language AGDA has been recently extended into C UBICAL AGDA[6], giving computation interpretation to the homotopy type theory. The statements in this paper aretranslated from C UBICAL AGDA code.
Homotopy type theory is based on a dependent type theory with• dependent function types (a 7→ . . .) : ∏a:A B(a);• dependent pair types ha; bi : Σa:A B(a) (we name projections fst and snd);• universe types we call just Type as we omit level issues for brevity,• non-dependent product types ha; bi : A × B (with projections named proj1 and proj2 );• empty type ⊥, and negation ¬A := A → ⊥;• coproduct types A + B; with constructors inl and inr1 ;• Booleans true : Bool; false : Bool
• ...
Definition A.1 (Identity types). There is a type family of identity types IdA : A → A → Type. It is also
called the path space of A. We use a standard notation a =A b or just a = b to denote that two elementsof the same type a, b : A are equal. The introduction rule is a dependent function
refl : ∏(a =A a).
a:A

Definition A.2 (Homotopy levels). Types can be classified according to their homotopy-level. Homotopy
levels are cumulative.
1 in AGDA code the A ] B is used to avoid clash with addition on natural numbers

Oleg Grenrus

5• A type is contractible when it has an element to which all others elements are equal
isContr A := ∑ ∏(x = y).
x:A y:A• A type is mere proposition when all its elements are equal:
isProp A := ∏ (x = y)x y:AMere propositions values a proof irrelevant: they are all equal if they exist. However, not as types
C OQ in Prop universe, values of mere proposition types can be eliminated into non-proposition
types too. isContr A and isProp A are itself mere propositions.
• A type is h-set when its path space is mere proposition.
isSet A := ∏ isProp (x = y)x y:AFor h-sets the uniqueness of identity proofs holds.
Definition A.3. It is possible to truncate any type to be a mere proposition, using propositional truncation|a| : kAk
The downside of using propositional truncation is that values of type kAk can be eliminated onlywith mere proposition motives.
Definition A.4. A fiber of a map f : A → B is the type of its pre-image values:
fiber f b := ∑( f a = b)a:ADefinition A.5. A function f : A → B is an equivalence if all its fibers are contractible:
isEquiv f := ∏ isContr (fiber f b)b:B

isEquiv f is a mere proposition which implies that there is the unique inverse function:f −1 isEquiv-f b := fst (isEquiv-f b).
Using isEquiv we define equivalence of types as:
A ' B :=

∑ isEquiv f

f :A→B

Theorem A.6. Using the just defined equivalence we can state the univalence axiom:
univalence := (A ' B) ' (A = B)
Though we call it an axiom, in cubical type theories like in C UBICAL AGDA it does compute. We
will not use the axiom directly, but it is nevertheless important to mention. For an example note that
Bool = Bool type is not contractible, there are also other values than refl.
Theorem A.7. Given a type A and a type family B : A → Type, consider the dependent functions f , g :∏a:A B a. The following functional extensionality equivalence is a theorem in homotopy type theory:
funExt := ( f = g) ' ∏( f a =B a g a).
a:A

6

B

Shattered Lens

Encrypt-decrypt example

This example will be written in H ASKELL. Let us develop a stream cipher implementation. We will
represent encryption keys by an initial state of the random number generator.
newtype Key = Key (Maybe Gen)
The generator is wrapped in Maybe, because we want to represent a special zero key:
zeroKey :: Key
zeroKey = Key Nothing
The behavior is best explained by the encryption code. We have a function to generate random Word8(8-byte unsigned integer) from a Maybe Gen:
nextW8 :: Maybe Gen → (Word8, Maybe Gen)
nextW8 Nothing = (0, Nothing)nextW8 (Just g) = ...
where the Just branch uses the RNG g. Using nextW8; we can encrypt a plain text message:
encrypt :: Key → [Word8] → [Word8]
encrypt[]= []encrypt (Key g) (x : xs) = xor w x : encrypt (Key g0 ) xs where (w, g0 ) = nextW8 gBecause of the properties of xor we can use the same function to decrypt cipher text, in other words:
decrypt = encrypt. Next let us a define a data structure which carries a key with a cipher text encryptedwith that key.
data Bundled = Bundle Key [Word8]
We can bundle a plain text with the zeroKey:
plain :: [Word8] → Bundledplain = Bundle zeroKey
Now the key part. We construct the key lens using a lens constructor which takes getter and setter
functions. When setting a new key, we first decrypt the cipher text with an old key and then re-encryptwith the new one:key :: Lens Bundled Key
key = lens(λ (Bundle k ) → k)(λ (Bundle k x) k0 → Bundle k0 (encrypt k0 (decrypt k x)))And let us also have an ordinary projection lens for the cipher text part:
ciphertext :: Lens Bundled [Word8]
ciphertext = lens

Oleg Grenrus

7(λ (Bundle x) → x)
(λ (Bundle k ) x → Bundle k x)
If we not take msg = [108, 101, 110, 115] (which stands for "lens" in Latin1 encoding); then we canencrypt it using lens primitives as:
secret = view ciphertext (set key anotherKey (plain msg))
secret could then be e.g. [113, 107, 89, 46] standing for "qkY.". But we can also decrypt that message
using the same procedure!
msg0 = view ciphertext (set key zeroKey (Bundle anotherKey secret))
The result msg0 will be equal to the original msg!
Both lenses used here – key and ciphertext – are lawful, one can verify that using e.g. Q UICK C HECK
library [2], It will not find any counterexamples. We think this is a cool example usage of lens but it feels
morally wrong.