Hasochism: the pleasure and pain of dependently typed haskell programming

Sam Lindley, Conor McBride

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Haskell's type system has outgrown its Hindley-Milner roots to the extent that it now stretches to the basics of dependently typed programming. In this paper, we collate and classify techniques for programming with dependent types in Haskell, and contribute some new ones. In particular, through extended examples---merge-sort and rectangular tilings---we show how to exploit Haskell's constraint solver as a theorem prover, delivering code which, as Agda programmers, we envy. We explore the compromises involved in simulating variations on the theme of the dependent function space in an attempt to help programmers put dependent types to work, and to inform the evolving language design both of Haskell and of dependently typed languages more broadly.
Original languageEnglish
Title of host publicationProceedings of the 2013 ACM SIGPLAN Symposium on Haskell, Boston, MA, USA, September 23-24, 2013
Number of pages12
ISBN (Print)978-1-4503-2383-3
Publication statusPublished - 2013

Cite this