search

gmalecha / mirror-core

A framework for extensible, reflective decision procedures.
Other
19 stars 5 forks source link

Modular Types with Higher Kinds #98

Open gmalecha opened 7 years ago

gmalecha commented 7 years ago

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 commented 7 years ago

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 commented 7 years ago

@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 commented 7 years ago

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

gmalecha commented 7 years ago

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.