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

[Adam Megacz]

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
BuildFlavour=quickest?


>> 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
instances.


> 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 :-)

Good point.


>> 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.

  - a