Yes, quoted code is typechecked. The right way to express the result would be for the TH implementation to make a data structure (Exp, Decl etc) representing the *typed* code, and then do_something could look at those types. This does come up quite regularly. So why have I not done it? (a) It needs some design work on TH syntax. It must be able to express typed code (produced by quotes) and untyped code (produced by the user's program) (b) The types are only partly there. For example \x -> $(do_something [| \y -> x |]) Here the (\y->x) doesn't know the full type for x. Indeed just, x's type may not be fully worked out by the time do_something runs. For example we might have \x -> ($(do_something [| \y -> x |]), x::Int) Eventually we know that x::Int, but perhaps not when we run do_something. It depends on the order in which the type checker does things. This is a pretty nasty problem because the semantics of TH would then depend on order of type checking etc. (c) When type checking a splice, should we ignore types in the TH code, or respect them? And, of course, it's work do to. The big one is (b). A pragmatist would say just go ahead and hack something up -- if you get type information it'll be accurate, but there's no guarantee of what you'll get. But I hate that. So that's why I keep postponing it. Better ideas welcomed. Simon | -----Original Message----- | From: Keean Schupke [mailto:k.schupke@imperial.ac.uk] | Sent: 23 February 2005 14:16 | To: Simon Peyton-Jones | Subject: template-haskell | | Had a bit of a chat on the template-haskell list about type checking | meta quoted code... would it be possible (as I don't think it is currently | supported) to get the type of meta-quotes expressions,. like: | | $(do_something [| | f a = a + 1 |] ) | | such that inside the splice we can access the type info for 'f'. | | I know it is type checked, because if will pick up type errors in the | meta quotes, | before macro expansion. | | One way of doing this would be to annotate the meta-quote with the type | info like: | | [| | f :: Num a => a -> a | f a = a + 1 | |] | | In other words if the type sig for 'f' is not given, add it to the data | structure returned from | the meta quotes... | | What do you think? possible? easy/hard? | | Keean.
Thanks for the info... some comments: Simon Peyton-Jones wrote:
Yes, quoted code is typechecked. The right way to express the result would be for the TH implementation to make a data structure (Exp, Decl etc) representing the *typed* code, and then do_something could look at those types. This does come up quite regularly.
So why have I not done it?
(a) It needs some design work on TH syntax. It must be able to express typed code (produced by quotes) and untyped code (produced by the user's program)
TH already has type syntax, as I can examine: [| f :: Num a => a -> a f a = a + 1 |] So I am not sure I understand which bit of syntax is missing?
(b) The types are only partly there. For example \x -> $(do_something [| \y -> x |]) Here the (\y->x) doesn't know the full type for x. Indeed just, x's type may not be fully worked out by the time do_something runs. For example we might have \x -> ($(do_something [| \y -> x |]), x::Int) Eventually we know that x::Int, but perhaps not when we run do_something. It depends on the order in which the type checker does things.
This is a pretty nasty problem because the semantics of TH would then depend on order of type checking etc.
Actually I would be happy with the best guess so far without going outside the current context, so for the above: \x -> ($(do_something [| \y -> x |]), x::Int) The type could be " a -> a " ... IE just looking at the anonymous functions it is fully polymorphic. You could veiw this as the most specific type available without information from outside the meta-quote, which is the only definition that makes sense to me at the moment.
(c) When type checking a splice, should we ignore types in the TH code, or respect them?
The easyest answer is do not put the types in. If TH creates two data structures, one with the code as written in the meta-quotes, and one containing the (derived) types of the functions: for example: f :: Num a => a -> a f a = a + 1 g b = putStrLn (show b) We would get one structure containing the definitions of f & g and the type sig for f, and another containing the (derived) type-sig for g. The programmer could then merge the two structures if wanted.
And, of course, it's work do to.
The big one is (b). A pragmatist would say just go ahead and hack something up -- if you get type information it'll be accurate, but there's no guarantee of what you'll get. But I hate that.
Even if more information is supplied outside the meta-quote context, any more general type derived inside is not wrong... it might just be more generalised than necessasry - but it is still a correct type, and I have no problem with is being more general than necesary - it makes sense that the code inside the meta-quotes should be viewed as a constant fragment, so its type should be fixed irrespective of the context in which it is used...
So that's why I keep postponing it. Better ideas welcomed.
This is really very useful, for example we can use it to let the compiler derive the constraints on a function (using class methods), and then extract the constraints from the type and build an instance... This should make it possible to derive a class instance from a function: $(derive ''Show [| showsPrec _ (MyType a) = shows a |] ) which could generate: instance Show a => Show (MyType a) where showsPrec _ (MyType a) = shows a Keean.
participants (2)
-
Keean Schupke -
Simon Peyton-Jones