On 3/19/08, John Meacham
Well, it seems like constrain doesn't really have any choice but to throw an error when asked to constrain a KBase KQuest with a KindSimple constraint... it has no way of indicating that the result should be a KBase KStar!
I was hoping you might have something to say about this?
Ah, sorry. I was mulling it over. Basically, it has to do with the issue that '?' and '??' are not real kinds. they are just shorthand for kind abstractions.
when you say: data App :: ?? -> ? -> *
you actually mean:
(in psuedo-haskell)
data App :: forall (k1 | k1 `elem` [*,#]) (k2 | k2 `elem` [*,#,(#)]) . k1 -> k2 -> *
the constraints are what is to the right of the |'s there. (I could also do this with superkinds, though I think constrained polymorphism is the way to go here.).
so, ? should not actually be a kind of type '?' but actually a newly instantiated kind variable with a KindQuest constraint on it. This instantiation should be done whenever we pull something out of the kind environment.
However, since full kind polymorphism isn't availibe in the front end, we use ? and ?? as placeholders in our code as well as data structures.
they actually behave the same as if they had been declared:
kindsynonym ?? = exists k | k `elem` [*,#] . k
Right now, for compatability with haskell 98 and because I would need to modify some data structures to handle it, we perform a 'defaulting', defaulting all kindvars to * at the end of inference. we could just as easily perform a generalization there and get true kind polymorphism. (and this will be done eventually)
note that type synonyms are already kind polymorphic:
type UIO a = World__ -> (# World__, a #)
'UIO Int' and 'UIO Bits32_' are both fine.
UIO :: forall k . k -> *
(actually, to be fully formal, UIO has superkind polymorhism, but that is irrelevant since type synonyms don't make it to jhc core, jhc can handle that fine, but I think I will wait until 'kind level' programming becomes popular before crossing that bridge :) )
so. to answer the question of why that case dealing with KQuest isn't in constrain, it is either because
1. I forgot it, it actually should be there.
or
2. an actual '?' or '??' is sneaking in as a kind when it should have been turned into a freshly instantiated kind variable with a ? or ?? constraint as appropriate.
Where is this process supposed to happen? I didn't see anything that looked like that in KindInfer, and I don't think it could be anywhere else, since the monad it would need to work in is only available in that module...
as an aside, it is interesting to note that methodless type classes give a sort of constrained polymorphism at the type level, I am not sure the signifigance exactly of this, but it might lead to a more elegant handling of kinds in the future... uncharted waters.