[Template-haskell] RE: Reification in TH

[Simon Peyton-Jones]

| I've played around with reifying types and found that one can only
| reify names that have the following format:
| 
| Name occ (NameG th_ns mod)

Well that's just a bug.  It's supposed to be possible to do

	f x = $(do { ... reify 'x .... })

modulo the caveats about how much of x's type will be visible by then.  

I'll fix that shortly.


Meanwhile you want something more ambitious that I don't understand yet.

| I might have a block of declarations like this
| 
| ds = [d|   f = ....
|                 g x = f .... x....
|           |]
| 
| It would be extra nice if I could reify the type of "x" in the
| following code.

What do you mean by "in the following code"?  You can't mean

	 ds = [d|   f = ....
	                g x = f .... x....
	         |]
	w = do { reify 'x ...

because x isn't in scope there.  And even if you say

	w = do { reify (mkName "x")... }

you'll get a dynamic error because x isn't in scope.   So I really don't
know what you mean.


Perhaps what you mean is: 
	let the Exp data structure be able to represent type-annotated
terms
	when [| ... |] constructs a data structure, let it be replete
with type annotations
	provide a way to look at these type annotations when taking the
data
		structure apart

I have thought about this a bit in the past, and it's tricky.  An
obvious place to attach type annotations would be to put the Type of a
Name inside the Name.  So you can say
	nameType :: Name -> Type
to get the type of a variable.  (Presumably it'd fail if given the Name
of a type constructor or class.)

But when the programmer constructs a Name with newName or mkName, he
doesn't want to supply a type.  So sometimes an Exp will have
type-annotated Names and sometimes not.  

And there's still the ever present aspect of only having *partial* type
information.


(More tiresomely, GHC adds lots of crud -- dictionary applications and
abstractions etc -- to the typechecked term, so it's not entirely easy
to get back to the original term.  But that part must be soluble.)

Simon

  Of course the problem is that we don't even know if
| "f" (or "g" for that matter) is going to type check until we've
spliced
| it.  So we can only reify "x"'s type at splice time.
| 
| I need the ability to reify "x"'s type and then, based on the
| information I get back, transform the block of declarations, "ds", in
a
| certain manner.
| So I would in effect be doing a kind of "speculative splice".   But a
| splice of top-level declarations can only occur at the top level! What
| I'm suggesting would be a speculative splice inside the body of a
| function, something that will ONLY work when the DecQ that we are
| splicing only contains Names that refer to functions in other modules
| or within the DecQ. (That is, we can't have the functions referring to
| variables outside the DecQ but in the current module!).  Fortunately,
| this condition is satisfied by the DecQs I wish to do reification in.
| 
| I can understand why no one would want to write a "reify" function as
| described above.
| 
| But the only reason I've been throwing functions in [d| |] brackets is
| because I can't reify entire modules. (We would have to bloat .hi
files
| for this to be the case.)  But, say this were possible.  Then it would
| be MUCH easier to code a reify function that could return the types of
| local Names, because we would already known that the module which we
| are reifying type checks and then in the bloated .hi files we could
| simple annotate each occurrence of a Name with its type.  This would
be
| extremely useful to me.
| 
| Cheers,
| 
| Sean
|