Hasochism :The pleasure and pain of dependently typed haskell programming

Sam Lindley, Conor McBride

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

23 Citations (Scopus)


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 publicationHaskell '13: Proceedings of the 2013 ACM SIGPLAN symposium on Haskell
PublisherAssociation for Computing Machinery
Number of pages12
ISBN (Print)9781450323833
Publication statusPublished - Sep 2013
Event2013 ACM SIGPLAN Haskell Symposium - Boston, United States
Duration: 23 Sep 201324 Sep 2013


Conference2013 ACM SIGPLAN Haskell Symposium
Abbreviated titleHaskell 2013
Country/TerritoryUnited States


  • Data type promotion
  • Dependent types
  • Invariants
  • Proof search
  • Singletons

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'Hasochism :The pleasure and pain of dependently typed haskell programming'. Together they form a unique fingerprint.

Cite this