modal types, generalized arrows, and core passes written in coq
megacz at cs.berkeley.edu
Sat Mar 12 22:46:35 CET 2011
Max Bolingbroke <batterseapower at hotmail.com> writes:
> It is possible that it just takes an extremely long time to build -
That is certainly the case. You need to let it run for at least four or
five minutes on a fast machine. Also, don't try to use anything above
-O0. Here's why:
> My initial diagnosis was wrong (I was confused since I was doing a
> parallel make).
The way Coq generates Haskell code for string literals is amazingly
inefficient (there's a special-case hack for Ocaml but none for
Haskell). I've managed to partly work around this in the latest
checkin, but it still takes around a minute to compile using -O0 on a
2ghz machine, so give it some time.
> after all, CoqPass.hs is huge! How long does it typically take in your
> experience? Last time I tried waiting for ~15 minutes with no luck.
Hrm, that seems too long, but I've never tried anything other than
BuildFlavour=quickest (which is what the canned
paste-it-into-a-shell-window commands use). Are you building with
>> Moreover, in the context of *heterogeneous* metaprogramming, using
>> CSP comes with a price
> What do you mean by the "price"? Runtime cost? Or the fact that CSP
> (at certain types) forces the embedded language to be a superset of
> the host language?
Precisely. A term which uses CSP gets flattened to a less-polymorphic
type than one which does not use CSP. Specifically, if you use CSP, the
flattened type will have (GArrowReify g)=> in its context. Most of the
GArrows which aren't Arrows (I suspect all of them) lack GArrowReify
> Naturally, there is no "run" that works for all languages, but since
> it is a tutorial it would be cool to see a "run" for at least one
> particular language :-)
>> It's definitely used inside code brackets; if there were a way I could
>> turn it on at syntactical-depth-greater-than-zero but off everywhere
>> else I could probably do that.
> Really? I'm probably being daft but I can't see what would go wrong if
> you turned off rebindable syntax. Can you give an example?
The flattener cannot currently handle the following constructs *inside*
code-brackets: type-lambda, type-let, coercion-lambda,
coercion-application, case-discrimination. Inside code brackets you
basically get PCF and not much more. I guess I ought to be more
up-front about this on the webpage.
So, I guess -XRebindableSyntax is just my way of getting GHC to avoid
case-branches wherever possible. But that only matters inside the code
brackets -- you've convinced me that there's no reason to have
-XRebindableSyntax active on depth=0 terms. So I'm going to try to find
a way to have -XModalTypes desugar depth>0 terms as if
-XRebindableSyntax were enabled -- that way the flag won't be necessary
and won't mess with flat terms.
Lastly, I'll add that I do know how to flatten products and coproducts,
so case on "Either" and "(,)" will probably be arriving shortly. Beyond
that it's a much bigger challenge.
More information about the Cvs-ghc