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