Many holes in hindley-milner

Sam Lindley

doi:10.1145/1411304.1411313

Many holes in hindley-milner

Sam Lindley

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, we extend our representation to allow holes to be marked with additional type information. As an example, we use these marks to implement statically-typed multi-holed XHTML contexts. We take advantage of Garrigue's relaxed value restriction.

Original language	English
Title of host publication	ML '08: Proceedings of the 2008 ACM SIGPLAN workshop on ML
Publisher	Association for Computing Machinery
Pages	59-68
Number of pages	10
ISBN (Print)	9781605580623
DOIs	https://doi.org/10.1145/1411304.1411313
Publication status	Published - Sept 2008
Event	2008 ACM SIGPLAN workshop - Victoria, Canada Duration: 21 Sept 2008 → 21 Sept 2008

Conference

Conference	2008 ACM SIGPLAN workshop
Country/Territory	Canada
City	Victoria
Period	21/09/08 → 21/09/08

Access to Document

10.1145/1411304.1411313

Cite this

@inproceedings{12d75df291db4765be675acb97c2f491,

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, we extend our representation to allow holes to be marked with additional type information. As an example, we use these marks to implement statically-typed multi-holed XHTML contexts. We take advantage of Garrigue's relaxed value restriction.",

author = "Sam Lindley",

year = "2008",

month = sep,

doi = "10.1145/1411304.1411313",

language = "English",

isbn = "9781605580623",

pages = "59--68",

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

publisher = "Association for Computing Machinery",

address = "United States",

note = "2008 ACM SIGPLAN workshop ; Conference date: 21-09-2008 Through 21-09-2008",

}

TY - GEN

T1 - Many holes in hindley-milner

AU - Lindley, Sam

PY - 2008/9

Y1 - 2008/9

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, we extend our representation to allow holes to be marked with additional type information. As an example, we use these marks to implement statically-typed multi-holed XHTML contexts. We take advantage of Garrigue's relaxed value restriction.

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, we extend our representation to allow holes to be marked with additional type information. As an example, we use these marks to implement statically-typed multi-holed XHTML contexts. We take advantage of Garrigue's relaxed value restriction.

U2 - 10.1145/1411304.1411313

DO - 10.1145/1411304.1411313

M3 - Conference contribution

SN - 9781605580623

SP - 59

EP - 68

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

PB - Association for Computing Machinery

T2 - 2008 ACM SIGPLAN workshop

Y2 - 21 September 2008 through 21 September 2008

ER -

Many holes in hindley-milner

Abstract

Conference

Access to Document

Fingerprint

Cite this