Many holes in Hindley-Milner

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
Original languageEnglish
Title of host publicationML '08 Proceedings of the 2008 ACM SIGPLAN workshop on ML
Number of pages9
Publication statusPublished - Jun 2008


  • multi-holed context


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

Cite this