modal types, generalized arrows, and core passes written in coq
megacz at cs.berkeley.edu
Wed Mar 9 19:20:04 CET 2011
Hi Max, I have access to email right now but not to a machine with the
code on it, so I can answer questions but can't fix bugs (yet):
Max Bolingbroke <batterseapower at hotmail.com> writes:
> 1. What is the %%a syntax in the dotproduct' function?
It's cross-stage persistence, but I need to remove that. I included CSP
out of respect for the MetaML effort, but truth be told the moment you
use CSP you've committed yourself to the guest language being a
*superset* of Haskell.
I want to add a mechanism for allowing CSP only at specific types (like,
say, Int but not (Int->Int)); this corresponds to assuming that the
guest language has literals of that type -- but prohibiting CSP at
function types keeps the entire Haskell language from leaking into the
guest language. Once I've added this I will change the example. But
thanks for noticing this; I'd forgotten about it! Curiously, this
mechanism is distinct from having literals inside code brackets.
> understand what was going on if that was ~~ instead.
That won't typecheck -- try it.
> 2. I think your tutorial would benefit from some examples showing how
> to actually run sth - your run functions are all currently ==
For good reason! Unlike homogeneous metaprogramming there is no
one-size-fits-all definition of "run" for heterogeneous metaprogramming,
nor can there be.
> I would suppose that there is some trivial way to run
> sufficiently-polymorphic modally-typed stuff as simple Haskell by
> taking g = (->), which would be good to show. (Speaking of which,
> wouldn't it make sense to have that GArrow instance in
Sure; in fact, that's precisely what a (non-generalized) Arrow is.
Every Arrow instance is a GArrow instance. I'll write the instance
definition tomorrow night and add it to the tutorial and will put it in
GHC.HetMet.GArrow as you suggest.
> 3. How is the Core -> GArrow extraction working?
At the moment, not quite in presentable shape. I hope to have it in
releasable shape by the 14th, but that will probably slip by a few days.
The code that renders GHC code as a proof tree in LaTeX is already doing
the heavy lifting, though -- if you stare at the proof tree long enough
(okay, for a *really* long time) you can probably see where the
ga_first/ga_id/ga_comp/etc invocations go.
> In particular, I'm interested in if you need to put a GArrowDrop
> constraint on extracted GArrow terms that use variables non-linearly.
I absolutely do. See HaskStrongToProof.v, arrangeContextAndWeaken --
this is where the goodies are: the heart and soul of the
Haskell-to-boxes-and-wires-aka-(pre)monoidal-categories logic is in
there. It reconstructs the explicit-Gentzen-structural-rule proof from
GHC.Core, which has implicit structural operations (there are no
weaken/exchange/contract operations in CoreSyn). It took me a very long
time to get that part right.
> 4. Do you actually use RebindableSyntax? If so, what is it needed for?
> I couldn't see any obvious place it was being used.
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. It's also partly historical; back when
all of this was in a perpetually-half-broken state I needed to be sure
the Prelude wasn't leaking in to the code brackets -- but that's no
longer a problem.
> 5. What is _c in your comment under staged_accept? The old name for
> the <>_c type constructor?
Exactly; thanks for catching this, I've fixed it. I really liked that
syntax because it looked like the subscripted box operator, which is
what the code type truly is. Unfortunately having the operator not be
"surroundfix" turned out to be a gigantic pain.
> 1. I would like GArrow as part of base even without HetMet, since
> there are so many arrows that do not have ga_reify..
Hrm, I think what you suggest is the plan -- in fact, the flattener only
adds (GArrowReify g)=>... to the context if you use CSP (the
%%-operator). I conjecture that every GArrowReify which uses (,) as its
tensor is [isomorphic to] a Haskell Arrow (and vice versa), though the
Coq proof of that fact is not yet finished. So, in that sense,
GArrowReify's are the least interesting GArrows (to me) because we've
known about those since Hughes/Power/Thielecke.
The main obstacle here is that Haskell's type system does not express
the substructural features, so you cannot be 100% sure of the flattened
type by looking at the unflattened type. This means that you can get
type errors in the flattener (which is *after* the desugarer, and
therefore bad!) if you assume a type more precise than "implements all
five classes". I doubt I will be able to solve this particular problem
in the next few weeks, but it's on my medium-range to-do list.
Incidentally, this was the motivation for my ridiculous-sounding
question a few weeks ago about whether or not the order of bindings in a
letrec is preserved. In hindsight that must have sounded like a silly
question for a pure language, but it starts to matter when you add
ordered linear types (i.e. restricted exchange rule).
> 2. I like your hack with (<[ x ]> :: t) to get two namespaces :-)
Glad you do because I'm not sure that I do! It (the multiple
namespaces) was the "least bad" of several options. I am anxious to
look for a better solution, but at the moment I don't know of any.
Unfortunately the problem is trickier than it looks... at some point
I'll write a brief summary of what I tried and found didn't work and see
if people on this list have any better ideas.
I also hope you didn't become ill at the sight of what I'd done to
OccName.NameSpace(VarName). That was another bad decision I need to
> Anyway, this looks like really cool work! I will see if I can build
> your modified GHC so I can play around (and perhaps answer some of my
> own questions above).
Please let me know if you have any problems getting it to build, and I
will be happy to help. Knowing that it builds out-of-the-box for
somebody other than me would be really awesome.
Thanks again for your insights!
More information about the Cvs-ghc