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

On 3/18/08, Samuel Bronson wrote:

On 3/18/08, John Meacham wrote:

...

On Tue, Mar 18, 2008 at 06:52:04PM -0400, Samuel Bronson wrote:

...

On 3/18/08, John Meacham wrote:

...

'constrain' refines a type subject to constraints, kindCombine actually returns what the unification of the kinds are. constrain works on constraints, combine works on kinds. constraints don't necessarily map to kinds, though currently most have an analog.

Eh? Doesn't KindInfer run before typechecking begins?

excuse me, I meant 'kind', not 'type'. this terminology is real trickylike... At least I made sure that jhc core's axioms allowed a stratified type system so 'term','type','kind','superkind' all are distinct sets and have no cyclic dependencies... though, I am not sure if there are practical languages where that is not the case.. though wacky type systems are fun to play with.

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?