Thumbnail
Access Restriction
Open

Author Lindley, Sam ♦ Mcbride, Conor
Source CiteSeerX
Content type Text
File Format PDF
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Theorem Prover ♦ Dependent Type ♦ Type System ♦ Dependent Function Space ♦ Hindley-milner Root ♦ Evolving Language Design ♦ Agda Programmer ♦ New One ♦ Rectangular Tiling ♦ Con-straint Solver
Description In Proceedings of the 2013 ACM SIGPLAN Symposium on Haskell, Haskell ’13
Haskell’s type system has outgrown its Hindley-Milner roots to the extent that it now stretches to the basics of dependently typed pro-gramming. In this paper, we collate and classify techniques for pro-gramming 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 con-straint 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.
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research
Education Level UG and PG ♦ Career/Technical Study
Learning Resource Type Article
Publisher Date 2013-01-01