Edwin Brady - Idris 2 - Type-driven Development of Idris

Edwin Brady：Idris 2——Idris 的类型驱动开发 Edwin Brady 介绍了 Idris 2，这是用 Idris 语言自身对该语言进行的完全重写，旨在克服严重的类型检查器性能瓶颈。其核心架构突破是集成了定量类型论（QTT），该理论为变量分配了编译期使用数量（0 表示擦除、1 表示线性，以及不受限制）。Brady 展示了这些数量如何极大地增强交互式类型驱动编辑和自动化程序合成，如何通过 Chez Scheme 实现高效编译，以及如何实现精准的状态跟踪。最后，他展示了结合线性类型与依赖类型如何让开发者能够通过会话类型清晰地建模并验证通信系统。 Edwin Brady 宣布推出 Idris 2，这是用 Idris 语言本身完全重写的 Idris 编译器，旨在解决跟踪外部状态时遇到的严重类型检查器延迟问题。 (0:04) Idris 2 集成了 Conor McBride 和 Bob Atkey 的定量类型论（QTT），将所有变量绑定标记为运行时使用数量：0（擦除）、1（线性）或不受限制（ω）。 (2:55) 该编译器以 Chez Scheme 为目标代码，而不是像 Idris 1 那样生成 C 代码，从而充分利用了数十年的运行时优化，开箱即可提供更快的执行速度。 (24:45) 线性数量约束极大地缩小了自动化类型导向程序合成的搜索空间，从而防止搜索例程生成非终止循环。 (16:59)

Edwin Brady presents Idris 2, a rewrite of the Idris programming language implemented in Idris itself, designed around Quantitative Type Theory (QTT) to resolve compiler latency and support interactive development. Brady argues that integrating usage quantities provides compile-time erasure guarantees, guides automated program synthesis, and enables rigorous verification of stateful protocols. Compiler Latency and the Chez Scheme Backend (0:04) The primary motivation for rewriting Idris stemmed from severe performance bottlenecks in Idris 1, which emerged while using dependent types to track external state changes in concurrent and network systems. Brady undertook a ground-up reimplementation in Idris itself to test how dependent types could assist compiler construction while restoring sub-second type-checking speeds. To improve execution speed alongside type-checking latency, Idris 2 abandons the Idris 1 C-compilation pipeline in favor of emitting code for Chez Scheme. Drawing on decades of engineering and runtime optimization by Cisco, early benchmarks showed that code compiled to Chez Scheme ran faster than Idris 1 programs targeting C. Quantitative Type Theory and Guaranteed Runtime Erasure (2:55) Idris 2 is founded on Quantitative Type Theory (QTT), developed by Conor McBride and Bob Atkey, which assigns an execution multiplicity to every variable binding. QTT categorizes variables into three runtime quantities: 0 for compile-time arguments that are erased before runtime, 1 for linear values that must be consumed exactly once, and unrestricted usage (ω). In Idris 2, variables must be explicitly annotated if they are needed at runtime; otherwise, they default to erased status. Brady demonstrates this behavior with vector operations: when implementing matrix transposition, an erased dimension variable annotated with 0 cannot be inspected at runtime to initialize empty accumulators. This prevents compile-time proofs from unintentionally adding runtime overhead or leaking into executable artifacts. Guiding Interactive Synthesis with Linear Constraints (10:07) Brady positions type-driven development as an interactive dialogue between programmer and machine using a "Type, Define, Refine" cycle. Developers declare type signatures, inspect open holes in editor environments, and invoke automated proof search—drawing on Roy Dyckhoff's LJT algorithm as implemented in Haskell's Djinn—to synthesize structural boilerplate such as tuple unpacking and projection functions from type-level predicates. While implementing QTT, Brady observed that linearity directly aids program synthesis by pruning the search space. Because the interactive search engine lacks an integrated termination checker, unrestricted synthesis attempts can produce infinite recursion loops. Annotating inputs with quantity 1 prevents the synthesizer from erroneously reusing spent arguments, leaving only valid traversals when generating functions like map or vector transposition. Resource Tracking and Dependent Session Types (26:12) Linear quantities (quantity 1) enable fine-grained typestate tracking without specialized ad-hoc language extensions. In an embedded DSL modeling door state transitions, actions return linear handles alongside dependent results. Opening a door produces a boolean flag paired with a door handle whose typestate (open or closed) depends on that flag, while linearity forces the caller to cleanly dispose of the resource via dedicated cleanup steps across all execution branches. Brady extends this framework to concurrent communication, showing how global session types map directly onto dependent linear types. Channels track the protocol state: sending a boolean value updates the channel type to require either a character or a string in response. The compiler catches protocol deviations immediately, rejecting implementations that attempt to close channels prematurely or transmit mismatched data types across communication steps. Idris 2 is now public on GitHub with most Idris 1 features ported, though complete self-hosting remains blocked by minor language incompatibilities. Brady notes that QTT integration is still early; future priorities include polishing compiler error diagnostics, integrating termination checking into proof synthesis, expanding editor tooling, and formalizing custom tactics to automate sequential protocol steps.

Edwin Brady 介绍了正在用 Idris 自身重构的下一代依赖类型编程语言 Idris 2，该版本通过集成 Conor McBride 与 Bob Atkey 开创的数量类型论（Quantitative Type Theory, QTT）并以 Chez Scheme 作为代码生成后端，大幅提升了类型检查速度与交互式程序合成能力。 自举重写动机与编译性能跨越 (0:04) Edwin Brady 指出，重写 Idris 的核心动力源于几年前使用类型系统跟踪并发和网络协议外部状态时遭遇的类型检查性能瓶颈。为了彻底解决严重的时延问题并检验依赖类型在编译器开发中的实用性，他决定在 Idris 自身内部完全重新实现该系统。这一重写带来了显著的性能飞跃，使得频繁重检代码以享受流畅检查成为可能。 在代码生成与运行时方面，Idris 2 抛弃了 Idris 1 传统的 C 语言后端，转而以 Chez Scheme 作为执行后端。Brady 观察到，得益于思科团队对 Chez Scheme 长期数十年维护与运行时优化的积累，初步基准测试显示生成的 Scheme 代码性能超越了旧版基于 C 的实现。他认为利用成熟的底层运行时工程是语言设计者大幅提升执行效率的高效路径。 数量类型论：擦除、线性与合成约束 (2:55) Idris 2 的核心理论基础是数量类型论（QTT）。在该理论框架下，每个变量绑定都被标注了运行时使用次数（数量）：0 表示在运行时被彻底擦除，仅用于编译期推理与证明；1 表示线性变量，在运行时必须且仅能被消费一次，禁止复制或丢弃；ω 则对应传统的无限制使用。在类型检查与孔洞（hole）内联交互时，环境会显式标注这些数量，保证零数量参数不会向运行时引入任何开销。 除了传统的资源追踪与内存就地复用，Brady 意外发现线性类型能为基于类型的程序合成提供强力约束。在传统的交互式“类型-定义-精化”循环中，程序员使用快捷键触发程序搜索（基于 Roy Dyckhoff 的 LJT 算法），但由于缺乏终止检查器，搜索有时会产生死循环（如矩阵转置辅助函数）。当输入被标注为线性数量 1 时，候选解空间被大幅压缩，由于已消费的向量无法被二次使用，系统能够精准合成出正确的遍历代码（类似 zipWith 操作）。 资源协议状态机与会话类型验证 (26:12) 结合线性（数量 1）与依赖类型，Idris 2 能够自然支持细粒度的资源感知抽象与类型状态转换。Brady 通过门的状态模型（打开/关闭）展示了线性 IO 领域特定语言：当执行开门操作时，返回的是一个依赖对（Res），其内部包含一个布尔标志以及状态依赖于该标志的门句柄。在交互式分支展开中，如果开门失败，线性系统要求必须显式调用 deleteDoor 释放资源，阻止了句柄泄露或错误复用。在问答环节，Brady 进一步解释道，依赖对中各字段的线性特征由类型构造器显式标注的多元性决定。 利用相同的依赖线性框架，Idris 2 可以直接以全局会话类型（Session Types）来规范并发通信协议。以客户端与服务端交互为例，通道类型严谨跟踪通信阶段：客户端发送布尔值后，若为 True 则通道状态自动切换为期望接收字符，若为 False 则期望接收字符串。当 Brady 故意引入类型不匹配或在协议中单方面增加传输整型数据的需求时，编译器能够立即捕获操作顺序错位并拒绝编译，从而在语言内部原生表达并验证并发系统的协作逻辑。 人机对话模式与社区工程展望 (37:08) Brady 强调，面向类型的开发本质上应当是程序员与机器之间的实时对话，而不是将编译器视为对抗性的阻碍。在 Idris 2 中，这一交互编辑闭环通过孔洞检查、变量按用例拆分（case split）以及基于作用域信息的自动证明搜索来实现。他认为编程的过程不仅仅是得到最终代码，未来理想的开发环境应该允许开发者抽象高频重复的合成模式，甚至能让系统智能识别出通用模式并提出重构建议。 目前 Idris 2 的代码库已在 GitHub 上公开发布，其大部分 Idris 1 的语言结构均已移植，但距离完全自举（Self-hosting）仍有少许不兼容细节需要攻克。Brady 坦承 QTT 的实现仍处于早期阶段，编译器诊断信息与错误定位尚待打磨，他呼吁社区积极参与包管理器构建、编辑器插件改进（如 Vim 插件）以及库生态的丰富，共同推进高效交互式依赖类型编程工具的落地。 Idris 2 表明，将依赖类型与数量类型论结合不仅解决了长期困扰依赖类型系统的运行时开销与协议状态验证难题，更在程序合成中发挥了收窄搜索空间的意外价值；但其证明搜索目前仍缺乏终止性检查器，且在自举完成度、错误诊断直观性及高级搜索策略的语言表达能力上仍有待进一步完善。

