Many holes in hindley-milner

9 years 10 months ago
Many holes in hindley-milner
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.
Sam Lindley
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2008
Where ML
Authors Sam Lindley
Comments (0)