Home

Concoqtion: Indexed Types Now!

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? :-)

By Paul Snively at 2007-03-12 15:20 | DSL | Functional | Implementation | Semantics | Type Theory | other blogs | 8829 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Quick service

I must say, I didn't expect an answer that fast!

This will enable me to fulfill the lifetime dream of writing

Qed.

as a valid statement in my program :^)

Josh

By J Storrs Hall at Mon, 2007-03-12 19:05 | login or register to post comments

Concoqtion

Walid's talk at PEPM, in which he explained the general design ideas for this, was very good. The slides are nice, but it's not quite the same as hearing Walid deliver it.

We had a nice discussion about Concoqtion too. With this, Walid (and co-authors) is explicitly exploring a particular portion of the design space for very powerful types. It is essentially at a logical extreme, where one does a full embedding of a theorem prover in a programming language. There are many points in-between (some of which I am quite interested in myself). The main reason to mention this is that for many of the examples in the paper, Concoqtion is actually serious overkill. That should not be taken as a negative reflection on Concoqtion, but rather as a negative of the examples [which themselves are mostly a reflection of the amount of space allowed on a PEPM paper and time pressures to get it all done].

It is a very interesting dual of sorts to program-extraction from Coq! In Coq, if one of your proofs does not have computational content, you have to be very careful to ensure that no code will be emitted for it. In contrast, by type erasure, we know [and I confirmed this with Walid] that all Coq proofs will have no 'traces' left at run-time of a Concoqtion program.

By Jacques Carette at Mon, 2007-03-12 20:15 | login or register to post comments

Duality with extraction

Actually, if a proof does not have any computational content (ie, it is in Prop), then it won't get extracted at all. The problem you could have with indexed types is some reindexing code lying around (to get an inductive from one index to an other, equal one), but if you inline such coercions during extraction they will simply disappear. So, what Coq lacks is a system for not extracting indexes themselves (and there's work on it based on the calculus of implicit constructions), not proofs on them. Hope I've cleared it up a bit :)

By Matthieu Sozeau at Tue, 2007-03-13 07:07 | login or register to post comments

GADT type-level proofs require runtime checking in Haskell?

Doesn't Oleg (et al)'s recent paper on resource aware programming use GADTS to do compile time type-level static property checking?

Or am I confused (again)?

By Phil Armstrong at Tue, 2007-03-13 10:47 | login or register to post comments

Sometimes

See , the "dependently-typed append" section, for details:

The solutions demonstrate two different levels of dependent typing. In both cases, we formulate the desired properties using dependent types, and attach them as signatures to functions. We may regard these dynamically-typed signature as ``compile-time assertions''. If the use of our function in a particular expression violates the assertion, the expression is flagged as ill-typed. In a semi-dynamic case, a run-time check is inserted. If a program compiled, it does not mean that append truly respects the sum-of-sizes constraint. It merely means that in this particular compilation unit, all the uses of append were statically found to respect the length constraint. The more powerful approach, exhibited in Epigram, is to say that in all possible compilations append shall be found to satisfy the length constraint.

Thus, at one level of dependent typing, assertions about a particular function are checked at the usage occurrences of that function, within the particular context of those occurrences. A far more stronger level of dependent typing guarantees that the assertions hold universally, in all possible contexts. That level checks the definition of the function. The difference between the levels is akin to the difference between `dynamic' and `static' typing, but only at the compile-time.

By Paul Snively at Tue, 2007-03-13 15:10 | login or register to post comments

Sometimes

See "dependently-typed append" for details:

The solutions demonstrate two different levels of dependent typing. In both cases, we formulate the desired properties using dependent types, and attach them as signatures to functions. We may regard these dynamically-typed signature as ``compile-time assertions''. If the use of our function in a particular expression violates the assertion, the expression is flagged as ill-typed. In a semi-dynamic case, a run-time check is inserted. If a program compiled, it does not mean that append truly respects the sum-of-sizes constraint. It merely means that in this particular compilation unit, all the uses of append were statically found to respect the length constraint. The more powerful approach, exhibited in Epigram, is to say that in all possible compilations append shall be found to satisfy the length constraint.

Thus, at one level of dependent typing, assertions about a particular function are checked at the usage occurrences of that function, within the particular context of those occurrences. A far more stronger level of dependent typing guarantees that the assertions hold universally, in all possible contexts. That level checks the definition of the function. The difference between the levels is akin to the difference between `dynamic' and `static' typing, but only at the compile-time.

By Paul Snively at Tue, 2007-03-13 15:11 | login or register to post comments