## Background 该视频由 Curry On! 频道于 2019 年 7 月 18 日发布在 YouTube 平台上。视频记录了 Edwin Brady 的主题演讲，主要展示新一代依赖类型编程语言 Idris 2 的设计理念、自举实现与核心特性（页面未提供额外的描述文本）。 ## TL;DR Edwin Brady 介绍了采用 Idris 自身进行自举重写的全新语言实现 Idris 2，着重展示了类型检查性能的大幅跃升与交互式开发体验。语言的核心理论革新在于引入了量化类型理论（QTT），通过 0（编译期擦除）、1（严格线性使用）和任意数量的精确约束，辅助系统完成自动程序搜索并避免非法逻辑。此外，Brady 通过经典的矩阵转置、门协议状态机以及会话类型并发通信示例，论证了依赖线性类型在资源跟踪和协议正确性保障上的强大能力，并号召开源社区共同完善生态工具链。 ## Atmosphere & style 整场演讲充满了典型的英式幽默与轻松随和的技术极客氛围，Brady 以生动的“魔术揭秘”比喻和自嘲（例如调侃终端报错提示、Linux 键盘按键与看板球分心）让高深的类型理论变得平易近人。现场人机交互式的现场编码充满悬念与惊喜，当快捷键卡顿或故意触发类型报错时，台下笑声不断，而当类型推导瞬间填补正确实现时又令人拍案叫绝。整个过程既是一场严谨的语言理论展示，又洋溢着创造者摆脱缓慢类型检查后纯粹、真挚的技术喜悦。 ## Bulletin - [00:04](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=4s) Edwin Brady 正式发布并开源了使用 Idris 自身进行自举重写的 Idris 2，类型检查速度取得突破性提升，极大改善了依赖类型编程的反馈延迟。 - [02:54](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=174s) Idris 2 在核心理论上引入量化类型理论（QTT），通过 0（编译期擦除）、1（严格线性使用）和 Many（无限制）三档数量标记，兼顾静态证明与运行时资源精确管理。 - [17:46](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=1066s) 通过引入线性约束，Idris 2 大幅缩小了代码搜索空间，不仅使自动程序合成能精准生成唯一实现，还自然支持了强类型约束的会话类型与通信协议验证。 - [22:33](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=1353s) Idris 2 目前采用开源的 Chez Scheme 作为代码生成后端，初步基准测试显示其执行速度甚至超过了基于 C 语言后端的 Idris 1。 ## Key takeaways - [00:04](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=4s) 用语言本身自举重写不仅验证了依赖类型在大型编译器工程中的实用价值，也彻底解决了 Idris 1 随着系统复杂度上升而导致的类型检查迟缓问题。 - [02:54](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=174s) 类型驱动开发（Type-driven Development）强调人机交互式协同，系统不再是开发者的“对手”，而是通过类型信息引导程序逐步成型的辅助工具。 - [02:54](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=174s) 量化类型理论（QTT）将变量分级为 0（仅编译期擦除）、1（线性资源）和 Many（常规使用），构成了 Idris 2 的核心语言语义基础。 - [13:46](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=826s) 数量标注为 0 的参数会在运行时被彻底抹除，编译器会静态拦截任何对擦除参数进行模式匹配的尝试，从而消除运行时代价。 - [10:07](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=607s) 基于类型的程序合成借鉴了 Djinn 工具与 Dyckhoff 证明搜索算法，其背后的“魔术”完全取决于程序员在类型签名中提供的约束信息量。 - [17:46](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=1066s) 线性类型（数量为 1）要求变量必须且仅被消耗一次，这不仅能防止数据别名和跟踪外部协议，还通过剪枝状态空间反向提升了类型定向代码合成的精准度。 - [17:46](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=1066s) 在矩阵转置示例中，由于默认隐式参数列数 n 的数量为 0，程序无法在运行时读取其数值，这暴露了纯类型期数据与运行时展开之间的显式边界。 - [20:34](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=1234s) Idris 2 要求开发者显式写出运行时所需的数据，若缺少数量约束或终止性检查，盲目的自动化生成可能会陷入非终止的递归死循环。 - [22:33](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=1353s) Chez Scheme 后端为 Idris 2 带来了惊人的执行效率，在数项基准测试中表现直接超越了 Idris 1 的 C 语言生成代码。 - [26:12](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=1572s) 通过“门协议”状态机演示，QTT 的线性类型能够严格在编译期追踪外部世界的不确定状态转移，并强制开发者安全释放未销毁的资源。 - [31:51](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=1911s) 利用依赖线性类型可以非常自然地编码会话类型（Session Types），信道状态随交互自动演化，无需额外引入专门的通信协议外挂系统。 - [34:56](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=2096s) 当客户端或服务器违反通信协议（如提早关闭信道或类型不匹配）时，类型系统会在编译期直接拦截，杜绝了并发网络通信中的协议不一致问题。 - [37:08](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=2228s) Idris 2 目前已实现一代的大部分语言特性，未来将重点优化交互式响应速度，并号召社区参与包管理、编辑器生态与错误提示信息的优化建设。 - [39:27](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=2367s) 在依赖对偶（Dependent Pair）等数据类型中，每个字段都可以独立标注多重度，从而灵活实现部分分量非线性、部分分量严格受控的管理模式。 ## Detailed walkthrough ### [00:04](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=4s) 重写 Idris 的缘起与目标 Edwin Brady 以幽默的开场向观众打招呼，调侃自己最近在 PowerPoint 技能上下足了功夫。他将这次演讲定义为一次“成果展示（show-and-tell）”，分享自己过去几个月“躲在小隔间里”全力开发的新一代语言实现——Idris 2。在现场举手表决确认多数听众对依赖类型编程（dependently typed programming）有一定了解后，Brady 阐述了他启动该项目的核心动力。几年前，他致力于利用类型来追踪程序状态以及外部世界的变更，这在并发编程和网络协议中尤为重要。然而随着系统变得复杂，类型检查器的耗时越来越长，迟缓的反馈令人抓狂。“And it's kind of whose fault is that then so so ok maybe I should step back and think about re-engineering this if I'm going to re-engineer it maybe I should try re-engineering it in itself and see if I can learn a bit about where the type system is going to help me away,” Edwin Brady 解释道。他决定用 Idris 本身来自举重写 Idris，探索类型系统在重构过程中能给予开发者的支持。 这次重写带来了显著的性能提升。Brady 兴奋地表示，类型检查速度取得了巨大的突破，以至于他常常“仅仅为了享受在合理时间内看到代码完成类型检查的快乐”而反复进行类型检查。除了速度，他强调 Idris 2 还致力于优化交互式编辑体验、引入量化类型理论（Quantitative Type Theory, QTT），并在此基础上实现基于会话类型（session types）的安全并发通信。该项目已在演讲前约一周于 GitHub 正式开源，Brady 欢迎社区积极参与贡献并提交反馈。 - **自举实现**：Idris 2 采用 Idris 自身进行编写，以验证依赖类型在大型工程和编译器实现中的实用价值。 - **开源进展**：项目在演进过程中经历了多次底层架构调整，在确认核心设计稳定后正式向公众开放仓库。 --- ### [02:54](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=174s) 交互式开发哲学与量化类型理论（QTT） ```mermaid flowchart TD accTitle: Idris 2 核心设计理念与数量维度 accDescr: 展示 Idris 交互式开发循环以及 QTT 中 0、1、许多 三种数量标记的语义 subgraph Interaction["类型驱动开发循环 (Type-Driven Development)"] A["给出类型 (Type)"] --> B["生成定义与待填孔 (Define & Holes)"] B --> C["精化实现与类型 (Refine)"] end subgraph QTT["量化类型理论 (QTT Quantities)"] Q0["数量 0: 仅编译期可用 (运行时完全擦除)"] Q1["数量 1: 严格线性使用一次"] QMany["数量 任意 (Many): 经典模式 (无使用次数限制)"] end Interaction --> QTT ``` Brady 指出，类型驱动开发（Type-driven Development）的灵魂在于“交互式编辑”，即程序员与机器之间展开持续的双向对话。在许多人初学生涩复杂的类型系统时，往往容易产生系统在与自己对抗的错觉。“It's too easy when when you're writing a program in a language with a more complicated type system it's it's quite easy to get into this feeling that the machine is your adversary your enemy,” Edwin Brady 说道。人们常常抱怨“Idris 讨厌我”或者“编译器在对我吼叫”，但他希望通过 Idris 2 转变这种认知：类型系统是在努力协助开发者，二者应该是一种协同探索的关系。 Idris 2 最核心的语言理论革新是采用了由 Conor McBride 和 Bob Atkey 在过去几年中提出的量化类型理论（Quantitative Type Theory, QTT）。在 QTT 中，每一个变量和参数都会附带一个使用数量（quantity）的标注。系统中存在三个关键的数量界限： 1. **0**：表示该实体仅存在于编译期，类型检查器会静态保证它在运行时被彻底擦除（erased）。 2. **1**：表示该资源是线性的，在运行时必须且仅能被精确使用一次。 3. **Many（任意）**：即传统编程语言的语义，对运行时的引用和使用次数不做限制。 Brady 提到，将线性资源意识（linearity）与依赖类型结合后，开发者能够以非常优雅的方式构建诸如会话类型（session types）系统，从而用类型严格刻画并发通信系统的状态转换。 --- ### [05:49](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=349s) 向量拼接示例与交互式程序搜索 按照依赖类型编程演讲的“行业惯例”，Brady 现场演示了经典的定长向量（`Vect`）拼接函数 `append` 的编写过程。虽然听众对这个例子极为熟悉，但他强调这次演示展示了 QTT 带来的全新细节。在 `append` 的类型签名中，输入分别为长度为 `n` 和 `m` 的向量，返回长度为 `n + m` 的向量。类型中隐含的类型变量 `a` 以及长度变量 `n`、`m` 是隐式参数（implicit arguments），它们的存在是为了辅助类型系统的规约。 遵循“给出类型、添加定义、逐步精化（Type, Define, Refine）”的开发范式，Brady 利用编辑器的交互菜单在声明下方生成了一个带有待填占位符（hole）的候选定义。通过检查该洞的局部上下文，编辑器展示了当前作用域内的所有变量及其类型。与 Idris 1 截然不同的是，在 `m`、`a` 和 `n` 的名字旁边赫然标注着神秘的数字“0”。这明确向开发者证明：虽然编译期可以任意利用这些参数推导维度与类型，但在运行时它们将被完全抹除，绝不产生开销。 随后，Brady 演示了依赖类型交互的核心步骤：首先对输入的向量变量执行“情况拆分（case split）”，自动将结构解构为“空向量”与“非空向量（Cons）”两组分支；接着在各个分支的孔上触发自动程序搜索（通过快捷键 `Ctrl-Alt-S`）。依赖丰富的类型约束，机器迅速且精准地推导并填补了合法的实现代码。在演示过程中，Brady 也展现了幽默松弛的讲台风格：先是吐槽右键菜单字体太小导致后排看不清，接着在快捷键失效时自嘲“我忘了先保存文件，我就知道会这样”。 在完成逐步推导后，Brady 引导听众思考更高层面的元编程问题：刚才的推导本质上是“拆分分支、执行搜索、若不行再继续拆分”的机械循环。既然开发者在编写重复的业务逻辑时会将其抽象为通用函数，“Wouldn't it be nice if we get abstract away in the acts of programming so if we could just say you know keep case splitting and searching until you find an answer,” Edwin Brady 总结道。他指出，交互式工具应当走得更远，将这种编码过程本身的套路沉淀为自动化的交互指令。 ### [10:07](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=607s) 类型驱动编辑与程序搜索的“魔术” Edwin Brady 解释了编辑器中的自动代码补全与搜索功能（例如通过快捷键直接完成推导）背后的本质。他打了个生动的比方：这就像看纸牌魔术，“当你看到魔术时觉得不可思议，但当魔术师揭秘手法后，你就会想‘我也能做到’”。在类型驱动开发中，系统之所以能自动补全看似神奇的代码，纯粹是因为程序员在类型签名中提供了额外的信息。当前系统中这种“拆分并搜索（split and search）”的机制虽然还是硬编码的，但他未来的愿景是让用户能够自行编写针对代码片段的抽象生成逻辑。 ```mermaid flowchart LR accTitle: Type Directed Search Flow accDescr: 描述类型信息如何引导程序自动推导出具体实现的流程图 subgraph Input ["输入规格"] T["丰富精确的类型签名"] end subgraph Engine ["证明搜索引擎"] D["Dyckhoff 算法 / 结构拆分"] end subgraph Output ["代码生成"] C["唯一/确定性的函数实现"] end T --> Engine Engine --> Output ``` 针对有人担心这种自动化工具会取代程序员的言论，Edwin Brady 予以了反驳。他指出程序员仍然必须清楚自己在做什么、想写出什么程序，并对自动搜索在何时能奏效保持直觉。他展示了几个从元组中解构并重组数据的“管道连接（plumbing）”示例，这些例子借鉴自 Haskell 的 Djinn 工具（该工具利用 Roy Dyckhoff 的直觉主义命题逻辑证明搜索算法从类型中提取代码）。在演示过程中，Edwin Brady 还因按错快捷键幽默地解释道，自己刚从 Mac 换到了 Linux 笔记本上，因为他听说“明年就是 Linux 桌面元年”，所以对键盘按键还不习惯。 随后，他又展示了一个异构列表（heterogeneous list）的示例。列表每个元素都有自己的类型，且这些类型被编码在异构列表的整体类型定义中。如果我们已经费心写出了一个类型谓词，断言列表中特定位置存在特定类型的值，那么提取该值的代码就不该再由人工手写。对此，Edwin Brady 总结道：“I shouldn't have to write that program again so I go to the machine and I say I've done it once you finish it so off you go.” 他打趣承认这些演示例子确实经过了挑选，其中一个甚至是他前一天在酒吧看板球比赛分心时想出来的，当时前三次类型都写错了导致搜索失败，直到类型完全准确，程序才瞬间自动生成。 - 交互快捷键如 `Ctrl-G` 触发了基于类型的隐式证明搜索与代码填充。 - 自动化代码合成的核心逻辑借鉴了 Haskell 社区著名的 Djinn 工具，其底层是 Roy Dyckhoff 的证明搜索算法。 - 异构列表的演示表明，只要前置的不变量谓词定义足够严密，提取元素的逻辑完全可以交给系统自动补全。 --- ### [13:46](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=826s) 数量类型论与线性类型（QTT）的引入 在展示完编辑辅助之后，Edwin Brady 转入了 Idris 2 最核心的新特性——引入 Conor McBride 与 Bob Atkey 关于数量类型论（Quantitative Type Theory, QTT）的研究成果。他坦言自己多年来一直渴望在语言中加入这一机制，但由于缺乏类型论底层的理论推演能力，直到 Conor McBride 和 Bob Atkey 形式化了这套理论并发表论文后，他才得以将其工程化落地。这套机制在直觉上与 GHC 的 Linear Haskell 非常相似：当一个函数在参数类型前标明其数量为 1 时，意味着如果该函数调用的结果被恰好使用了一次，那么该输入参数也必须且只能被精确使用一次。 为了展示线性限制的效果，Edwin Brady 演示了一个构造数对的函数。如果参数没有任何数量约束，系统可以轻松将单个值 `x` 复制两次生成 `(x, x)`；但一旦为参数加上线性标记（数量为 1），自动生成就会报错失败。他在交互环境中拆解了原因：当尝试在数对的第一项使用 `x` 之后，查看未完成的右侧类型洞（hole），会发现上下文中的 `x` 的可用数量已经归零。Edwin Brady 将这种现象形象地描述为：“I see that I have no xs so I can't use x anymore I've spent it I can talk about it it's available I can reason about it as much as I like but I can't have it in the program.” 试图再次使用 `x` 就会引发编译错误，警告线性变量被重复使用。 ```mermaid flowchart TD accTitle: Quantitative Type Theory Usages accDescr: 展示数量类型论中数量0、数量1和无限制数量的三种用法 subgraph Quantities ["QTT 变量数量分级"] Q0["数量 0 (Erased)"] Q1["数量 1 (Linear)"] QW["无限制 (Unrestricted)"] end Q0 -->|"类型检查与编译期证明"| E["运行时擦除，严禁模式匹配解构"] Q1 -->|"资源跟踪 / 原地复用"| L["精确使用一次，防止数据别名"] QW -->|"常规函数式编程"| U["可任意丢弃或复制多次"] ``` 在演示编译器报错时，终端中弹出了 Idris 2 自带的一句欢快提示语“Enjoying yourself?”，惹得全场大笑。Edwin Brady 苦笑着表示，在用户程序报错时嘲讽用户“玩得开心吗”，迟早会把人惹毛，之后得改成说句“Sorry”或者提供点实际帮助。随后他澄清，线性检查只关心变量在整个程序中被消耗的总次数，与代码中的左右求值顺序无关。此外，数量为 0 的标记则用于显式声明那些仅在编译期供类型检查和形式化证明使用、而在运行时必须被完全擦除（erased）的变量。如果尝试对数量为 0 的参数进行模式匹配提取，编译器会明确拦截并报错“attempt to match on erased argument”。 - 数量 1（线性）确保变量不被复制也不被随意丢弃，适用于协议状态跟踪、资源管理以及避免非法别名。 - 数量 0 确保参数仅作为编译期命题和不变量证明存在，不会为生产二进制文件带来运行时代价与内存开销。 - 编译器的线性检查分析整段代码对变量的消耗总和，不受语法层面的从左到右求值顺序影响。 --- ### [17:46](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=1066s) 线性约束对程序合成的助推与矩阵转置的困境 除了众所周知的资源跟踪（防止违背通信协议）与性能优化（由于没有别名引用，可以直接在原内存空间复用更新数据）之外，Edwin Brady 分享了一个意料之外的新发现：线性类型能够显著提升基于类型的代码自动合成能力。在常规类型下，由于可能存在任意丢弃或多次复用参数的路径，搜索空间极大；但如果给高阶函数（如 `map`）的列表参数施加“恰好消耗一次”的线性约束，能够合法消费整个列表且类型匹配的实现往往只剩下唯一的标准解。Edwin Brady 指出：“kind of by accident I discovered that the linearity gives more information to the type directed synthesis.” 为了说明这套数量系统如何在实际编码中发挥约束与指引作用，他开始现场演示一个经典的依赖类型范式案例——矩阵转置（Matrix Transpose）。矩阵被定义为嵌套向量 `Vect m (Vect n a)`，转置的目标是将其转换为 `Vect n (Vect m a)`。在通常的开发流程中，直接构思完整的转置实现需要较强的技巧，因此在类型驱动方法下，首先采用模式匹配将矩阵拆解为空矩阵与非空行向量组合。 ```mermaid flowchart TD accTitle: Matrix Transpose Base Case Issue accDescr: 矩阵转置在处理空矩阵基准情况时因列数参数在运行时被擦除而导致的停滞 M["输入矩阵: Vect 0 (Vect n a)"] --> T["转置目标: Vect n (Vect 0 a)"] T --> E["需要调用 empties 生成 n 个空向量"] E --> F{"检查维度变量 n"} F -->|"n 的数量为 0 (Erased)"| ERR["编译错误: 运行时无法读取 n 的值，无法展开循环"] ``` 当处理外层行数为 0 的基准情况（即处理空矩阵）时，Edwin Brady 将右侧表达式提取为一个独立的子目标函数 `empties`，该函数的目标是构造出包含 $n$ 个空向量的外层向量。然而，当他在编辑器中按下 `Ctrl-Alt-L` 生成辅助函数的类型签名时，立刻暴露出一个隐蔽的问题：矩阵的列数变量 $n$ 在原始类型签名中属于隐式参数，其默认数量为 0（即在运行时被擦除）。这就意味着，程序在编译期知道有 $n$ 列，但在生成可执行代码的运行时阶段，根本没有 $n$ 的具体数值可供读取，因此不可能在运行时根据 $n$ 循环展开生成包含 $n$ 个空向量的结构。依赖类型驱动的编辑环境在此刻精准地捕捉到了运行期数据与纯类型期信息之间的矛盾。 - 线性类型的额外约束削减了状态空间的冗余分支，使得类型定向自动合成能够直接推导出唯一的合法逻辑。 - 矩阵转置的类型签名为 `Vect m (Vect n a) -> Vect n (Vect m a)`，其基础情况需要根据列数 $n$ 生成 $n$ 个长度为 0 的空向量。 - 由于隐式维度变量 $n$ 的数量属性默认为 0，运行时无法获知其具体数值，直接导致基准情况下的辅助函数因“缺少运行时数据”而无法通过类型检查。 ### [20:34](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=1234s) 运行时可用性与矩阵转置的递归挑战 在 Idris 1 到 Idris 2 的迁移过程中，存在一处略显恼人的不兼容变更：如果开发者希望某个变量在运行时可用，就必须显式将其写进类型定义中。Edwin Brady 总结道：“基本上经验法则是：如果你把它写下来，它就会出现在你的程序里；如果你不写，它就不在。”如果想完全明确，开发者可以显式标注数量（Quantity）。例如，将辅助函数 `empties` 提升（lift out）后，系统看到类型中明确包含了 `m`，便知道可以在运行时依据 `m` 生成内容，并顺畅地自动生成所需实现。 真正更有趣的挑战出现在处理向量其余部分的转置逻辑上。转置的核心思路是：先对子向量 `xs` 进行递归转置，然后将另一个向量“旋转”拼接上去，即把第一个向量的对应元素通过 `cons` 挂到转置后的第二个向量前。通常的切入点是直接发起递归调用，也就是引入归纳假设（inductive hypothesis）。然而，当 Brady 让机器自动为此生成类型并尝试自动填补时，程序给出了看似合理的输出，但实际上这并非正确解答。由于类型驱动的程序搜索（type-directed program search）中当时尚未加入终止性检查（termination checker），生成的代码并不能终止运行。 Brady 借此提醒大家：“你不能只是盲目地按按钮，指望最终生成的程序就一定是对的。我们必须对正在做的事情稍加思考。”问题在于，开发者给辅助函数 `transpose_helper` 提供了过多无关信息。为了让机器真正帮上忙，人类必须向机器进一步阐明意图。 - Idris 1 与 Idris 2 在变量可见性上的差异：Idris 2 要求在类型签名中显式写出运行时需要的量（数量级标注）。 - 盲目依赖自动化生成可能产生无法终止的递归死循环，必须由程序员介入约束。 ### [22:33](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=1353s) 利用精确数量约束代码生成与 Chez Scheme 性能惊喜 为了纠正死循环，Brady 撤销了代码并审视 `transpose_helper` 的上下文类型。他指出，开发者掌握着一条尚未告诉机器的关键事实：当转置一个矩阵或向量时，那个待处理的矩阵究竟会被使用几次？答案是“恰好一次”（exactly once）。如果在类型中明确限定该向量的使用数量为 1，机器在推导时就不会把已经消耗掉的向量再次错误传递给辅助函数。加入这一数量信息后，自动化代码生成终于生成了正确且终止的实现。 Brady 幽默地承认，台下观众心中可能在狂喊“这不就是 `zipWith` 吗！”。它确实本质上就是某种特化的 `zipWith`。他畅想道，在系统的理想未来版本中，或许会像经典的 Office 助手 Clippy 一样弹出来提醒：“看起来你又在重新实现 `zipWith` 了，需要我帮你重构吗？” 随后 Brady 现场演示了该程序的执行。Idris 2 可以将代码编译为可执行文件，而当前它是通过 Chez Scheme 后端来生成的。Chez Scheme 是 Cisco 近年开源的一款积累了 30 多年研发底蕴的 Scheme 实现。Brady 惊叹其运行速度快得惊人：“事实证明，Chez Scheme 速度快得不可思议：在哪怕只是从源码生成的版本上，针对我尝试的一小组基准测试，它的运行速度都比走 C 语言后端的 Idris 1 还要快。”他感叹道，编写运行时系统如果有 30 年的深厚功底确实非同凡响，非常期待懂运行时优化的专家能参与到 Idris 编译器的优化中来。 ```mermaid flowchart TD accTitle: 线性数量约束对代码生成的剪枝 accDescr: 展示当输入无数量限制导致死循环，与引入使用一次约束后成功生成的逻辑流 subgraph Unconstrained ["无数量约束 (默认)"] U1["输入向量/矩阵 xs"] --> U2["程序搜索尝试匹配"] U2 --> U3["重复传递已使用的变量"] U3 --> U4["生成非终止代码 (死循环)"] end subgraph LinearConstraint ["线性约束 (Quantity = 1)"] L1["限定矩阵仅使用一次 (1)"] --> L2["程序搜索进行资源剪枝"] L2 --> L3["禁止将已消耗资源传给辅助函数"] L3 --> L4["成功合成正确的类 zipWith 转置"] end ``` ### [26:12](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=1572s) 基于定量类型论的资源跟踪与门协议交互演示 演讲的最后十几分钟聚焦于 QTT（定量类型论，Quantitative Type Theory）最具吸引力的应用场景之一：资源跟踪（Resource Tracking）。在复杂的类型系统中编写操作外部状态的程序时，如果必须将整个程序写完才能看编译器是否通过，过程会极其痛苦；但如果能通过人机交互逐个“洞”（holes）推进，系统会友好得多。Brady 介绍了一个线性的嵌入式 DSL（类似线性 IO Monad 的结构），用于在类型层面描述资源的创建与销毁。 为直观演示，Brady 引入了经典的“门协议”（Door Protocol）。在这个协议中，门有开启和关闭两种状态，可执行的操作包括敲门、开门与关门。但开门操作的特殊之处在于：现实世界并非完全受程序控制，尝试开门并不保证一定成功，系统必须将实际结果返回给程序。在类型层面上，标注为 `1` 的程序代表产生一个恰好使用一次的资源，标注为 `any` 的程序则代表产物可被使用任意次。 - `1`：表示线性资源，必须被精确消耗/使用一次，不可丢弃也不可重复使用。 - `any`：表示普通数据，可无限制使用或随时丢弃。 - 外部世界的不确定性：像开门操作这类具有不确定结果的行为，需通过依值配对返回状态。 ### [28:08](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=1688s) 交互式孔洞驱动开发与依值结果模式匹配 Brady 现场在编辑器中逐步构建该协议的实现。首先创建一个新门 `d`，在交互式洞中检查当前拥有的资源：拥有类型维度的变量 `m`，以及一个当前处于关闭状态且数量恰好为 1 的门。接着他对门执行敲门操作 `knock d`，并将新结果绑定为 `d'`。此时上下文中 `d` 变成了历史遗留资源，而当前可用的则是 `d'`。正如 Brady 所形容的：“`d` 依然是一个关着的门，但它是我们在过去拥有的关着的门；`d'` 则是我们现在拥有的关着的门。我们不能再对 `d` 进行任何操作了，但我们依然可以谈论它，谈论我们在敲门之前那扇门的辉煌历史。” 随后尝试执行开门操作 `openDoor d'`。查看该操作返回的结果，它是一个特殊的依值对（dependent pair，显示为红色类型）：第一项是布尔值操作结果（开门是否成功），第二项则是根据该结果计算出状态的门资源。在编译期我们只能抽象表达这种依赖关系，在运行期才会真正确定其真伪。 通过对该依值结果进行模式匹配拆解出 `(x, y)`，再对布尔值 `x` 做情况分支（case split）： 1. **成功分支（`x = True`）**：门成功变为打开状态（Open），程序可以合法继续推进门开启后的协议； 2. **失败分支（`x = False`）**：门依然是关闭状态（Closed）。 如果此时程序希望在此结束，由于线性资源 `y`（门）的数量被强制限定为 1，必须将其显式消费掉（例如调用注销/删除门的清理函数），编译器才会通过检查。Brady 顺畅完成删除操作，类型检查成功通过，完美展现了借助线性类型系统在编译期强约束资源状态机流转的全过程。最后他提到，剩余的几分钟将用来展示更为高级的并发编程与会话类型（Session Types）示例。 ### [31:51](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=1911s) 基于会话类型与线性类型的通信协议编码 Edwin Brady 展示了本场演讲的最后一个示例：如何在 Idris 2 中使用会话类型（Session Types）来编码通信协议。他首先说明自己不会展开所有底层实现细节，而是给观众一个直观的“风味体验”。在该协议中，他通过一种全局会话类型来描述通信行为：客户端首先向服务器发送一个布尔值（`Bool`）；如果该布尔值为 `True`，服务器将向客户端返回一个字符（`Char`）；如果该布尔值为 `False`，服务器则返回一个字符串（`String`）。Edwin 指出，依托于 Idris 强大的全功能依赖类型系统，开发者无需发明特殊的通信协议原语，“基本上除了时序控制（sequencing）或者时序加依赖（sequencing and dependency）之外，我们不需要做任何额外的事情；任何形式的分支选择，我们都能直接使用 Idris 自身的语言操作符来编码。” 在演示客户端代码时，Edwin 将已写好的实现注释掉，转而使用编辑器进行交互式类型检查（通过留出类型洞 hole）。信道（Channel）本身具有类型，随着交互的进行，信道的状态与类型会随之演变。当客户端向信道发送了一个 `False` 后，再次检查类型洞的类型，编译器明确指出：“下一步你必须在这个信道上接收一个字符串”，这完全契合了协议规范。如果刚才发送的是 `True`，系统给出的下一步期望就会立刻变成接收一个字符。Edwin 感慨，交互式编辑的精髓在于不是一次性写完整个程序，而是“一步一步地查看下一步我们究竟需要做什么”。他还设想，若未来结合“可编程的程序搜索（programmable program search）”，这种方式将极具价值：在同时处理多个通信协议或外部资源的复杂场景中，开发者可以编写专用的策略（tactics），让工具自动完成协议规定的下一个操作步骤，不过目前这套策略语言仍在构想之中。 ```mermaid flowchart TD accTitle: Protocol Type Evolution accDescr: Global session type branching based on boolean request Start["Client sends Bool"] --> Cond{"Bool Value?"} Cond -->|"True"| ExpectChar["Server sends Char<br/>Client must receive Char"] Cond -->|"False"| ExpectStr["Server sends String<br/>Client must receive String"] ``` - **协议分支逻辑**：发送 `True` $\to$ 期望接收 `Char`；发送 `False` $\to$ 期望接收 `String`。 - **状态追踪**：线性信道在每一步操作后消耗旧信道并产生新信道，类型系统强制下一步操作严格匹配协议分支。 ### [34:56](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=2096s) 协议违规与协议变更触发的类型错误 为了验证这套静态约束不是摆设，Edwin 故意在代码中引入两类错误进行测试。第一类错误是客户端违背协议约定：向信道发送了 `True`，却试图通过字符串拼接操作（`string append`）将接收到的数据当作字符串处理。编译检查执行后立即报错，检测到 `Char` 与 `String` 之间发生类型不匹配。Edwin 舒了一口气打趣道：“谢天谢地报错了，如果这都能通过类型检查，那关于这个系统的一切就全是在骗人了。”不过他也坦承，当前的错误信息看起来还有些粗糙丑陋，编译器定位的是捕获到类型冲突的那个表达式位置，若有社区贡献者能来对错误提示进行润色和优化，将会带来巨大的体验提升。 第二类错误则是模拟实际开发中的协议变更。Edwin 开玩笑假设这个协议已经是一个“价值百万美元的商业项目”，此时客户突然提出变更需求：在发送字符串之后，必须再返回一个整数（`Int`）。Edwin 在全局协议定义中增加了这个整数返回项，但服务器端代码尚未更新。重新检查时，编译器立刻精准报错：类型不匹配，提示服务器本应继续发送数据，但当前代码却直接关闭了信道（`close`）。Edwin 总结道，依赖线性类型（Dependent Linear Types）使表达会话类型成为了一种极其自然的能力，不需要任何外挂系统即可获得严密的通信正确性保障。 - “If this type checks and everything about this is a lie.”（Edwin Brady 调侃道，如果违规代码通过了检查，那他今天讲的就全成了谎言） - **类型系统捕获违规**：静态杜绝了通道未完成传输便提前关闭（提前终止协议）或类型解读错误（如把字符当字符串拼接）的问题。 ### [37:08](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=2228s) Idris 2 现状总结、未来路线与社区号召 Edwin 切换到了总结环节（他笑称这是自己的“总结幻灯片”，尽管其实是在编辑器里打开的文件）。他表示 Idris 2 的进展非常喜人，自己写得非常开心，“老实说，光是不必干等着类型检查器出结果这一点，就让我感到其乐无穷了。”目前 Idris 1 的大部分语言特性都已在 Idris 2 中实现，但由于存在少数底层不兼容的改动，目前还不能一键切换实现完全自举（self-hosting），还需要多走一步，但这一步非常值得。 对于量化类型论（QTT），Edwin 坦言自己也才刚刚开始摸索，“基本上你们在这场演讲中看到的，就是我目前做过的 QTT 的全部内容了。”未来在探索类型系统的表达能力上有非常广阔的空间。此外，交互式编辑需要进一步优化执行效率，他希望交互式模式能够成为大家使用 Idris 2 的默认工作流，这就要求系统响应必须极快。最后，Edwin 向社区发出了协助邀请，无论是编写更多生态库、打造包管理器（package management tools）、改善编辑器支持（他悄悄提到自己其实偏好 Vim 而非 Atom，并笑着向在场的 Emacs 用户道歉），还是美化错误信息与实现 Tab 键补全，都非常需要贡献。所有参与指导都已写在 GitHub 仓库的 `CONTRIBUTING.md` 中。 - **自举状态**：已高度接近自举，但由于少许破坏性变更，仍需进一步适配才能完全替代 Idris 1。 - **核心诉求**：极速响应的交互式编辑体验、完善的生态工具链（包管理、编辑器插件）。 - “I think interesting is making some good progress, I'm certainly having loads of fun with it. I'm just having loads of fun not waiting for the result of the type checker quite honestly.”（Edwin Brady 谈及 Idris 2 的开发体验与相比一代巨大的性能飞跃） ### [39:27](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=2367s) 问答环节：依赖对偶中的线性多态性 演讲结束后进入现场提问。一位听众起立感谢了 Edwin 一如既往幽默精彩的演讲，并针对前文关于“门（Door）”状态机的示例提出了一个具体疑问：在表示门及其状态的依赖对偶（Dependent Pair）`(x: Type ** y)` 中，为什么 `y` 是线性的（受到消耗限制），而 `x` 却不是线性的？听众表示没完全想通背后的机制是如何运作的。 Edwin 揭晓了谜底：这是因为在该类型本身的定义中，就显式声明了这种不对称性。在依赖对偶的类型定义里，第一个分量的计数被赋予了非线性（例如 $0$ 或无限制使用），而第二个分量的多重度被显式定义为线性（恰好消耗一次）。Edwin 笑着自嘲道：“答案就这么简单，可能有点令人失望。我本来还挺想给出一个听起来更神奇、更高大上的答案呢，但事实确实就是如此。”随后全场爆发出热烈的掌声，演讲圆满结束。 - “That's because I didn't show you the definition of that type and it's because I say in the type first thing is not linear but the second thing is.”（Edwin Brady 回答为什么依赖对偶中一个分量线性而另一个不线性） - **类型定义的显式性**：在量化类型论中，数据类型的每一个字段都可以独立标注其多重度（Multiplicity），从而灵活控制哪部分数据参与运行时计算、哪部分数据作为线性资源受限管理。 ## Notable quotes > [20:34](https://www.youtube.com/watch?v=DRq2NgeFcO0&t=1234s) 你不能只是盲目地按按钮，指望最终生成的程序就一定是对的。我们必须对正在做的事情稍加思考。 — Edwin Brady ## Mentioned Edwin Brady, Idris, Idris 2, Conor McBride, Bob Atkey, Chez Scheme, Cisco, Roy Dyckhoff, Djinn, Linear Haskell, GHC, Atom, Emacs, Vim, GitHub [Source](https://www.youtube.com/watch?v=DRq2NgeFcO0)

