Modular Types with Higher Kinds

[gmalecha]

This is an extension to @mmalvarez's work on core types that includes support for higher kinds, e.g. you have a deep embedding of types that are not of sort Type.

For example, there is a representation of option rather than option T for some T. This makes it possible to implement more sophisticated structures, e.g. functors, applicatives, and monads, that can not be represented in without higher-order types.

Note: Not yet ready to merge.

[gmalecha]

I'm thinking that I will leave in CTypes for the time being even though its implementation is morally equivalent to Types.FTypes. The CTypes implementation might be faster because the kind language is implicit. The downside of this is that because it doesn't match up with the interface, I will have to resurrect a bunch of code.

[gmalecha]

@jesper-bengtson We should see if theories/Types/FTypes.v (this is morally the same as the old modular types) or theories/Types/HTypes.v (this includes higher kinds) will work better. I believe with the current code that you are working on FTypes will probably be sufficient, though automating something like Applicative might be easier with HTypes.

[gmalecha]

@mmalvarez would you be up for doing a code review before this gets merged?

[gmalecha]

The library code is done, but the interface is not very usable without patterns. Unfortunately, this is just an aspect of Coq usability, dependent pattern matching does not have good enough heuristics.