Concoqtion: Indexed Types Now!

Almost twenty years after the pioneering efforts of Cardelli, the programming languages community is vigorously pursuing ways to incorporate F_{ω}-style indexed types into programming languages. This paper advocates Concoqtion, a practical approach to adding such highly expressive types to full-fledged programming languages. The approach is applied to MetaOCaml using the Coq proof checker to conservatively extend Hindley-Milner type inference. The implementation of MetaOCaml Concoqtion requires minimal modifications to the syntax, the type checker, and the compiler; and yields a language comparable in notation to the leading

proposals. The resulting language provides unlimited expressiveness in the type system while maintaining decidability. Furthermore, programmers can take advantage of a wide range of libraries not only for the programming language but also for the indexed types. Programming in MetaOCaml Concoqtion is illustrated with small examples and a case study implementing a statically-typed domain-specific language.

The follow-up to Concoqtion: Mixing Indexed Types and Hindley-Milner Type Inference, discussed earlier. Good stuff.

**Update:** There's now a public Concoqtion web site!

Josh, does this answer your question? :-)

## Recent comments

3 hours 48 min ago

10 hours 26 min ago

10 hours 58 min ago

18 hours 41 min ago

19 hours 15 min ago

21 hours 27 min ago

21 hours 49 min ago

1 day 1 hour ago

1 day 2 hours ago

1 day 5 hours ago