Many holes in Hindley-Milner

Samuel Lindley

doi:10.1145/1411304.1411313

Many holes in Hindley-Milner

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

Abstract

We implement statically-typed multi-holed contexts in OCaml using an underlying algebraic datatype augmented with phantom types. Existing approaches require dynamic checks or more complex type systems. In order to support concatenation we use two type parameters to represent the number of holes in a context as the difference between two Peano numbers. In order to support plugging a context with contexts of different arity we introduce a datatype of lists of contexts of length n with a total of m holes. Further

Original language	English
Title of host publication	ML '08 Proceedings of the 2008 ACM SIGPLAN workshop on ML
Pages	59-67
Number of pages	9
DOIs	https://doi.org/10.1145/1411304.1411313
Publication status	Published - Jun 2008

Keywords

multi-holed context

Access to Document

10.1145/1411304.1411313

Lindley 2008 Many Holes in Hindley-MilnerSubmitted manuscript, 136 KB

http://dl.acm.org/citation.cfm?id=1411313

Cite this

@inproceedings{729d2fd96d7649f898c441863d6c5916,

title = "Many holes in Hindley-Milner",

abstract = "We implement statically-typed multi-holed contexts in OCaml using an underlying algebraic datatype augmented with phantom types. Existing approaches require dynamic checks or more complex type systems. In order to support concatenation we use two type parameters to represent the number of holes in a context as the difference between two Peano numbers. In order to support plugging a context with contexts of different arity we introduce a datatype of lists of contexts of length n with a total of m holes. Further",

keywords = "multi-holed context",

author = "Samuel Lindley",

year = "2008",

month = jun,

doi = "10.1145/1411304.1411313",

language = "English",

isbn = "978-1-60558-062-3",

pages = "59--67",

booktitle = "ML '08 Proceedings of the 2008 ACM SIGPLAN workshop on ML",

}

TY - GEN

T1 - Many holes in Hindley-Milner

AU - Lindley, Samuel

PY - 2008/6

Y1 - 2008/6

N2 - We implement statically-typed multi-holed contexts in OCaml using an underlying algebraic datatype augmented with phantom types. Existing approaches require dynamic checks or more complex type systems. In order to support concatenation we use two type parameters to represent the number of holes in a context as the difference between two Peano numbers. In order to support plugging a context with contexts of different arity we introduce a datatype of lists of contexts of length n with a total of m holes. Further

AB - We implement statically-typed multi-holed contexts in OCaml using an underlying algebraic datatype augmented with phantom types. Existing approaches require dynamic checks or more complex type systems. In order to support concatenation we use two type parameters to represent the number of holes in a context as the difference between two Peano numbers. In order to support plugging a context with contexts of different arity we introduce a datatype of lists of contexts of length n with a total of m holes. Further

KW - multi-holed context

U2 - 10.1145/1411304.1411313

DO - 10.1145/1411304.1411313

M3 - Conference contribution

SN - 978-1-60558-062-3

SP - 59

EP - 67

BT - ML '08 Proceedings of the 2008 ACM SIGPLAN workshop on ML

ER -

Many holes in Hindley-Milner

Abstract

Keywords

Access to Document

Fingerprint

Cite this