Re: [jhc] explanation of FrontEnd.KindInfer.constrain

On 3/19/08, John Meacham wrote:

On Wed, Mar 19, 2008 at 07:16:16PM -0400, Samuel Bronson wrote:

...

On 3/19/08, John Meacham 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.