这篇文章介绍了将双向类型检查实现为光学（optic）的过程，使用 Haskell 的Control.Lens库。

• 双向类型化的 STLC：将语言的项分为可合成（synthesisable）和可检查（checkable）两类，在简单类型 lambda 演算（STLC）中，变量是可合成的，应用当函数部分可合成且参数部分可检查时是可合成的，抽象当参数部分可检查时是可检查的。用 Haskell 代码表示为data Type = TVar String | Unit | Function Type Type等数据类型。同时定义了双向类型化的规则，如(Var)规则用于合成变量的类型，(App)规则用于合成应用的类型等。
• 问题与答案：用边界由问题和答案组成的方式来安排双向类型检查为光学，问题有“这个可合成项的类型是什么？”和“这个可检查项有这个类型吗？”等，用Question和Answer数据类型表示。通过函数lam等实现了“问题-答案协议”，并引入了关于透镜类别的一些直觉，如透镜必须调用其延续一次等。
• 单子遍历（Monadic traversals）：(App)规则的类型签名需要一种类似单子（Monad）的超类，即app :: forall f. (Monad f) => (Question -> f Answer) -> Question -> f Answer，这种光学类没有名字，被建议称为“monadic traversal”，并推测其与一个具体的实现type MonadicTraversal s t a b = s -> Interaction a b t同构，Interaction a b t可以终止或继续询问问题。
• 整合在一起：给出了作为单子遍历的类型检查器的完整实现rules，通过无限复合stlc = rules. stlc来处理嵌套的子项，最后可以通过typecheck函数调用这个光学来进行类型检查，示例代码展示了在特定 lambda 项上的类型检查结果。
• 处理错误路径：理论上已完成，但实际中处理类型错误的方式很糟糕，一半的实现都在处理错误，且将所有错误合并为一个值。通过滥用 Haskell 的do-notation和MonadFail类来尝试修复第一个问题，最后提到处理错误的正确方式是定义TypeError类型并使用Control.Monad.Except.MonadError类的光学，但尚未实际构建。
• 管道（Pipelines）：最近 André 写了关于编译器管道的文章，而本文的无限复合光学在组成管道时存在问题，作者认为应该有某种（不对称）的单子积来正确地序列化这些光学，但尚未找到，最后展示了一个可能的但不太满意的将范围检查和类型检查的光学组合起来的方式pipeline。