Hostname: page-component-7c8c6479df-xxrs7 Total loading time: 0 Render date: 2024-03-28T15:11:04.771Z Has data issue: false hasContentIssue false

Faking it Simulating dependent types in Haskell

Published online by Cambridge University Press:  08 July 2003

CONOR McBRIDE
Affiliation:
Department of Computer Science, University of Durham, Science Laboratories, South Road, Durham DH1 3LE, UK (e-mail: c.t.mcbride@durham.ac.uk)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Dependent types reflect the fact that validity of data is often a relative notion by allowing prior data to affect the types of subsequent data. Not only does this make for a precise type system, but also a highly generic one: both the type and the program for each instance of a family of operations can be computed from the data which codes for that instance. Recent experimental extensions to the Haskell type class mechanism give us strong tools to relativize types to other types. We may simulate some aspects of dependent typing by making counterfeit type-level copies of data, with type constructors simulating data constructors and type classes simulating datatypes. This paper gives examples of the technique and discusses its potential.

Type
Research Article
Copyright
© 2002 Cambridge University Press
Submit a response

Discussions

No Discussions have been published for this article.