Many holes in hindley-milner

Sam Lindley

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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
Number of pages10
ISBN (Print)9781605580623
Publication statusPublished - Sept 2008
Event2008 ACM SIGPLAN workshop - Victoria, Canada
Duration: 21 Sept 200821 Sept 2008


Conference2008 ACM SIGPLAN workshop


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

Cite this