|
| 1 | +# `Lens` vs `ALens`: a Note on Impredicativity |
| 2 | + |
| 3 | +Sometimes, you may encounter some strange errors to do with types that |
| 4 | +_should_ unify but don't. For example: |
| 5 | + |
| 6 | +```purescript |
| 7 | +newtype Wrapped = Wrapped String |
| 8 | +derive instance newtypeWrapped :: Newtype Wrapped _ |
| 9 | +
|
| 10 | +-- `_Newtype` is an `Iso'`, so we can specialise to `Lens'`. |
| 11 | +good :: Lens' Wrapped String |
| 12 | +good = _Newtype |
| 13 | +
|
| 14 | +-- So, we should be able to do the same when lifted into a record. |
| 15 | +type Example = { lens :: Iso' Wrapped String } |
| 16 | +
|
| 17 | +bad :: Example -> Lens' Wrapped String |
| 18 | +bad = _.lens |
| 19 | +
|
| 20 | +-- Could not match constrained type |
| 21 | +-- Profunctor t2 => t2 String String -> t2 Wrapped Wrapped |
| 22 | +-- with type |
| 23 | +-- p0 String String -> p0 Wrapped Wrapped |
| 24 | +``` |
| 25 | + |
| 26 | +Below, we'll discuss how these problems arise, and what we can do to overcome |
| 27 | +them. |
| 28 | + |
| 29 | +## The Long Answer |
| 30 | + |
| 31 | +The subtle issue here relates to a subject called *impredicativity*. We can make |
| 32 | +a smaller reproducible example: |
| 33 | + |
| 34 | +```purescript |
| 35 | +{ foo: id } :: { foo :: forall a. a -> a } |
| 36 | +``` |
| 37 | + |
| 38 | +We can, as we would expect, take `foo` out and cast it to whatever we like: |
| 39 | + |
| 40 | +```purescript |
| 41 | +({ foo: id } :: { foo :: forall a. a -> a }).foo |
| 42 | + :: String -> String |
| 43 | +``` |
| 44 | + |
| 45 | +So, while the original type said that we could pick _any_ `a`, we restricted that |
| 46 | +to `String` afterwards. In some situations, such as the above, the type-checker |
| 47 | +will cope happily. However, the troubles usually arrive when you extract a value |
| 48 | +with **a constraint**. Let's generalise the `id` function a little further: |
| 49 | + |
| 50 | +```purescript |
| 51 | +({ foo: id } :: { foo :: forall k a. Category k => k a a }).foo |
| 52 | + :: String -> String |
| 53 | +``` |
| 54 | + |
| 55 | +Now, we've generalised our `foo` to work with any `Category`, and not just |
| 56 | +`(->)`. However, we've also got ourselves a type error! _What did we do?_ |
| 57 | + |
| 58 | +Let's break this line down into two parts: |
| 59 | + |
| 60 | +1. We extract `foo` out of our record, which has the type signature: `forall k a. Category k => k a a`. |
| 61 | +2. We specialise `forall k a. Category k => k a a` to `String -> String`. |
| 62 | + |
| 63 | +Now, step `1` and `2`, independently, seem fine and dandy; they certainly work |
| 64 | +if we try it with a function _not_ wrapped in a record. The issue is with how |
| 65 | +these lines *interact*. We started with our record type, then extracted a value. |
| 66 | +At this point, the compiler has to hold onto its value, the `id` function, and |
| 67 | +its type, `forall k a. Category k => k a a`. At this point, we can |
| 68 | +observe something a bit weird: in this signature, the `a` type could correspond to our |
| 69 | +original record type! |
| 70 | + |
| 71 | +In fact, with this step, we've made a *more general* type signature, which is |
| 72 | +not something that the compiler wants to do. After all, if we keep getting more |
| 73 | +general, how will we ever solve the type equations? This situation, (where a |
| 74 | +type signature is general enough to contain the structure containing it), is |
| 75 | +called **impredicativity**. |
| 76 | + |
| 77 | +The next question is: why did `foo` work when we specialised it to `a -> a`? The |
| 78 | +answer to this is that the compiler actually can work certain situations out, |
| 79 | +but ends up struggling when we introduce *type constraints*. Why? Simply because |
| 80 | +the capability isn't in the compiler at the moment. While we _can_ talk about type |
| 81 | +variables, the fact is that this particular transformation would require us to be |
| 82 | +able to store constraints on the type variables, too. Not having an allowance for |
| 83 | +impredicative types will make very little difference to us in practice, but does |
| 84 | +mean that we might sometimes need to work around the issue. |
| 85 | + |
| 86 | +So... why does this matter to _lenses_? |
| 87 | + |
| 88 | +## Conclusion (The Short Answer) |
| 89 | + |
| 90 | +Well, let's take another look at that first failing example: |
| 91 | + |
| 92 | +```purescript |
| 93 | +newtype Wrapped = Wrapped String |
| 94 | +derive instance newtypeWrapped :: Newtype Wrapped _ |
| 95 | +
|
| 96 | +type Example = { lens :: Iso' Wrapped String } |
| 97 | +
|
| 98 | +bad :: Example -> Lens' Wrapped String |
| 99 | +bad = _.lens |
| 100 | +``` |
| 101 | + |
| 102 | +The optic types in this library are defined using various forms of the |
| 103 | +`Profunctor` constraint. That means that our example here will fail to pass |
| 104 | +type-checking, despite looking reasonable. To get around this, we just need to |
| 105 | +use a different form of the optic that doesn't have a visible constraint: |
| 106 | + |
| 107 | +```purescript |
| 108 | +type Example = { lens :: AnIso' Wrapped String } |
| 109 | +
|
| 110 | +bad :: Example -> Lens' Wrapped String |
| 111 | +bad = cloneLens <<< _.lens |
| 112 | +``` |
| 113 | + |
| 114 | +Here, instead of using `Iso'`, we use `AnIso'`. There's a difference in the type |
| 115 | +signatures: |
| 116 | + |
| 117 | +```purescript |
| 118 | +-- The main comparison |
| 119 | +type Iso' s a = Iso s s a a |
| 120 | +type AnIso' s a = Optic (Exchange a a) s s a a |
| 121 | +
|
| 122 | +-- For context |
| 123 | +type Optic :: (Type -> Type -> Type) -> Type -> Type -> Type -> Type -> Type |
| 124 | +type Optic p s t a b = p a b -> p s t |
| 125 | +
|
| 126 | +type Iso s t a b = forall p. Profunctor p => Optic p s t a b |
| 127 | +
|
| 128 | +data Exchange a b s t = Exchange (s -> a) (b -> t) |
| 129 | +``` |
| 130 | + |
| 131 | +What's the difference? Well, if you explore `Optic` and `Exchange`, you won't |
| 132 | +find any constraints! All we're doing here is side-stepping the impredicativity |
| 133 | +issue. Afterwards, we can use `cloneIso` to turn our `AnIso` back into the `Iso` |
| 134 | +that we've always wanted. |
| 135 | + |
| 136 | +In short, we used the optics prefixed with `A` or `An` to avoid impredicativity |
| 137 | +issues, and then `clone` those optics to recover the original lens. `Exchange` |
| 138 | +is a data type that characterises `Iso`, but there are similar types for all the |
| 139 | +favourites: |
| 140 | + |
| 141 | +| Profunctor Optic | Profunctor | `data` Optic | Inner Type | Recovery Function | |
| 142 | +| -- | -- | -- | -- | -- | |
| 143 | +| `Iso` | `Profunctor` | `AnIso` | `Exchange` | `cloneIso` | |
| 144 | +| `Lens` | `Strong` | `ALens` | `Shop` | `cloneLens` | |
| 145 | +| `IndexedLens` | `Strong` | `AnIndexedLens` | `Shop` | `cloneIndexedLens` | |
| 146 | +| `Prism` | `Choice` | `APrism` | `Market` | `clonePrism` | |
| 147 | +| `Grate` | `Closed` | `AGrate` | `Grating` | `cloneGrate` | |
| 148 | + |
| 149 | +So, when you run into a strange type error that doesn't look like a problem, |
| 150 | +consider impredicativity, and see whether one of the analogous optics and its |
| 151 | +recovery function solve the issue! |
0 commit comments