[jhc] explanation of FrontEnd.KindInfer.constrain

[John Meacham]

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

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.

        John



-- 
John Meacham - ⑆repetae.net⑆john⑈