Frederic Kettelhoit, A Prelude for Agda
A Prelude for Agda
Dependent types promise the open-minded programmer a wealth of powerful ways to describe properties about their program, but the cost of this blessing is high: Many dependently typed ``programming languages'' are more theorem provers than programming languages and lack convenience for anyone not well versed in the depths of their standard libraries.
Agda is a dependently typed language which explicitly intends to be useful also for programming and not just for proving, and its standard library indeed offers most of the necessary functionality. Unfortunately a myriad of name clashes between the different modules make the life of an aspiring Agda programmer rather unpleasant.
This thesis aims to improve the situation by implementing type classes which resolve many of the name clashes. Even though type classes are well understood in the context of non-dependently typed languages, the more sophisticated types in Agda often make the situation more interesting and require some workarounds. A number of type classes together with additional functionality are bundled into a ``Prelude'', which provides all the necessary data types and functions for day-to-day Agda programming. Apart from the Prelude itself, two example programs will be discussed that show the successful usage of the Prelude in the context of IO-related programs.