Hasochism :The pleasure and pain of dependently typed haskell programming

Sam Lindley; Conor McBride

doi:10.1145/2578854.2503786

Hasochism :The pleasure and pain of dependently typed haskell programming

Sam Lindley, Conor McBride

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

24 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 language	English
Title of host publication	Haskell '13: Proceedings of the 2013 ACM SIGPLAN symposium on Haskell
Publisher	Association for Computing Machinery
Pages	81-92
Number of pages	12
ISBN (Print)	9781450323833
DOIs	https://doi.org/10.1145/2578854.2503786
Publication status	Published - Sept 2013
Event	2013 ACM SIGPLAN Haskell Symposium - Boston, United States Duration: 23 Sept 2013 → 24 Sept 2013

Conference

Conference	2013 ACM SIGPLAN Haskell Symposium
Abbreviated title	Haskell 2013
Country/Territory	United States
City	Boston
Period	23/09/13 → 24/09/13

Keywords

Data type promotion
Dependent types
Invariants
Proof search
Singletons

ASJC Scopus subject areas

Software

Access to Document

10.1145/2578854.2503786

Cite this

@inproceedings{5f06dd3f8324465cb71ee768c77aab33,

title = "Hasochism :The pleasure and pain of dependently typed haskell programming",

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.",

keywords = "Data type promotion, Dependent types, Invariants, Proof search, Singletons",

author = "Sam Lindley and Conor McBride",

year = "2013",

month = sep,

doi = "10.1145/2578854.2503786",

language = "English",

isbn = "9781450323833",

pages = "81--92",

booktitle = "Haskell '13: Proceedings of the 2013 ACM SIGPLAN symposium on Haskell",

publisher = "Association for Computing Machinery",

address = "United States",

note = "2013 ACM SIGPLAN Haskell Symposium, Haskell 2013 ; Conference date: 23-09-2013 Through 24-09-2013",

}

TY - GEN

T1 - Hasochism :The pleasure and pain of dependently typed haskell programming

AU - Lindley, Sam

AU - McBride, Conor

PY - 2013/9

Y1 - 2013/9

N2 - 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.

AB - 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.

KW - Data type promotion

KW - Dependent types

KW - Invariants

KW - Proof search

KW - Singletons

UR - http://www.scopus.com/inward/record.url?scp=84885644496&partnerID=8YFLogxK

U2 - 10.1145/2578854.2503786

DO - 10.1145/2578854.2503786

M3 - Conference contribution

AN - SCOPUS:84885644496

SN - 9781450323833

SP - 81

EP - 92

BT - Haskell '13: Proceedings of the 2013 ACM SIGPLAN symposium on Haskell

PB - Association for Computing Machinery

T2 - 2013 ACM SIGPLAN Haskell Symposium

Y2 - 23 September 2013 through 24 September 2013

ER -

Hasochism :The pleasure and pain of dependently typed haskell programming

Abstract

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this