Programming in System Fω using Dhall

This book is an advanced tutorial on functional programming in System Fω using Dhall. The book's topics include an overview of Dhall's type system; techniques for numerical calculations in Dhall; techniques for encoding recursive types and code in System F$\omega$ via the Church encoding; implementation of various combinators and typeclass derivation for functors, monads, and other typeclasses; and some basic applications of dependent types. The book shows many code examples that have been validated by the Dhall interpreter.