Hasochism :The pleasure and pain of dependently typed haskell programming

Sam Lindley, Conor McBride

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

18 Citations (Scopus)

Abstract

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
Pages81-92
Number of pages12
ISBN (Print)9781450323833
DOIs
Publication statusPublished - Sep 2013
Event2013 ACM SIGPLAN Haskell Symposium - Boston, United States
Duration: 23 Sep 201324 Sep 2013

Conference

Conference2013 ACM SIGPLAN Haskell Symposium
Abbreviated titleHaskell 2013
CountryUnited States
CityBoston
Period23/09/1324/09/13

Keywords

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

ASJC Scopus subject areas

  • Software

Cite this