[jhc] explanation of FrontEnd.KindInfer.constrain

[Samuel Bronson]

On 3/19/08, John Meacham <john at repetae.net> wrote:

> > > 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.