  Dependent types allow us to express precisely what a function is intended to
do. Recent work on Quantitative Type Theory (QTT) extends dependent type
systems with linearity, also allowing precision in expressing when a function
can run. This is promising, because it suggests the ability to design and
reason about resource usage protocols, such as we might find in distributed and
concurrent programming, where the state of a communication channel changes
throughout program execution. As yet, however, there has not been a full-scale
programming language with which to experiment with these ideas. Idris 2 is a
new version of the dependently typed language Idris, with a new core language
based on QTT, supporting linear and dependent types. In this paper, we
introduce Idris 2, and describe how QTT has influenced its design. We give
examples of the benefits of QTT in practice including: expressing which data is
erased at run time, at the type level; and, resource tracking in the type
system leading to type-safe concurrent programming with session types.
