#38 Haskell, Lean, Idris, and the Art of Writing - David Christiansen
2024/5/16
Type Theory Forall
D
David Christiansen
@David Christiansen : 我对函数式编程的兴趣始于大学时期，当时我学习了Lisp和Haskell等语言。早期的学习经历并不顺利，因为学习资源匮乏，而且我对lazy lists的理解不足。我的本科专业是哲学，辅修计算机科学，这使得我的学习经历与众不同。在学习过程中，我逐渐对类型理论产生了兴趣。
我的博士研究课题最初是关于一个用于指定精算产品的DSL，但在研究过程中，我开始探索依赖类型，并参与了Idris的开发。我的博士导师Peter Sestov对我的研究提供了很大的帮助，他注重沟通和交流，鼓励我向公众传播知识。
在职业生涯中，我曾担任Haskell基金会的执行董事，这段经历让我对不同社区成员的观点和需求有了更深入的理解。目前，我主要负责Lean项目的Verso文档系统，这是一个旨在简化文档编写过程并提高代码示例准确性的工具。
在选择新项目时，我会考虑项目的趣味性和能否满足生活需求。我比较享受写作和与人交流的过程。
关于依赖类型在主流编程中的应用，我认为这取决于其易用性和周边生态系统的成熟度，以及在特定领域中的实际价值。目前，依赖类型在软件验证领域已经取得了进展，但在主流编程中的应用仍需克服诸多挑战。
@Pedro Abreu : 作为主持人，引导访谈的进行，并就函数式编程、依赖类型、学术研究等话题与David Christiansen进行深入探讨。
@Francesc Campoy : 作为主持人，引导访谈的进行，并就函数式编程、依赖类型、学术研究等话题与David Christiansen进行深入探讨。
Deep Dive
David Christiansen's path to functional programming started with a curiosity for Lisp and Haskell during his undergraduate years. Despite studying in a C++-focused environment, he pursued these interests, leading to projects like a Markov chain text generator. After a detour in philosophy and IT work, he returned to academia, driven by a desire to learn and contribute. His PhD journey, focused on a DSL for actuarial products, took an unexpected turn when he encountered Idris, a dependently typed language that captivated his interest and ultimately reshaped his research.
- David's interest in functional programming began with Lisp and Haskell.
- He pursued these interests despite a C++-focused academic environment.
- His PhD project shifted from a DSL for actuarial products to working with Idris.