You may have heard about the high degree of safety you can achieve by using new and experimental, dependently-typed programming languages, but did you know that you can get some of those benefits in a programming language you already know and use? Enter the GADT: your gateway to writing safer code today.
Generalized Algebraic Data Types (GADTs) allow programmers to provide extra information to their programming language’s type system based on values of types. Using this, programmers can write code that forces the compiler to prove certain facts about the code being compiled before type checking terminates. While GADTs are significantly more limited than dependently-typed programming languages, there is still a class of bugs we can protect ourselves from by using GADTs, bugs that would ordinarily be accepted by the compiler. We will review a variety of patterns with GADTs, including encoding Peano numbers, restricting sizes of data structures, using typed heterogeneous data structures, and restricting certain states of values at compile time. We will also review practical applications of these techniques to catch bugs, including an example or two of how my company is using GADTs to better validate our cryptocurrency protocol. The talk will focus on the OCaml programming language, but these techniques apply to any language with support for GADTs.
29 сен 2024
