modal types, generalized arrows, and core passes written in coq

[Simon Peyton-Jones]

Adam

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.

Simon

|  -----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:
|  
|    http://www.cs.berkeley.edu/~megacz/garrows/
|  
|  Information on how I use Coq to write GHC passes can be found here:
|  
|    http://www.cs.berkeley.edu/~megacz/coq-in-ghc/
|  
|  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
|  http://www.haskell.org/mailman/listinfo/cvs-ghc