modal types, generalized arrows, and core passes written in coq
simonpj at microsoft.com
Fri Mar 4 06:24:40 CET 2011
Wow. My brain exploded when I read about what you've done. I don't understand it at all, but it sounds impressive. Do show it to me when you have a chance.
| -----Original Message-----
| From: cvs-ghc-bounces at haskell.org [mailto:cvs-ghc-bounces at haskell.org] On Behalf
| Of Adam Megacz
| Sent: 02 March 2011 22:59
| To: cvs-ghc at haskell.org
| Subject: modal types, generalized arrows, and core passes written in coq
| With much gratitude to everybody who put up with my incessant CoreSyn
| questions, I'd like to announce "very early preview" availability of
| -XModalTypes and GHC.GArrow, mainly in order to collect feedback.
| Information on the extensions to allow modal types and flatten them into
| GArrow terms is here:
| Information on how I use Coq to write GHC passes can be found here:
| More details will arrive over the course of the next week, but
| feedback/advice is most welcome (either here or off-list). If you're
| itching to actually try compiling some programs, I suggest waiting until
| Monday; there are still a bunch of quirks to be ironed out.
| The -XModalTypes extension and flattening pass are the main focus and
| are what I will be working on most intensely over the next three weeks;
| the coq-in-ghc bit was mostly a means to an end.
| Thanks again to everybody who helped me figure out GHC's guts!
| (especially Dimitrios and SPJ).
| - a
| Cvs-ghc mailing list
| Cvs-ghc at haskell.org
More information about the Cvs-ghc