Many holes in hindley-milner

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish
Title of host publicationML '08: Proceedings of the 2008 ACM SIGPLAN workshop on ML
PublisherAssociation for Computing Machinery
Pages59-68
Number of pages10
ISBN (Print)9781605580623
DOIs
Publication statusPublished - Sep 2008
Event2008 ACM SIGPLAN workshop - Victoria, Canada
Duration: 21 Sep 200821 Sep 2008

Conference

Conference2008 ACM SIGPLAN workshop
CountryCanada
CityVictoria
Period21/09/0821/09/08

Fingerprint Dive into the research topics of 'Many holes in hindley-milner'. Together they form a unique fingerprint.

  • Cite this

    Lindley, S. (2008). Many holes in hindley-milner. In ML '08: Proceedings of the 2008 ACM SIGPLAN workshop on ML (pp. 59-68). Association for Computing Machinery. https://doi.org/10.1145/1411304.1411313