[Template-haskell] Re: template-haskell

[Keean Schupke]

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.