[20:34] Edwin Brady: 你不能只是盲目地按按钮，指望最终生成的程序就一定是对的。我们必须对正在做的事情稍加思考。

[2:55] Edwin Brady: I don't want you to think Idris is shouting at you, Idris is trying to help you, it's trying to be in a conversation with you [10:07] Edwin Brady: I sort of feel like if we go to the trouble of expressing a predicate that says that a value at a particular location is a particular type, surely we've done enough work to write the program that pulls that value out of the list.

[0:04] I've been working very hard on my [0:07] PowerPoint skills recently this is a [0:10] this is a kind of a show-and-tell [0:11] session so I've been I've been hiding [0:16] away in my cupboard over the last few [0:19] months working on a new implementation [0:22] of address and I just want to show show [0:26] you where it is [0:26] so just now curiosity has anyone played [0:29] with any dependently type of programming [0:32] languages before just by way of show of [0:34] hands okay that's that's great because I [0:36] mean I asked this question often and [0:39] it's nice to see bigger proportions of [0:41] hands going up over time so that's [0:43] that's marvelous I'm not going to ask [0:44] you how you know experience you are [0:45] anything I'm just going to assume lis [0:47] you've seen the basics before and I'm [0:50] going to show you how the new version of [0:52] Idris does some of those basics and some [0:55] of the new things that can do and why [0:57] I've done in the first place so there's [1:02] a few things I want to do in this talk [1:03] one what's the answer to point one are [1:08] we ok if I read it as it's kind of good [1:12] hands are going up at the back so if [1:14] hands didn't go up it says check whether [1:16] this font size is big enough so well [1:18] right so as an important question of why [1:21] did I what are they I even start doing [1:23] this so so a couple of years ago doing [1:27] new things with Idris I was working on [1:29] one of my interests is in kind of [1:31] tracking state in types tracking [1:33] tracking how the state of the outside [1:35] world changes and getting the type [1:37] system to help you get it right so this [1:39] is particularly interesting when it [1:40] comes to say concurrent programming or [1:42] network protocol programming so you want [1:44] to get these things right and I was [1:45] thinking well how how can i how can I [1:47] use the type system to write these [1:49] programs and be confident that they work [1:51] but I was increasingly getting to a [1:52] point where the type checker was taking [1:54] too long and it was getting frustrating [1:57] and it's kind of whose fault is that [1:59] then so so ok maybe I should step back [2:03] and think about re-engineering this if [2:05] I'm going to re-engineer it maybe I [2:08] should try re-engineering it in itself [2:10] and see if I can learn a bit about where [2:13] the type system is going to help me [2:14] away so I'm not gonna I'm not today [2:17] you're going to say too much about where [2:18] the type system has helped me in the [2:20] implementation of interest to itself [2:22] that's a talk for another time [2:24] I might allude to it from time to time [2:25] mostly I want to show you the results of [2:27] this of this work so what we played a [2:32] little bit about the progress we've got [2:33] so far and what's coming up so firstly [2:36] definitely faster type checking I'm [2:39] going to point at the minute where I've [2:40] just made it a kind of a big a big [2:42] improvement in the speed I'm retype [2:44] checking things just for the joy of [2:46] seeing things type check in reasonable [2:48] time to marvelous I don't get out much [2:51] you know so them so I'm gonna show you a [2:55] bit about the new interactive additive [2:56] feature so one of the key things about [2:57] interest and time driven development and [2:59] I don't think when people start playing [3:02] with with certainly with Idris I don't [3:05] think this really comes across enough [3:06] but it's all about the interactive [3:08] editing it's all about the condo that [3:11] the machine and the program of being in [3:14] a conversation so it's it's it's too [3:16] easy when when you're writing a program [3:18] in a language with a more complicated [3:20] type system it's it's quite easy to get [3:22] into this feeling that the machine is [3:24] your adversary your enemy and you know [3:26] people come on the mailing list or the [3:28] IRC Channel and they use phrases like or [3:30] interest hates me because or Idris is [3:32] shouting at me because I don't want you [3:34] to think interest is chatting me are you [3:35] interest is trying to help you it's [3:37] trying to be in a conversation with you [3:38] and I think we need to one thing we need [3:40] to do is work quite a lot harder at [3:41] making that either way people interact [3:43] with the system so that's something I'm [3:45] trying to do with this new version as [3:46] well well maybe see a little bit of of [3:49] that as we go as well and the the the [3:53] key new feature of the language though [3:55] is that it's based on quantitative type [3:59] theory so quantitative type theory is a [4:03] new core language that's been developed [4:05] over the last couple years by economic [4:08] brides and bob ascii and the idea with [4:13] quantitative type theory is that every [4:15] there [4:16] is annotated with how many of it there [4:19] are essentially ask some of the [4:20] intuition behind this and there are [4:22] three interesting numbers 0 1 and [4:26] everything else so 0 means this is going [4:30] to be a race at runtime and the type [4:32] checker has told me that it's going to [4:33] be raised at runtime 1 means I can use [4:35] this exactly once at runtime and many is [4:38] just back in the old world where we [4:39] always used to be we can have lots of [4:41] these things that were a runtime and [4:44] then we'll see examples of where that [4:45] goes hopefully I'll have enough time to [4:47] get to my favorite thing that I like to [4:50] try with with new are these new resource [4:53] aware types is can i implement session [4:58] types so that are inspired by koreander [5:01] and many others by now the system for [5:03] describing the types of concurrent [5:05] communicating systems turns out if you [5:07] have linearity and dependent types you [5:10] absolutely can do that and I think I [5:13] think it's quite a nice way of writing [5:15] concurrent programs so also please [5:17] contribute go to github it's it's I only [5:21] made it public about a week ago the [5:23] reason I held off I know some people [5:25] have been saying when are you gonna let [5:26] me have a go with this I I've changed it [5:30] too many times and I was slightly scared [5:32] that I would completely change my mind [5:36] about the implementation of some core [5:38] detail after someone it's been ages [5:40] working on something related to it I'm [5:41] confident that's not going to happen [5:42] there so so please come along I'd love [5:46] to have your funky issues right so this [5:49] isn't dependent type stock so by law I [5:51] have to show you the vexes there's a [5:55] reason I'm going to show you the vectors [5:56] I'm sure some of you have just died [5:58] inside because you've seen these [5:59] thousand times [6:00] there is a reason I'm going to show you [6:02] the vectors I'm going to show you [6:03] something slightly new about the way [6:06] vector programs work so anyone not seen [6:09] this before a couple of hands have gone [6:12] up ok so hopefully hopefully what I'm [6:15] about to show you will be enough ask me [6:18] afterwards if you want a bit more detail [6:21] basic idea is the lengths are encoded in [6:23] the type [6:24] so if if I'm writing an append function [6:27] and I say the effector has n things and [6:30] another vector has n things then the [6:32] resulting vector has n plus M States now [6:34] questions sometimes people ask is if [6:36] they haven't seen this before is what [6:37] are these n a and and you know where are [6:39] they found so these are these are [6:42] implicitly bound in the type these are [6:44] implicit arguments so they are going to [6:47] be arguments to the append function just [6:50] like any other argument but there's a [6:52] bit special about them because they're [6:53] only there because we wanted them in the [6:55] time so this is why this program and [6:58] I'll show you a bit more about what that [6:59] means so the type of the development way [7:02] is you give a type you've asked the [7:06] Machine things about your type it will [7:07] give you a bit more of your program so [7:09] they type define refine so come with the [7:11] type come up with a definition and then [7:13] then refine the definition and the type [7:15] as we learn more about the problem so in [7:17] this case I'm gonna I'm gonna try that [7:19] stat menu is too small isn't it but [7:22] sometimes I get feedback that says I [7:25] can't see what you're doing when you use [7:26] the keyboard so please could you use the [7:29] context menu I don't think you can see [7:31] what I'm doing when I use the context [7:32] menu either as you can see when I'm [7:34] doing it so this says add definition [7:37] that's okay so that's out of a candidate [7:39] definition for a parent and this thing [7:41] on the right this is a hole so this is [7:43] what I really want people to be in this [7:44] is the way I want people to be [7:45] interacting with the system is adding a [7:47] candidate definition seeing the poll [7:49] working with the hole so if I check the [7:51] type of that hole we'll see what we have [7:54] in scope and what we what we need to [7:57] produce so oh this is no that's [8:00] hopefully that's legible so what do we [8:03] have in scope we have our ma and n we [8:05] have our vector axes and we have our [8:06] vector wise but we have these mysterious [8:08] zeros next to ma and n so these zeros [8:12] these are the quantities so these say [8:15] you can talk about MA and then as much [8:17] as you like a compile time but there [8:19] will be zero of them at runtime but [8:21] guaranteed these are erased guaranteed [8:23] that the type system ensures that they [8:26] won't appear in our program okay so next [8:29] step is we'll ask the machine to case [8:36] splits on one of these variables that [8:38] gives us the two possible cases and I've [8:42] seen this before that if you've got it [8:44] if you've got a bit more information in [8:45] the type that means the machine can help [8:47] you out a bit more and you know maybe [8:50] search for a program based on what's in [8:51] scope so I'll do that again if I hit [8:53] control old s for search there then then [8:58] it doesn't work because I didn't save it [9:01] and I knew that would happen so let's [9:03] try that again so control elapsed with [9:06] the search for possible implementations [9:08] of this program and then ctrl s again in [9:10] the other case this is the first program [9:12] it finds that matches that type so so [9:14] far so much what you've seen before with [9:16] a dependently type language so I thought [9:18] well Oh sometimes people ask in fact [9:21] you've done you've done a few things [9:23] they're kind of repeatedly the same [9:25] thing as almost a pattern to what you're [9:27] doing [9:27] you're almost brute-force case splits [9:30] search see what happens case split a bit [9:33] more so to see what happens and why [9:36] don't you ask the machine to do those [9:37] steps for you there's a process we're [9:39] following and somehow the act of [9:41] programming is not just about the end [9:44] result it's sort of what we do to get [9:46] there and and which we kind of know that [9:49] when we write programs and we do we have [9:51] programs that are repetitive so we have [9:55] weekly repeated patterns in the code [9:56] itself we abstract it away so wouldn't [9:59] it be nice if we get abstract away in [10:01] the acts of programming so if we could [10:04] just say you know keep case splitting [10:06] and searching until you find an answer [10:07] and hilariously that works quite well so [10:10] ctrl G is just do that so save the zip [10:13] with just you know go save it save the [10:16] zip with just just do that and all its [10:19] doing literally all it's doing is like [10:21] you know when you see a card trick [10:23] and it looks amazing and then they tell [10:25] you how it's done and you think yeah I [10:27] could do that literally all that's [10:29] happened this is just a magic trick but [10:31] the cool thing is just because we've [10:34] given that little extra bit of [10:35] information in the tie we can do that [10:37] magic trick and we can sort of what I [10:39] really want to be able to is hard-coded [10:40] this into the system the sort of split [10:43] and search thing what I really want is [10:46] for you to be able to write your own [10:48] abstractions over the bits of program [10:50] that you would have written and see what [10:52] comes out but just it's good to have a [10:55] flavor to sort of a bit of a feel for [10:57] the kinds of things that search can do [11:00] sometimes I see people comment that oh [11:02] no you're taking my job away as a [11:04] programmer well no you still have to [11:06] know what you're doing you still have to [11:08] know the program's you want to write and [11:09] it's still good to have a feel for when [11:12] it's going to work so this is I guess [11:16] kind of when you're doing kind of [11:19] plumbing you're taking bits out of pairs [11:21] and putting them into new pairs so so [11:25] these examples I've got up here that at [11:27] the top these are sort of manipulating [11:29] pairs so they're examples taken out of [11:30] the gym documentation so you know the [11:32] gym tool for Haskell so this is a tool [11:34] that uses Reuter coves proof search [11:37] algorithm to extract programs from types [11:39] and pleasingly this sort of thing [11:43] oops if I hit there we go if I hit the [11:45] right key it health this is the new [11:47] laptop I said I've got used to where all [11:48] the keys are this is a because I've [11:51] moved from Mac to Linux because I heard [11:56] that next year is the era of Linux on [11:57] the desktop so so I'm not entirely used [12:02] to where all the keys are anyway so [12:03] these ones all all work quite nicely so [12:06] kind of pulling things out of pairs [12:08] another sort of place which comes up in [12:10] practice is if you have one data [12:13] structure related to another data [12:14] structure you might have some invariants [12:16] that you express in the type so here [12:18] I've got this is a heterogeneous list [12:21] I'm not going to go through exactly the [12:22] details of how this works except to say [12:24] that every element has a type and we [12:27] encode the types of the elements in the [12:30] type of the heterogeneous list so I sort [12:33] of feel like if we go to the trouble of [12:35] expressing a predicate that says that a [12:38] value at a particular location is a [12:40] particular type surely we've done enough [12:43] work to write the program that pulls [12:45] that value out of the list [12:47] I shouldn't have to write that program [12:48] again so I go to the machine and I say [12:51] I've done it once you finish it so off [12:54] you go so that's a kind of feel for [12:58] kind of places where it works so if [13:00] you're thinking oh yeah you just [13:02] carefully picked them because you knew [13:04] that they would work well guilty this [13:08] one I actually came up with this one in [13:09] a pub yesterday watching the crickets [13:11] and I was a little bit distracted and I [13:14] got it wrong about three times but every [13:15] time it said known it was only when I [13:17] got the typewriter that said yes here's [13:18] the program so that's kind of fun okay [13:22] again this is you know I freaking done [13:24] MIT this but I find it weirdly pleasing [13:26] just to generate programs as well I'm [13:28] procrastinating okay so that's the the [13:34] type given editing is something I want [13:36] to make a big thing and I want it to be [13:38] programmable here it's hard coded it's [13:40] hard coded in terms of some primitives [13:41] that have been glued together but turns [13:44] out you need quite a lot with it already [13:46] now here's the really interesting thing [13:49] I think about the new thing about the [13:52] language and this is where grown very [13:54] heavily on Colin McBride and Bob [13:56] Mackey's work and I'm so glad they did [13:57] this because I've wanted this for ages [13:59] but I don't have the skills to figure [14:00] out that the type theory details myself [14:03] so so well so Bob Connor did this [14:06] they're these lovely platers honest I've [14:08] tried to implement it to see what we can [14:09] do in practice so also if you don't know [14:12] if you've seen any of the linear Haskell [14:14] work I don't know if anyone's Lots at [14:15] that it's it's a similar kind of idea so [14:17] similar kind of intuition that so the [14:21] intuition that I highlighting that [14:23] doesn't really help but if if you have a [14:25] function a function of X and you say in [14:28] the type that there is one of X then the [14:30] intuition is going to be that if f of X [14:32] is used once exactly once then you know [14:35] X is used exactly once but essentially [14:37] it means it's a thing you can use once [14:39] so let's say we're trying to build a [14:41] pair of things so we're trying to build [14:44] a pair of things from from a thing so [14:47] for X in a we can always build a pair of [14:49] A's because you know parity there's only [14:52] one thing it could possibly be so that's [14:55] let's search and we get that but I'm [14:58] using X twice so if I were to say [15:01] something like okay I'm only going to [15:03] use X once then well it's fire writing [15:06] that if I try to generate it you get I [15:09] haven't figured out in ass [15:11] how to make this font size adjustable [15:14] but it basically says it went wrong so [15:16] they can't find a definition for this [15:19] function let's let's dig a bit deeper as [15:21] to why they is so try adding a [15:24] definition and I'll look at the type of [15:26] pair RHS likes to call this DUP but I [15:33] don't like having DUP around so I call [15:35] it pair name so I only have one X and I [15:44] need to produce two A's so sure I could [15:48] use one X so let's use one X and if I [15:54] check the type of this pair RHS now then [15:58] I see that I have no access so I can't [16:00] use X anymore I've spent it I can talk [16:03] about it it's available I can reason [16:05] about it as much as I like but I can't [16:07] have it in the program and if I I guess [16:10] it's probably better to show this [16:11] somewhere where the font is big enough [16:14] what I call a cute et tu idea it says [16:17] there are two uses of linear named X [16:19] just occurred to me this morning when I [16:21] was working through this I put this [16:23] jaunty little message enjoying yourself [16:25] and it's just told you that your [16:26] programs wrong and I'm thinking that [16:28] might [16:29] that might start to annoy me so I'd like [16:33] to quit sorry or something you know [16:34] anything I can do to help I don't know [16:36] whatever right so sometimes it again [16:41] people sometimes ask what happens if I [16:43] put X second just so just to show you [16:45] just to save you ask it if you put X [16:48] second you can still use X and you can't [16:50] use X here so so there's no there's no [16:52] left-to-right ordering or anything here [16:54] it's really about it being used in the [16:55] whole program so we can't we can't [16:59] finish that [16:59] another thing we can't do like we we [17:01] might want to express that something is [17:03] only something we want to talk about [17:04] something we don't want to use so [17:07] typical place where there where you [17:08] might want to do that is is if you have [17:10] proofs so you don't want your proofs [17:14] hanging around at runtime but you do [17:15] want them at compile time because [17:16] they're telling you interesting things [17:17] about your program this is a very [17:19] trivial example there's not actually a [17:21] proof but let's say I'm trying to invert [17:23] this B well I'm not going to be able to [17:25] do that because I said I can't have a [17:28] match on it so it does actually let me [17:31] do the K split which it shouldn't but if [17:33] I if I try loading it again it says [17:37] attempt to match on e raised argument so [17:38] I can't I can't inspect anything that is [17:41] zero quantity so I'll get rid of that [17:44] because it's in the way and finally [17:47] something that I sort of discovered by [17:49] accident so when you when you see people [17:51] talk about linear types often the things [17:53] they cite is the value of the linear [17:54] types is either resource tracking so we [17:56] can show that a protocol is being [17:58] followed and you're not referring to old [17:59] old things you know aliasing when you [18:01] shouldn't that sort of thing um also for [18:03] performance reasons you might want to [18:05] use the linearity to say well I don't [18:07] need to allocate memory here I can just [18:09] reuse the thing I spent both of these [18:10] things are really cool but kind of by [18:12] accident I discovered that the linearity [18:14] gives more information to the type [18:16] prototype directed synthesis so here [18:19] I've got a map function while I'm [18:22] consuming the list exactly once so that [18:25] turns out to be enough to find the [18:29] definition because there's only one way [18:31] of consuming that list exactly once in [18:34] order to build this progress all that [18:35] was it a cool little side effect of this [18:38] thing yes question yes [18:43] that's a fantastic question I'll show [18:45] you how to it doesn't work it's [18:48] fantastic question but I better move on [18:49] so I'd love to talk to you about this I [18:51] know you have interesting things to say [18:53] though this so right let me show you an [18:57] example that in practice again this is [18:59] an example you may have seen before [19:00] I'm going to use it again because the [19:02] quantities turn out to give us new [19:04] things to say about writing transpose on [19:07] vectors so what matrices rather so if [19:10] I've got an N by n matrix I want to get [19:13] back in n by n matrix and we're just [19:15] going to work through that with the [19:16] types and see what the type of an [19:18] approach can do so usual thing I'll add [19:22] a candidate definition there's not a lot [19:28] I can do that kind of a fourth choice [19:30] that I don't know unless I happen to [19:32] know how to write this program already [19:34] like it's basically as if we're the cons [19:36] but let's assume we don't know how to [19:38] write this program already we'll work [19:40] through it and see what to see what to [19:42] do next [19:42] the only thing we can really do is is [19:46] pattern match on the matrix so we'll do [19:49] that [19:50] what I like to do if I've got something [19:52] that's starting to look a little bit [19:53] complicated is just rename the hole and [19:57] then I hit ctrl alt L and it gives me [20:00] the type of the thing that will [20:02] implement this program where when I get [20:06] round to it and we're going to see [20:08] fairly quickly that we have a problem [20:10] so I'm going to try writing empties so [20:13] empties is going to produce us n copies [20:17] of an empty vector but if I look at the [20:19] ty see that I'm not allowed to have em [20:23] at runtime so it is it's a zero quantity [20:26] at runtime so there's no way I'm going [20:29] to be able to produce n copies of the [20:30] empty vector because M is not available [20:32] to me at runtime so the thing we have to [20:34] do is so this is this is where address [20:37] one and a versa to have a slightly [20:39] annoying incompatibility is if I want [20:42] this to be available at runtime I have [20:44] to write it explicitly as part of the [20:47] type so the rule of well the rule of [20:52] thumb [20:52] basically if you write it down it's in [20:54] your program [20:55] you don't write it down it's not if you [20:57] want to be completely explicit about it [20:58] you can give the quantity explicitly so [21:01] now if I if I lift out empties it says [21:04] okay M is available so I know can [21:06] generate things from M at runtime and [21:08] pleasingly generate it for me [21:11] so a more interesting case is [21:15] transposing the rest of the vector so [21:17] the way I to think about this is we can [21:20] transpose X is recursively and then [21:22] somehow we have to rotate the other [21:24] vector kind of rotate it onto the top so [21:27] it kind of cons the the corresponding [21:29] elements of our first vector onto the [21:32] transposed second vector so a good place [21:36] to start is by making a recursive call [21:38] so invoking the inductive hypothesis so [21:43] and I'll do the same thing as before [21:45] I'll I'll call this it's a bit [21:48] complicated so I'll ask the machine to [21:51] generate me the type for this thing and [21:54] lift it no but let's just do this and [21:56] see what happens then you'll think [22:00] that's the right answer I'll tell you [22:04] now it's not the right answer [22:05] this doesn't actually terminate I [22:07] haven't put a termination chapter in the [22:09] time directed program search yet so I [22:12] like to show this just because like you [22:15] can't just blindly press buttons and [22:18] hope that the program comes out is going [22:19] to be the right program we have to think [22:20] a little bit about what we're doing and [22:22] what happened here is we've kind of [22:24] given transpose help with too much [22:26] information we in order for the machine [22:28] to help us we have to tell the Machine a [22:30] little bit more about what we mean so [22:33] I'm going to undo this I'm going to show [22:35] you the type of transpose helper in this [22:38] context so so it says says what we've [22:41] got a lot of we got we've got we've got [22:45] our axes we've got I found supposed X's [22:47] we've got our X that we want the glue on [22:48] the front now because I've done this [22:50] before I happen to know that there is a [22:52] piece of information that we have we [22:54] know that we haven't told the machine so [22:57] the question is if you're transposing a [23:00] vector or supposing a matrix how many [23:02] times are we going to use that matrix [23:05] exactly once so [23:08] maybe if we tell it that we're going to [23:10] use the matrix exactly once maybe then [23:12] that will help us a bit more so you know [23:13] it can it can only help us if we if we [23:16] give it a bit more information [23:18] so let's lips they put the page up key [23:25] or I expect it to be a left arrow which [23:27] is kind of kind of awkward okay so if we [23:30] lift it out now this is not quite [23:31] visible so let's just let's just [23:34] generate it so pressing the wrong button [23:39] again finally so if we give it that [23:46] extra little bit of information that [23:48] let's make that visible on the screen [23:50] that the vector is only going to be used [23:52] once then it's not going to pass that [23:54] vector that we've already spent to the [23:57] transpose helper function so it can help [23:59] us out a little bit more so by the way [24:05] there's a step that we haven't done here [24:08] and probably a lot of you are screaming [24:11] inside it's just zip we've come on it's [24:15] just zip with yes it is just it's a kind [24:17] of instance of zip with something so in [24:20] my dreams in the dream version of this [24:22] system you'll sort of get to the end of [24:25] this and the machine will say you know [24:27] clicky will pop up and say it looks like [24:30] you're implementing zip with again [24:32] would you like me to refactor that for [24:34] you I think that'll be a very nice thing [24:36] to have an out I think you know so a [24:38] feasible thing to believe that we could [24:40] do one day well but it today is not that [24:43] day [24:45] okay I'm gonna show you any programs [24:47] running yes let's let's at least run [24:48] this one it's got a main program that [24:53] generator a vector and I do cool on exec [25:02] I give it just to just to show that it [25:05] type checks so we can ship it it's we've [25:08] got a couple of vectors and then we've [25:09] got a transpose both of those vectors [25:10] and I guess is worth throwing in at this [25:12] point that we can generate and [25:17] executable I suppose as things stand the [25:22] executable it generated in scheme so [25:25] yeah so this is running via a shape [25:28] scheme so a che scheme something that's [25:32] been developed over 30 over decades it [25:34] at Cisco recently open sourced and I [25:36] thought okay that would be a good scope [25:37] stopgap it turns out that show scheme is [25:42] astonishingly fast so even from source [25:45] the shape scheme generated version for [25:48] the small set of benchmarks I've tries [25:50] has run faster than the idris one which [25:52] goes by a siege so I guess spending [25:55] thirty years of knowing what you're [25:57] doing is quite good if you're writing a [25:59] runtime system so so it'd be interesting [26:01] to see what could happen if someone who [26:03] knows how to write a runtime system [26:05] could get their hands on on the address [26:07] compiler I'd love for that to happen [26:09] [Applause] [26:11] okay [26:12] so the other interesting things only [26:13] about 10 to 15 minutes left and the [26:16] thing I really wanted to get to was [26:17] resource tracking I think that's one of [26:20] the cool things you can do with [26:23] quantitative type theory and it's [26:26] something where it really pays to have [26:28] interactive editing so if you're trying [26:29] to write a program which does [26:31] complicated things in the type system [26:34] and you have to get the whole program [26:36] right before the compiler will accept it [26:38] that can get quite frustrating but if [26:40] you can do it step by step and having a [26:42] machine tell you what you need to do [26:43] next [26:43] I think that [26:44] be a lot more helpful so without going [26:47] into all of the details about how this [26:48] works I'm just gonna give like kind of [26:52] its gonna give an overview of what [26:54] happened what happens there's a I guess [26:58] you'd call it a linear linear IO monad [27:01] or something like that it's not really [27:03] more mad but a linear embedded dsl that [27:07] allows us to describe when we create and [27:10] destroy resources so my favorite way of [27:12] illustrating this is where the protocol [27:15] for describing the movements of a door [27:17] where the ridore is open or not there [27:19] are two things we can do in this [27:21] protocol we can open the door we can [27:23] close the door [27:23] but if we open the door the door might [27:26] not open so we're not always in complete [27:28] control of what happens in the outside [27:31] world so it might be that we say open [27:35] the door but the Machine tells us [27:36] whether opening that will actually [27:37] succeed it so let's see how this works [27:38] so just to read these types so one is a [27:45] program in this linearity monad that [27:48] produces a thing that's just used once [27:49] any is a program that produces a thing [27:52] that can be used any number of times and [27:54] there's a little bit of type level [27:56] jiggery-pokery to feed this together [27:58] again that's a talk for another day how [28:00] this works but let's just let's just see [28:03] what happens so if I start writing a [28:08] program in this linearity let's create a [28:11] new door so D is a new door and we'll [28:15] check what we have so in every stage [28:16] we'll check what we have and what we [28:18] need so what we have so we haven't we [28:22] have an M that's just in type world we [28:24] have a door that's currently closed and [28:26] we have exactly one of it so what could [28:30] we do with the door that closed we could [28:33] we could knock on this so D prime is [28:37] knock D I'm gonna call it D prime [28:39] because we're then we can see everything [28:40] that we have so so D is still a closed [28:45] door but it's a closed door that we had [28:48] in the past D prime is the closed door [28:50] that we have now so we can't work with [28:54] you anymore [28:54] we can still talk about it we can still [28:56] talk about the [28:57] glorious history of how the door was [28:59] before we knocked on it but we can't [29:01] have that door as before we knocked on [29:04] it more interestingly we could try [29:06] opening a door so that the type of open [29:09] door is this thing I'm not going to tell [29:12] you what this thing is because I'm going [29:13] to show you interactively what this is [29:14] we're going to learn interactively by [29:15] talking to the Machine what this is so [29:17] result is open door on d-prime and let's [29:23] have a let's have a look at that it's [29:26] it's it's some red thing so red it's [29:29] kind of a dependent parrot the first [29:31] thing is a result and the second thing [29:33] is a resource with a type computed from [29:36] that result so this is going to be given [29:39] the result it's going to be a door [29:40] that's either open or closed depending [29:43] on what this boolean actually is at [29:45] runtime so what we're going to do is [29:46] talk about what this is at compile time [29:48] but a runtime will actually find out [29:50] what it is so the easiest way to find [29:52] out what you know what this is Beit of [29:54] is to kind of do it I didn't spell that [29:59] right but I'm going to pattern match on [30:00] anyway [30:00] so if I pattern match on the result of [30:03] this we've got an X out why what are X [30:07] out why again we do we just look at the [30:10] holes to find out what we've got and it [30:12] says we've we've got a few things we've [30:15] spent but the things that we've got are [30:16] the X which is the result of the [30:18] operation let's make that all visible [30:19] and the Y which is a door that depending [30:23] on X it's going to be either open or [30:25] closed so that's K split on X if I case [30:31] split on X then that's either true or [30:33] false so so this is the this is the case [30:40] where there's a door prog RHS 2 so in [30:44] this case X was true so the door is open [30:46] so now we can we can carry on working [30:48] with the door and carrying on with the [30:49] protocol and in the second case the door [30:51] was door opening did not succeed so if I [30:55] check the type of RHS 3 it says in this [30:58] case Y is a closed door so and the only [31:01] way I'm going to be able to complete [31:02] writing this program is if I you know [31:05] finish up and delete the door so what [31:08] while something if I have something with [31:10] a quantity one in the type I have to [31:13] spend it before before before I'm [31:17] allowed to continue so so I have to make [31:20] sure that that this Y has been consumed [31:22] and I can consume it by deleting the [31:26] door hopefully I'll type check it did [31:29] good so that's the basic idea of [31:32] encoding protocols using linearity and [31:34] it looks like to have about five minutes [31:36] which means I can show you the [31:39] concurrent programming example so kind [31:42] of a basic version of session types [31:46] encoded using this this kind of language [31:48] so what have we got I'll just show that [31:51] the way I encode the protocols again I'm [31:54] not going to show you all the details [31:55] just let this be a flavor of what you [31:57] can do so a protocol I describe a [32:01] protocol with sort of global session [32:03] type so a global description of the [32:05] protocol so this says in the protocol [32:07] there will be a request to a server that [32:11] is a type bool and then the rest of the [32:14] protocol says well if that boolean is [32:15] true then the server will send me back a [32:17] character if that boolean is false then [32:20] the server will send me back a string so [32:23] what's quite fun about this is because [32:24] we have the full extent of the language [32:27] we don't need to do any anything beyond [32:30] essentially sequencing or sequencing and [32:32] dependency so any kind of choice we can [32:34] include we can encode using the address [32:37] language operators so either client for [32:41] this protocol but completed the client [32:43] here but what I'm gonna do is I'll just [32:46] um I'll comment it out I'll point out [32:49] most of this will so all I'm doing is [32:54] you know sending a couple of messages I [32:56] did the sleep just to convince myself [32:57] that it was working so you actually need [33:00] that sleep so so so let's check don't [33:13] need to do I can do it I can do it in [33:15] the editor right so says I have a [33:18] channel [33:19] and the channel has a tie and the [33:21] interesting thing to look at the most [33:23] important thing to look at is what is [33:25] the first thing we do on the channel so [33:27] the first thing we're going to do on [33:28] this channel is send the boolean so we [33:33] do this check the type of our whole [33:37] again it says right the next thing you [33:40] have to do on this channel is send a [33:42] string and the reason we have to send a [33:44] string is because the boolean was false [33:46] and that's what that's what the protocol [33:48] says are sort of demeaning we have to [33:49] receive a string or what I expect to [33:51] receive the string at the kids that was [33:52] false if that was a true then as one [33:56] would hope the next thing we're going to [33:58] receive is a character the typeset side [34:00] so we're using that that's where you [34:03] think this interactive editing to say [34:05] not to write the whole program at once [34:06] but to say step by step what did what is [34:11] it that we have to do next and by the [34:12] way this is where I think this [34:14] programmable program search could be [34:17] really valuable because it might be that [34:19] you're working in a world where you've [34:21] got multiple protocols going on at one [34:22] so you've got multiple resources that [34:24] you need to deal with and there are [34:26] several valid things that you could do [34:28] next I mean here the the valid thing to [34:30] do next in this protocol is going to be [34:32] to receive something but it might be [34:34] that the next thing I want to do is [34:35] nothing to do with the protocol so it [34:36] might be that you want to write kind of [34:38] special-purpose tactics for ok I want to [34:41] do the protocol thing now do me the next [34:43] thing in the protocol that's not ready [34:45] yet that's not something we have a [34:46] language for expressing yet I would love [34:48] to have a language for expressing that [34:51] so let's you know complete that so [34:54] that's that's not a complete client [34:56] we've seen what happens if this goes [34:58] wrong I haven't really shown you any [35:00] error message or many error messages yet [35:01] let's see what happens if I try to if I [35:08] send true and then I just pull back the [35:11] the string so this has to be a string [35:13] because I'm using string append so this [35:15] hopefully won't type check because if [35:18] this type checks and everything about [35:20] this is a lie [35:21] I'll thank God for that [35:23] certainly so it didn't slide mismatch [35:26] between character and strength that's [35:27] what we expect so it's expecting a [35:28] character got string so if we look at [35:33] the error messages are a little bit ugly [35:35] I think I think this is something where [35:36] if someone came into polish this up a [35:39] bit it could be really valuable because [35:40] now if you look at if you look if you [35:42] get the location and you match the [35:44] location to the point in the file you'll [35:46] find it exactly this that it's pointing [35:48] at so there's a leave this that's got I [35:50] mean it's kind of technically it's this [35:51] that we did Rob but this is the point [35:54] where I found the error so I think I [35:55] think that's somewhere where it might be [35:57] worth exploring where we can do a bit [35:59] better here too so something else that [36:00] might go wrong is you know let's imagine [36:03] that we've sold this is a million dollar [36:05] business this little protocol and then [36:07] then a customer comes along and says oh [36:08] actually I want you to send an integer [36:10] back after the character so hang on I'm [36:16] I'm integrating anti false yeah okay [36:19] I wanted you to send an integer back [36:20] after the string so it's always [36:23] interesting to see what happens if I if [36:25] I don't somebody violate the protocol [36:27] but I changed the protocol so that my [36:28] program doesn't work anymore so what [36:30] happens it says I know you've got a [36:33] mismatch here because you need to send [36:37] some of this is actually in the server [36:38] so you need to send something but what [36:40] you did was close the channel so so by [36:43] so by changing that expression of the [36:47] description of the protocol we've got a [36:49] type error in the program so essentially [36:51] that session types was kind of kind of [36:53] basic implementation of second types but [36:55] one thing I think they want one thing I [36:56] found really nice is that it turns out [36:58] if you have dependent linear types then [37:00] it's an actual thing to be able to [37:01] express so so that's my last example I'm [37:08] going to show you my conclusion slide if [37:10] we can call it a slide so I think [37:13] interesting is making some good progress [37:14] I'm certainly having loads of fun with [37:17] it I'm just having loads of fun not [37:18] waiting for the result of the type [37:19] checker quite honestly so most of the [37:22] other Swan constructs are there sadly [37:24] there's a couple of incompatibilities so [37:26] we're not just going to be able to [37:27] suddenly flick a switch and be [37:29] self-hosting there's a little bit more [37:31] of a step to do I think it's a step [37:33] that's worth taking because you know [37:35] we're [37:36] with your own system you know you're [37:37] always gonna make it better but it's [37:40] pretty much there it's there I would [37:41] love for people to have a go let me know [37:44] what you succeed with what you don't [37:46] succeed with anything we can do to help [37:48] quantity the type theory I've only just [37:50] started playing with it you've basically [37:52] seen every bit of qtt I've done in some [37:55] form in this talk so I think we gonna [37:58] have a lot of fun exploring what is [38:00] actually possible all kinds of things we [38:02] can express gonna be fun finding that [38:04] out and then interactive editing there's [38:07] a lot more we can do with interactive [38:08] editing really important that it's [38:11] responsive so this is I want this to be [38:13] the default mode in which you people [38:14] interact with the system if that's going [38:16] to be the case it has to come back with [38:18] the answer very quickly so I think we [38:19] need to put a lot of that effort into [38:21] into efficiency that we just haven't so [38:23] far [38:24] finally definitely need your help just [38:29] there are some little things some big [38:30] things like we can always use more [38:32] libraries we could use you know work on [38:35] package management tools we could use [38:37] more editor support for example I prefer [38:40] to be using vim than Assam sorry I said [38:43] that out loud to the Emacs users but [38:45] there you have it [38:46] bit of Polish would be nice you know [38:48] pretty errormsgs but if tab completion [38:50] all sorts of things so if you look here [38:52] if you go to the github repo I've [38:55] written I've written a lot of this down [38:56] in in contributing MD does anything I [38:59] can do that could help you find your way [39:01] around the codebase please let me know [39:04] I'm nearly out of time so I probably [39:06] don't have any time for questions but so [39:08] much time for questions but thank you [39:10] for your attention [39:27] there's one over here hello thank you [39:34] entertaining as always just in your door [39:37] example I have a quick question the [39:39] dependent pair he had X Y yeah and why [39:44] was linear where X was not quite work [39:46] out why that is that's because I didn't [39:48] show you the definition of that type and [39:50] it's because I say in the type first [39:53] thing is not linear but the second thing [39:55] is so so so you can do that so come to [40:02] disappointingly so I you know kind of [40:04] wanted to give a more magical answer but [40:05] yeah that's what what is [40:17] okay thank you [40:24] [Applause] [40:37] you