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 <[email protected]> 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 == > undefined! 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 > GHC.HetMet.GArrow?) 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 revisit. > 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! - a _______________________________________________ Cvs-ghc mailing list [email protected] http://www.haskell.org/mailman/listinfo/cvs-ghc
