[jhc] explanation of FrontEnd.KindInfer.constrain

[Samuel Bronson]

On 3/19/08, John Meacham <john at repetae.net> wrote:
> On Wed, Mar 19, 2008 at 07:16:16PM -0400, Samuel Bronson wrote:
> > On 3/19/08, John Meacham <john at repetae.net> wrote:
> > > On Wed, Mar 19, 2008 at 06:55:29PM -0400, Samuel Bronson wrote:
> > > > > 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...
> > >
> > > Well, that's the thing, I never implemented users being able to use '?'
> > > and '??' directly, so I never needed to implement it for user defined
> > > kinds.
> >
> > Well, what are the KBase constructors for, then? "Future proofing" is
> > clearly not a very good answer...
>
> Oh, it is a direct analogy to a 'type scheme' in the type level
> typechecker. A kind can be either a 'kind' or a 'kind scheme' a 'kind
> scheme' is something you must instantiate to get a 'kind', just like
> 'forall a . a -> a' is not a type[1], but rather a type scheme. an
> actual type it can be instantiated to would be 'Int -> Int' or 'v1 ->
> v1' (where v1 is a type variable).
>
> now, I could extend the 'Kind' type to actually have the full
> quantification, but since the polymorphism allowed is always of a
> specific variety, it is easier and more straightforward to just have
> KQuest and KQuestQuest as placeholders.
>
> and Future Proofing is always a good answer, assuming one can back it
> up, full kind polymorphism is an eventual goal and the kind inference
> algorithm and terminology used was written with that in mind. oddly
> enough it leads to a much cleaner implementation than the THIH
> implementation as a side effect...

It's only a good answer if the code actually works... dead code
doesn't get much testing, generally...

> oh, also note that for all _infered_ kinds, due to defaulting, the kind
> scheme and the kind will be identical, but the distinction is quite
> important.
>
> [1]. we are ignoring rank 2 polymorphism for now, it doesn't complicate
> things really from an algorithmic point of view, but it would complicate
> the discussion and isn't relevant to kinds anyway.