| What would be most flexible for the user is to return the best | information that is available. In the example: | | >NB This can apply to top-level decls too: | > f = 1+2 | > $( ... reify 'f... ) | > g = f + (4::Int) | > | >Because of the monomorphism restriction, the type of f is fixed by f's | >caller, which may be "after" the reification. | > | it might still be useful to find out that an approximation to the type | is f :: Num a => a, even though that isn't the final type. That would | suggest something like | | data TypeQuery a = ExactType a | ApproximationType a Actually, I was thinking of something more modest. The type of f will, at the stage of reification, be a -> a where a is an as-yet-refined internal type variable. If instead we had id x = x the type would be forall a. a->a So I'm thinking that if the Type returned to you by TH contains free type variables, that might simply signify types that might be later refined. Simple. But not very principled, because the type you see will depend on which order the type checker happens to do its work in. Simon
Hi Simon,
So I'm thinking that if the Type returned to you by TH contains free type variables, that might simply signify types that might be later refined. Simple.
That sounds good, it provides the information that ghc knows in a way that's useful to the application.
But not very principled, because the type you see will depend on which order the type checker happens to do its work in.
That's right, but this may be inevitable in a staged system. There might be some applications where this is a serious issue, but at least for my work, your suggestion above would be fine - it doesn't actually matter to me whether the free type variables get refined later. I would like to go ahead with this proposal for reification. I don't know how to get around these "problems of principle", or ever whether it is possible to solve them, but making partial type information available would enable me to do some things that I just cannot do with the current system. John Simon Peyton-Jones wrote:
| What would be most flexible for the user is to return the best | information that is available. In the example: | | >NB This can apply to top-level decls too: | > f = 1+2 | > $( ... reify 'f... ) | > g = f + (4::Int) | > | >Because of the monomorphism restriction, the type of f is fixed by f's | >caller, which may be "after" the reification. | > | it might still be useful to find out that an approximation to the type | is f :: Num a => a, even though that isn't the final type. That would | suggest something like | | data TypeQuery a = ExactType a | ApproximationType a
Actually, I was thinking of something more modest. The type of f will, at the stage of reification, be a -> a where a is an as-yet-refined internal type variable. If instead we had
id x = x
the type would be forall a. a->a
So I'm thinking that if the Type returned to you by TH contains free type variables, that might simply signify types that might be later refined. Simple.
But not very principled, because the type you see will depend on which order the type checker happens to do its work in.
Simon
_______________________________________________ template-haskell mailing list template-haskell@haskell.org http://www.haskell.org/mailman/listinfo/template-haskell
So I'm thinking that if the Type returned to you by TH contains free type variables, that might simply signify types that might be later refined. Simple.
But not very principled, because the type you see will depend on which order the type checker happens to do its work in.
I've got some alarm bells ringing here. It seems to me that any application that used this extra information would be very brittle - a small change in the code or, it seems, in the compiler could change something from working to not working or from being fast to being slow or <whatever benefit it is that the extra information gives you>. Maybe I just don't understand John's application enough? [Sorry John, I missed your IFL talk when it was moved to after the end of IFL.] -- Alastair
Hi Alastair and Simon... Alastair Reid wrote:
So I'm thinking that if the Type returned to you by TH contains free type variables, that might simply signify types that might be later refined. Simple.
But not very principled, because the type you see will depend on which order the type checker happens to do its work in.
I've got some alarm bells ringing here.
It seems to me that any application that used this extra information would be very brittle - a small change in the code or, it seems, in the compiler could change something from working to not working or from being fast to being slow or <whatever benefit it is that the extra information gives you>.
The point is that my application (Hydra) shouldn't ever need the values of the type variables; what it needs is the top level function type. An example might be something like f :: Signal a => (a, [a]) -> a -> (a,[(a,a)]) Now, I believe it to be the case that at least this much of the type will always be known, and that's all I need. Later on it might turn out that the type is really f :: (Stream CMOS, [Stream CMOS]) -> Stream CMOS -> ... and you're right, it would be brittle to rely on having that extra information -- but I don't need that extra information. The problem is that conceivably the typechecker might only come up with something like f :: b -> a -> (a, [(a,a)]) where later on it will be discovered that b is actually (a,[a]). If this were to happen it might be a problem (but still wouldn't be disastrous). However, I think there are going to be enough other constraints that such an over-general type would not arise at all. If I understand things correctly, my TH code would at least know if there is a problem. If it sees an unexpected free type like b in the above, it would *know* that it doesn't know enough about the type, and could emit an error message asking the user to provide a type declaration. Does this sound reasonable? I don't have time to be more clear - lectures coming up.
Maybe I just don't understand John's application enough? [Sorry John, I missed your IFL talk when it was moved to after the end of IFL.]
Ah yes... that's what comes of trying to give a talk with laptop and beamer :-) Cheers, John
participants (3)
-
Alastair Reid -
John O'Donnell -
Simon Peyton-Jones